This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → ( ( 𝑆 ⊕ 𝑇 ) ⊆ ( 𝑍 ‘ 𝑈 ) ↔ ( 𝑆 ⊆ ( 𝑍 ‘ 𝑈 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ) )