Metamath Proof Explorer


Theorem mnd1id

Description: The singleton element of atrivial monoid is its identity element. (Contributed by AV, 23-Jan-2020)

Ref Expression
Hypothesis mnd1.m
|- M = { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. }
Assertion mnd1id
|- ( I e. V -> ( 0g ` M ) = I )

Proof

Step Hyp Ref Expression
1 mnd1.m
 |-  M = { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. }
2 snex
 |-  { I } e. _V
3 1 grpbase
 |-  ( { I } e. _V -> { I } = ( Base ` M ) )
4 2 3 ax-mp
 |-  { I } = ( Base ` M )
5 eqid
 |-  ( 0g ` M ) = ( 0g ` M )
6 snex
 |-  { <. <. I , I >. , I >. } e. _V
7 1 grpplusg
 |-  ( { <. <. I , I >. , I >. } e. _V -> { <. <. I , I >. , I >. } = ( +g ` M ) )
8 6 7 ax-mp
 |-  { <. <. I , I >. , I >. } = ( +g ` M )
9 snidg
 |-  ( I e. V -> I e. { I } )
10 velsn
 |-  ( a e. { I } <-> a = I )
11 df-ov
 |-  ( I { <. <. I , I >. , I >. } I ) = ( { <. <. I , I >. , I >. } ` <. I , I >. )
12 opex
 |-  <. I , I >. e. _V
13 fvsng
 |-  ( ( <. I , I >. e. _V /\ I e. V ) -> ( { <. <. I , I >. , I >. } ` <. I , I >. ) = I )
14 12 13 mpan
 |-  ( I e. V -> ( { <. <. I , I >. , I >. } ` <. I , I >. ) = I )
15 11 14 syl5eq
 |-  ( I e. V -> ( I { <. <. I , I >. , I >. } I ) = I )
16 oveq2
 |-  ( a = I -> ( I { <. <. I , I >. , I >. } a ) = ( I { <. <. I , I >. , I >. } I ) )
17 id
 |-  ( a = I -> a = I )
18 16 17 eqeq12d
 |-  ( a = I -> ( ( I { <. <. I , I >. , I >. } a ) = a <-> ( I { <. <. I , I >. , I >. } I ) = I ) )
19 15 18 syl5ibrcom
 |-  ( I e. V -> ( a = I -> ( I { <. <. I , I >. , I >. } a ) = a ) )
20 10 19 syl5bi
 |-  ( I e. V -> ( a e. { I } -> ( I { <. <. I , I >. , I >. } a ) = a ) )
21 20 imp
 |-  ( ( I e. V /\ a e. { I } ) -> ( I { <. <. I , I >. , I >. } a ) = a )
22 oveq1
 |-  ( a = I -> ( a { <. <. I , I >. , I >. } I ) = ( I { <. <. I , I >. , I >. } I ) )
23 22 17 eqeq12d
 |-  ( a = I -> ( ( a { <. <. I , I >. , I >. } I ) = a <-> ( I { <. <. I , I >. , I >. } I ) = I ) )
24 15 23 syl5ibrcom
 |-  ( I e. V -> ( a = I -> ( a { <. <. I , I >. , I >. } I ) = a ) )
25 10 24 syl5bi
 |-  ( I e. V -> ( a e. { I } -> ( a { <. <. I , I >. , I >. } I ) = a ) )
26 25 imp
 |-  ( ( I e. V /\ a e. { I } ) -> ( a { <. <. I , I >. , I >. } I ) = a )
27 4 5 8 9 21 26 ismgmid2
 |-  ( I e. V -> I = ( 0g ` M ) )
28 27 eqcomd
 |-  ( I e. V -> ( 0g ` M ) = I )