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 eqtrid 
 |-  ( 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 )