Metamath Proof Explorer


Theorem lsmcntz

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

Ref Expression
Hypotheses lsmcntz.p = ( LSSum ‘ 𝐺 )
lsmcntz.s ( 𝜑𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
lsmcntz.t ( 𝜑𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
lsmcntz.u ( 𝜑𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
lsmcntz.z 𝑍 = ( Cntz ‘ 𝐺 )
Assertion lsmcntz ( 𝜑 → ( ( 𝑆 𝑇 ) ⊆ ( 𝑍𝑈 ) ↔ ( 𝑆 ⊆ ( 𝑍𝑈 ) ∧ 𝑇 ⊆ ( 𝑍𝑈 ) ) ) )

Proof

Step Hyp Ref Expression
1 lsmcntz.p = ( LSSum ‘ 𝐺 )
2 lsmcntz.s ( 𝜑𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
3 lsmcntz.t ( 𝜑𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
4 lsmcntz.u ( 𝜑𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
5 lsmcntz.z 𝑍 = ( Cntz ‘ 𝐺 )
6 subgrcl ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
7 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
8 7 subgss ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
9 7 5 cntzsubg ( ( 𝐺 ∈ Grp ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑍𝑈 ) ∈ ( SubGrp ‘ 𝐺 ) )
10 6 8 9 syl2anc ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑍𝑈 ) ∈ ( SubGrp ‘ 𝐺 ) )
11 4 10 syl ( 𝜑 → ( 𝑍𝑈 ) ∈ ( SubGrp ‘ 𝐺 ) )
12 1 lsmlub ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑍𝑈 ) ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑆 ⊆ ( 𝑍𝑈 ) ∧ 𝑇 ⊆ ( 𝑍𝑈 ) ) ↔ ( 𝑆 𝑇 ) ⊆ ( 𝑍𝑈 ) ) )
13 2 3 11 12 syl3anc ( 𝜑 → ( ( 𝑆 ⊆ ( 𝑍𝑈 ) ∧ 𝑇 ⊆ ( 𝑍𝑈 ) ) ↔ ( 𝑆 𝑇 ) ⊆ ( 𝑍𝑈 ) ) )
14 13 bicomd ( 𝜑 → ( ( 𝑆 𝑇 ) ⊆ ( 𝑍𝑈 ) ↔ ( 𝑆 ⊆ ( 𝑍𝑈 ) ∧ 𝑇 ⊆ ( 𝑍𝑈 ) ) ) )