let G be Group; :: thesis: ( G is finite implies for C being Subgroup of G
for A, B being Subgroup of C
for D being Subgroup of A st D = A /\ B holds
for E being Subgroup of B st E = A /\ B holds
for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_coprime holds
( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) )
assume A1: G is finite ; :: thesis: for C being Subgroup of G
for A, B being Subgroup of C
for D being Subgroup of A st D = A /\ B holds
for E being Subgroup of B st E = A /\ B holds
for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_coprime holds
( index (C,B) = index (A,D) & index (C,A) = index (B,E) )
let C be Subgroup of G; :: thesis: for A, B being Subgroup of C
for D being Subgroup of A st D = A /\ B holds
for E being Subgroup of B st E = A /\ B holds
for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_coprime holds
( index (C,B) = index (A,D) & index (C,A) = index (B,E) )
let A, B be Subgroup of C; :: thesis: for D being Subgroup of A st D = A /\ B holds
for E being Subgroup of B st E = A /\ B holds
for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_coprime holds
( index (C,B) = index (A,D) & index (C,A) = index (B,E) )
let D be Subgroup of A; :: thesis: ( D = A /\ B implies for E being Subgroup of B st E = A /\ B holds
for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_coprime holds
( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) )
assume A2: D = A /\ B ; :: thesis: for E being Subgroup of B st E = A /\ B holds
for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_coprime holds
( index (C,B) = index (A,D) & index (C,A) = index (B,E) )
let E be Subgroup of B; :: thesis: ( E = A /\ B implies for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_coprime holds
( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) )
assume A3: E = A /\ B ; :: thesis: for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_coprime holds
( index (C,B) = index (A,D) & index (C,A) = index (B,E) )
let F be Subgroup of C; :: thesis: ( F = A /\ B & index (C,A), index (C,B) are_coprime implies ( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) )
assume A4: F = A /\ B ; :: thesis: ( not index (C,A), index (C,B) are_coprime or ( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) )
assume A5: index A, index B are_coprime ; :: thesis: ( index (C,B) = index (A,D) & index (C,A) = index (B,E) )
index F = (index E) * (index B) by A1, A3, A4, GROUP_2:149;
then A6: (index E) * (index B) = (index D) * (index A) by A1, A2, A4, GROUP_2:149;
then index B divides (index A) * (index D) by INT_1:def 3;
then A7: index B divides index D by A5, INT_2:25;
ex n being Element of NAT st index D = (index B) * n
proof
consider i being Integer such that
A8: index D = (index B) * i by A7, INT_1:def 3;
0 <= i by A1, A8, Th20;
then reconsider i = i as Element of NAT by INT_1:3;
take i ; :: thesis: index D = (index B) * i
thus index D = (index B) * i by A8; :: thesis: verum
end;
then A9: index B divides index D by NAT_D:def 3;
A10: index (C,B) >= index (A,D) by A1, A2, Th19;
A11: index B = index D
proof
assume A12: index B <> index D ; :: thesis: contradiction
index D > 0 by A1, Th20;
then index B <= index D by A9, NAT_D:7;
hence contradiction by A10, A12, XXREAL_0:1; :: thesis: verum
end;
index A divides (index B) * (index E) by A6, INT_1:def 3;
then A13: index A divides index E by A5, INT_2:25;
ex n being Element of NAT st index E = (index A) * n
proof
consider i being Integer such that
A14: index E = (index A) * i by A13, INT_1:def 3;
0 <= i by A1, A14, Th20;
then reconsider i = i as Element of NAT by INT_1:3;
take i ; :: thesis: index E = (index A) * i
thus index E = (index A) * i by A14; :: thesis: verum
end;
then A15: index A divides index E by NAT_D:def 3;
A16: index A >= index E by A1, A3, Th19;
index A = index E
proof
assume A17: index A <> index E ; :: thesis: contradiction
index E > 0 by A1, Th20;
then index A <= index E by A15, NAT_D:7;
hence contradiction by A16, A17, XXREAL_0:1; :: thesis: verum
end;
hence ( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) by A11; :: thesis: verum