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