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

Metamath Proof Explorer

Theorem cntzrecd

Description: Commute the "subgroups commute" predicate. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses cntzrecd.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
cntzrecd.t ⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
cntzrecd.u ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
cntzrecd.s ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) )
Assertion cntzrecd ( 𝜑 → 𝑈 ⊆ ( 𝑍 ‘ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 cntzrecd.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
2 cntzrecd.t ⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
3 cntzrecd.u ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
4 cntzrecd.s ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) )
5 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
6 5 subgss ⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
7 5 subgss ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
8 5 1 cntzrec ⊢ ( ( 𝑇 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ↔ 𝑈 ⊆ ( 𝑍 ‘ 𝑇 ) ) )
9 6 7 8 syl2an ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ↔ 𝑈 ⊆ ( 𝑍 ‘ 𝑇 ) ) )
10 2 3 9 syl2anc ⊢ ( 𝜑 → ( 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ↔ 𝑈 ⊆ ( 𝑍 ‘ 𝑇 ) ) )
11 4 10 mpbid ⊢ ( 𝜑 → 𝑈 ⊆ ( 𝑍 ‘ 𝑇 ) )