Metamath Proof Explorer

Theorem lsmcntzr

Description: The "subgroups commute" predicate applied to a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses lsmcntz.p 
|- .(+) = ( LSSum ` G )
lsmcntz.s 
|- ( ph -> S e. ( SubGrp ` G ) )
lsmcntz.t 
|- ( ph -> T e. ( SubGrp ` G ) )
lsmcntz.u 
|- ( ph -> U e. ( SubGrp ` G ) )
lsmcntz.z 
|- Z = ( Cntz ` G )
Assertion lsmcntzr 
|- ( ph -> ( S C_ ( Z ` ( T .(+) U ) ) <-> ( S C_ ( Z ` T ) /\ S C_ ( Z ` U ) ) ) )

Proof

Step Hyp Ref Expression
1 lsmcntz.p 
 |-  .(+) = ( LSSum ` G )
2 lsmcntz.s 
 |-  ( ph -> S e. ( SubGrp ` G ) )
3 lsmcntz.t 
 |-  ( ph -> T e. ( SubGrp ` G ) )
4 lsmcntz.u 
 |-  ( ph -> U e. ( SubGrp ` G ) )
5 lsmcntz.z 
 |-  Z = ( Cntz ` G )
6 1 3 4 2 5 lsmcntz 
 |-  ( ph -> ( ( T .(+) U ) C_ ( Z ` S ) <-> ( T C_ ( Z ` S ) /\ U C_ ( Z ` S ) ) ) )
7 subgrcl 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
8 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
9 2 7 8 3syl 
 |-  ( ph -> G e. Mnd )
10 eqid 
 |-  ( Base ` G ) = ( Base ` G )
11 10 subgss 
 |-  ( T e. ( SubGrp ` G ) -> T C_ ( Base ` G ) )
12 3 11 syl 
 |-  ( ph -> T C_ ( Base ` G ) )
13 10 subgss 
 |-  ( U e. ( SubGrp ` G ) -> U C_ ( Base ` G ) )
14 4 13 syl 
 |-  ( ph -> U C_ ( Base ` G ) )
15 10 1 lsmssv 
 |-  ( ( G e. Mnd /\ T C_ ( Base ` G ) /\ U C_ ( Base ` G ) ) -> ( T .(+) U ) C_ ( Base ` G ) )
16 9 12 14 15 syl3anc 
 |-  ( ph -> ( T .(+) U ) C_ ( Base ` G ) )
17 10 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ ( Base ` G ) )
18 2 17 syl 
 |-  ( ph -> S C_ ( Base ` G ) )
19 10 5 cntzrec 
 |-  ( ( ( T .(+) U ) C_ ( Base ` G ) /\ S C_ ( Base ` G ) ) -> ( ( T .(+) U ) C_ ( Z ` S ) <-> S C_ ( Z ` ( T .(+) U ) ) ) )
20 16 18 19 syl2anc 
 |-  ( ph -> ( ( T .(+) U ) C_ ( Z ` S ) <-> S C_ ( Z ` ( T .(+) U ) ) ) )
21 10 5 cntzrec 
 |-  ( ( T C_ ( Base ` G ) /\ S C_ ( Base ` G ) ) -> ( T C_ ( Z ` S ) <-> S C_ ( Z ` T ) ) )
22 12 18 21 syl2anc 
 |-  ( ph -> ( T C_ ( Z ` S ) <-> S C_ ( Z ` T ) ) )
23 10 5 cntzrec 
 |-  ( ( U C_ ( Base ` G ) /\ S C_ ( Base ` G ) ) -> ( U C_ ( Z ` S ) <-> S C_ ( Z ` U ) ) )
24 14 18 23 syl2anc 
 |-  ( ph -> ( U C_ ( Z ` S ) <-> S C_ ( Z ` U ) ) )
25 22 24 anbi12d 
 |-  ( ph -> ( ( T C_ ( Z ` S ) /\ U C_ ( Z ` S ) ) <-> ( S C_ ( Z ` T ) /\ S C_ ( Z ` U ) ) ) )
26 6 20 25 3bitr3d 
 |-  ( ph -> ( S C_ ( Z ` ( T .(+) U ) ) <-> ( S C_ ( Z ` T ) /\ S C_ ( Z ` U ) ) ) )