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 ) |