Metamath Proof Explorer


Theorem 0subm

Description: The zero submonoid of an arbitrary monoid. (Contributed by AV, 17-Feb-2024)

Ref Expression
Hypothesis 0subm.z 0 = ( 0g𝐺 )
Assertion 0subm ( 𝐺 ∈ Mnd → { 0 } ∈ ( SubMnd ‘ 𝐺 ) )

Proof

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