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 ‘ 𝐺 )
lsmcntz.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
lsmcntz.t ⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
lsmcntz.u ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
lsmcntz.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
Assertion lsmcntzr ( 𝜑 → ( 𝑆 ⊆ ( 𝑍 ‘ ( 𝑇 ⊕ 𝑈 ) ) ↔ ( 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑈 ) ) ) )

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 1 3 4 2 5 lsmcntz ⊢ ( 𝜑 → ( ( 𝑇 ⊕ 𝑈 ) ⊆ ( 𝑍 ‘ 𝑆 ) ↔ ( 𝑇 ⊆ ( 𝑍 ‘ 𝑆 ) ∧ 𝑈 ⊆ ( 𝑍 ‘ 𝑆 ) ) ) )
7 subgrcl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
8 grpmnd ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
9 2 7 8 3syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
10 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
11 10 subgss ⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
12 3 11 syl ⊢ ( 𝜑 → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
13 10 subgss ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
14 4 13 syl ⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
15 10 1 lsmssv ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑇 ⊕ 𝑈 ) ⊆ ( Base ‘ 𝐺 ) )
16 9 12 14 15 syl3anc ⊢ ( 𝜑 → ( 𝑇 ⊕ 𝑈 ) ⊆ ( Base ‘ 𝐺 ) )
17 10 subgss ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
18 2 17 syl ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
19 10 5 cntzrec ⊢ ( ( ( 𝑇 ⊕ 𝑈 ) ⊆ ( Base ‘ 𝐺 ) ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) → ( ( 𝑇 ⊕ 𝑈 ) ⊆ ( 𝑍 ‘ 𝑆 ) ↔ 𝑆 ⊆ ( 𝑍 ‘ ( 𝑇 ⊕ 𝑈 ) ) ) )
20 16 18 19 syl2anc ⊢ ( 𝜑 → ( ( 𝑇 ⊕ 𝑈 ) ⊆ ( 𝑍 ‘ 𝑆 ) ↔ 𝑆 ⊆ ( 𝑍 ‘ ( 𝑇 ⊕ 𝑈 ) ) ) )
21 10 5 cntzrec ⊢ ( ( 𝑇 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑇 ⊆ ( 𝑍 ‘ 𝑆 ) ↔ 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) ) )
22 12 18 21 syl2anc ⊢ ( 𝜑 → ( 𝑇 ⊆ ( 𝑍 ‘ 𝑆 ) ↔ 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) ) )
23 10 5 cntzrec ⊢ ( ( 𝑈 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑈 ⊆ ( 𝑍 ‘ 𝑆 ) ↔ 𝑆 ⊆ ( 𝑍 ‘ 𝑈 ) ) )
24 14 18 23 syl2anc ⊢ ( 𝜑 → ( 𝑈 ⊆ ( 𝑍 ‘ 𝑆 ) ↔ 𝑆 ⊆ ( 𝑍 ‘ 𝑈 ) ) )
25 22 24 anbi12d ⊢ ( 𝜑 → ( ( 𝑇 ⊆ ( 𝑍 ‘ 𝑆 ) ∧ 𝑈 ⊆ ( 𝑍 ‘ 𝑆 ) ) ↔ ( 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑈 ) ) ) )
26 6 20 25 3bitr3d ⊢ ( 𝜑 → ( 𝑆 ⊆ ( 𝑍 ‘ ( 𝑇 ⊕ 𝑈 ) ) ↔ ( 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑈 ) ) ) )