0subm

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

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

Proof

Step	Hyp	Ref	Expression
1		0subm.z	⊢ 0 = ( 0_g ‘ 𝐺 )
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	biimtrid	⊢ ( 𝐺 ∈ 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 ‘ 𝐺 ) )

Metamath Proof Explorer

Theorem 0subm

Proof