0subm

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

		Ref	Expression
	Hypothesis	0subm.z	\|- .0. = ( 0g ` G )
	Assertion	0subm	\|- ( G e. Mnd -> { .0. } e. ( SubMnd ` G ) )

Proof

Step	Hyp	Ref	Expression
1		0subm.z	\|- .0. = ( 0g ` G )
2		eqid	\|- ( Base ` G ) = ( Base ` G )
3	2 1	mndidcl	\|- ( G e. Mnd -> .0. e. ( Base ` G ) )
4	3	snssd	\|- ( G e. Mnd -> { .0. } C_ ( Base ` G ) )
5	1	fvexi	\|- .0. e. _V
6	5	snid	\|- .0. e. { .0. }
7	6	a1i	\|- ( G e. Mnd -> .0. e. { .0. } )
8		velsn	\|- ( a e. { .0. } <-> a = .0. )
9		velsn	\|- ( b e. { .0. } <-> b = .0. )
10	8 9	anbi12i	\|- ( ( a e. { .0. } /\ b e. { .0. } ) <-> ( a = .0. /\ b = .0. ) )
11		eqid	\|- ( +g ` G ) = ( +g ` G )
12	2 11 1	mndlid	\|- ( ( G e. Mnd /\ .0. e. ( Base ` G ) ) -> ( .0. ( +g ` G ) .0. ) = .0. )
13	3 12	mpdan	\|- ( G e. Mnd -> ( .0. ( +g ` G ) .0. ) = .0. )
14		ovex	\|- ( .0. ( +g ` G ) .0. ) e. _V
15	14	elsn	\|- ( ( .0. ( +g ` G ) .0. ) e. { .0. } <-> ( .0. ( +g ` G ) .0. ) = .0. )
16	13 15	sylibr	\|- ( G e. Mnd -> ( .0. ( +g ` G ) .0. ) e. { .0. } )
17		oveq12	\|- ( ( a = .0. /\ b = .0. ) -> ( a ( +g ` G ) b ) = ( .0. ( +g ` G ) .0. ) )
18	17	eleq1d	\|- ( ( a = .0. /\ b = .0. ) -> ( ( a ( +g ` G ) b ) e. { .0. } <-> ( .0. ( +g ` G ) .0. ) e. { .0. } ) )
19	16 18	syl5ibrcom	\|- ( G e. Mnd -> ( ( a = .0. /\ b = .0. ) -> ( a ( +g ` G ) b ) e. { .0. } ) )
20	10 19	biimtrid	\|- ( G e. Mnd -> ( ( a e. { .0. } /\ b e. { .0. } ) -> ( a ( +g ` G ) b ) e. { .0. } ) )
21	20	ralrimivv	\|- ( G e. Mnd -> A. a e. { .0. } A. b e. { .0. } ( a ( +g ` G ) b ) e. { .0. } )
22	2 1 11	issubm	\|- ( G e. Mnd -> ( { .0. } e. ( SubMnd ` G ) <-> ( { .0. } C_ ( Base ` G ) /\ .0. e. { .0. } /\ A. a e. { .0. } A. b e. { .0. } ( a ( +g ` G ) b ) e. { .0. } ) ) )
23	4 7 21 22	mpbir3and	\|- ( G e. Mnd -> { .0. } e. ( SubMnd ` G ) )

Metamath Proof Explorer

Theorem 0subm

Proof