Step |
Hyp |
Ref |
Expression |
1 |
|
dprd0.0 |
⊢ 0 = ( 0g ‘ 𝐺 ) |
2 |
|
0ex |
⊢ ∅ ∈ V |
3 |
1
|
dprdz |
⊢ ( ( 𝐺 ∈ Grp ∧ ∅ ∈ V ) → ( 𝐺 dom DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ∧ ( 𝐺 DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ) = { 0 } ) ) |
4 |
2 3
|
mpan2 |
⊢ ( 𝐺 ∈ Grp → ( 𝐺 dom DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ∧ ( 𝐺 DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ) = { 0 } ) ) |
5 |
|
mpt0 |
⊢ ( 𝑥 ∈ ∅ ↦ { 0 } ) = ∅ |
6 |
5
|
breq2i |
⊢ ( 𝐺 dom DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ↔ 𝐺 dom DProd ∅ ) |
7 |
5
|
oveq2i |
⊢ ( 𝐺 DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ) = ( 𝐺 DProd ∅ ) |
8 |
7
|
eqeq1i |
⊢ ( ( 𝐺 DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ) = { 0 } ↔ ( 𝐺 DProd ∅ ) = { 0 } ) |
9 |
6 8
|
anbi12i |
⊢ ( ( 𝐺 dom DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ∧ ( 𝐺 DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ) = { 0 } ) ↔ ( 𝐺 dom DProd ∅ ∧ ( 𝐺 DProd ∅ ) = { 0 } ) ) |
10 |
4 9
|
sylib |
⊢ ( 𝐺 ∈ Grp → ( 𝐺 dom DProd ∅ ∧ ( 𝐺 DProd ∅ ) = { 0 } ) ) |