Theorem gsumvallem2

Description: Lemma for properties of the set of identities of G . The set of identities of a monoid is exactly the unique identity element. (Contributed by Mario Carneiro, 7-Dec-2014)

	Ref	Expression
Hypotheses	gsumvallem2.b	|- B = ( Base ` G )
	gsumvallem2.z	|- .0. = ( 0g ` G )
	gsumvallem2.p	|- .+ = ( +g ` G )
	gsumvallem2.o	|- O = { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) }
Assertion	gsumvallem2	|- ( G e. Mnd -> O = { .0. } )

Proof

Step	Hyp	Ref	Expression
1		gsumvallem2.b	|- B = ( Base ` G )
2		gsumvallem2.z	|- .0. = ( 0g ` G )
3		gsumvallem2.p	|- .+ = ( +g ` G )
4		gsumvallem2.o	|- O = { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) }
5	1 2 3 4	mgmidsssn0	|- ( G e. Mnd -> O C_ { .0. } )
6	1 2	mndidcl	|- ( G e. Mnd -> .0. e. B )
7	1 3 2	mndlrid	|- ( ( G e. Mnd /\ y e. B ) -> ( ( .0. .+ y ) = y /\ ( y .+ .0. ) = y ) )
8	7	ralrimiva	|- ( G e. Mnd -> A. y e. B ( ( .0. .+ y ) = y /\ ( y .+ .0. ) = y ) )
9		oveq1	|- ( x = .0. -> ( x .+ y ) = ( .0. .+ y ) )
10	9	eqeq1d	|- ( x = .0. -> ( ( x .+ y ) = y <-> ( .0. .+ y ) = y ) )
11	10	ovanraleqv	|- ( x = .0. -> ( A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) <-> A. y e. B ( ( .0. .+ y ) = y /\ ( y .+ .0. ) = y ) ) )
12	11 4	elrab2	|- ( .0. e. O <-> ( .0. e. B /\ A. y e. B ( ( .0. .+ y ) = y /\ ( y .+ .0. ) = y ) ) )
13	6 8 12	sylanbrc	|- ( G e. Mnd -> .0. e. O )
14	13	snssd	|- ( G e. Mnd -> { .0. } C_ O )
15	5 14	eqssd	|- ( G e. Mnd -> O = { .0. } )