Metamath Proof Explorer


Theorem dprdgrp

Description: Reverse closure for the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Assertion dprdgrp ( 𝐺 dom DProd 𝑆𝐺 ∈ Grp )

Proof

Step Hyp Ref Expression
1 reldmdprd Rel dom DProd
2 1 brrelex2i ( 𝐺 dom DProd 𝑆𝑆 ∈ V )
3 2 dmexd ( 𝐺 dom DProd 𝑆 → dom 𝑆 ∈ V )
4 eqid dom 𝑆 = dom 𝑆
5 eqid ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
6 eqid ( 0g𝐺 ) = ( 0g𝐺 )
7 eqid ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
8 5 6 7 dmdprd ( ( dom 𝑆 ∈ V ∧ dom 𝑆 = dom 𝑆 ) → ( 𝐺 dom DProd 𝑆 ↔ ( 𝐺 ∈ Grp ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆𝑦 ) ) ∧ ( ( 𝑆𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g𝐺 ) } ) ) ) )
9 3 4 8 sylancl ( 𝐺 dom DProd 𝑆 → ( 𝐺 dom DProd 𝑆 ↔ ( 𝐺 ∈ Grp ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆𝑦 ) ) ∧ ( ( 𝑆𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g𝐺 ) } ) ) ) )
10 9 ibi ( 𝐺 dom DProd 𝑆 → ( 𝐺 ∈ Grp ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆𝑦 ) ) ∧ ( ( 𝑆𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g𝐺 ) } ) ) )
11 10 simp1d ( 𝐺 dom DProd 𝑆𝐺 ∈ Grp )