Step |
Hyp |
Ref |
Expression |
1 |
|
0subm.z |
⊢ 0 = ( 0g ‘ 𝐺 ) |
2 |
|
eqid |
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) |
3 |
2 1
|
mndidcl |
⊢ ( 𝐺 ∈ Mnd → 0 ∈ ( Base ‘ 𝐺 ) ) |
4 |
3
|
snssd |
⊢ ( 𝐺 ∈ Mnd → { 0 } ⊆ ( Base ‘ 𝐺 ) ) |
5 |
1
|
fvexi |
⊢ 0 ∈ V |
6 |
5
|
snid |
⊢ 0 ∈ { 0 } |
7 |
6
|
a1i |
⊢ ( 𝐺 ∈ Mnd → 0 ∈ { 0 } ) |
8 |
|
velsn |
⊢ ( 𝑎 ∈ { 0 } ↔ 𝑎 = 0 ) |
9 |
|
velsn |
⊢ ( 𝑏 ∈ { 0 } ↔ 𝑏 = 0 ) |
10 |
8 9
|
anbi12i |
⊢ ( ( 𝑎 ∈ { 0 } ∧ 𝑏 ∈ { 0 } ) ↔ ( 𝑎 = 0 ∧ 𝑏 = 0 ) ) |
11 |
|
eqid |
⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) |
12 |
2 11 1
|
mndlid |
⊢ ( ( 𝐺 ∈ Mnd ∧ 0 ∈ ( Base ‘ 𝐺 ) ) → ( 0 ( +g ‘ 𝐺 ) 0 ) = 0 ) |
13 |
3 12
|
mpdan |
⊢ ( 𝐺 ∈ Mnd → ( 0 ( +g ‘ 𝐺 ) 0 ) = 0 ) |
14 |
|
ovex |
⊢ ( 0 ( +g ‘ 𝐺 ) 0 ) ∈ V |
15 |
14
|
elsn |
⊢ ( ( 0 ( +g ‘ 𝐺 ) 0 ) ∈ { 0 } ↔ ( 0 ( +g ‘ 𝐺 ) 0 ) = 0 ) |
16 |
13 15
|
sylibr |
⊢ ( 𝐺 ∈ Mnd → ( 0 ( +g ‘ 𝐺 ) 0 ) ∈ { 0 } ) |
17 |
|
oveq12 |
⊢ ( ( 𝑎 = 0 ∧ 𝑏 = 0 ) → ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) = ( 0 ( +g ‘ 𝐺 ) 0 ) ) |
18 |
17
|
eleq1d |
⊢ ( ( 𝑎 = 0 ∧ 𝑏 = 0 ) → ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ { 0 } ↔ ( 0 ( +g ‘ 𝐺 ) 0 ) ∈ { 0 } ) ) |
19 |
16 18
|
syl5ibrcom |
⊢ ( 𝐺 ∈ Mnd → ( ( 𝑎 = 0 ∧ 𝑏 = 0 ) → ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ { 0 } ) ) |
20 |
10 19
|
syl5bi |
⊢ ( 𝐺 ∈ Mnd → ( ( 𝑎 ∈ { 0 } ∧ 𝑏 ∈ { 0 } ) → ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ { 0 } ) ) |
21 |
20
|
ralrimivv |
⊢ ( 𝐺 ∈ Mnd → ∀ 𝑎 ∈ { 0 } ∀ 𝑏 ∈ { 0 } ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ { 0 } ) |
22 |
2 1 11
|
issubm |
⊢ ( 𝐺 ∈ Mnd → ( { 0 } ∈ ( SubMnd ‘ 𝐺 ) ↔ ( { 0 } ⊆ ( Base ‘ 𝐺 ) ∧ 0 ∈ { 0 } ∧ ∀ 𝑎 ∈ { 0 } ∀ 𝑏 ∈ { 0 } ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ { 0 } ) ) ) |
23 |
4 7 21 22
|
mpbir3and |
⊢ ( 𝐺 ∈ Mnd → { 0 } ∈ ( SubMnd ‘ 𝐺 ) ) |