let G be Group; ( 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
; 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; 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; 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; ( 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
; 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; ( 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
; 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; ( 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
; ( 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
; ( 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
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
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
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
hence
( index (C,B) = index (A,D) & index (C,A) = index (B,E) )
by A11; verum