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