Metamath Proof Explorer

Theorem abl1

Description: The (smallest) structure representing atrivial abelian group. (Contributed by AV, 28-Apr-2019)

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

Proof

Step Hyp Ref Expression
1 abl1.m 
 |-  M = { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. }
2 1 grp1 
 |-  ( I e. V -> M e. Grp )
3 eqidd 
 |-  ( I e. V -> ( I { <. <. I , I >. , I >. } I ) = ( I { <. <. I , I >. , I >. } I ) )
4 oveq1 
 |-  ( a = I -> ( a { <. <. I , I >. , I >. } b ) = ( I { <. <. I , I >. , I >. } b ) )
5 oveq2 
 |-  ( a = I -> ( b { <. <. I , I >. , I >. } a ) = ( b { <. <. I , I >. , I >. } I ) )
6 4 5 eqeq12d 
 |-  ( a = I -> ( ( a { <. <. I , I >. , I >. } b ) = ( b { <. <. I , I >. , I >. } a ) <-> ( I { <. <. I , I >. , I >. } b ) = ( b { <. <. I , I >. , I >. } I ) ) )
7 6 ralbidv 
 |-  ( a = I -> ( A. b e. { I } ( a { <. <. I , I >. , I >. } b ) = ( b { <. <. I , I >. , I >. } a ) <-> A. b e. { I } ( I { <. <. I , I >. , I >. } b ) = ( b { <. <. I , I >. , I >. } I ) ) )
8 7 ralsng 
 |-  ( I e. V -> ( A. a e. { I } A. b e. { I } ( a { <. <. I , I >. , I >. } b ) = ( b { <. <. I , I >. , I >. } a ) <-> A. b e. { I } ( I { <. <. I , I >. , I >. } b ) = ( b { <. <. I , I >. , I >. } I ) ) )
9 oveq2 
 |-  ( b = I -> ( I { <. <. I , I >. , I >. } b ) = ( I { <. <. I , I >. , I >. } I ) )
10 oveq1 
 |-  ( b = I -> ( b { <. <. I , I >. , I >. } I ) = ( I { <. <. I , I >. , I >. } I ) )
11 9 10 eqeq12d 
 |-  ( b = I -> ( ( I { <. <. I , I >. , I >. } b ) = ( b { <. <. I , I >. , I >. } I ) <-> ( I { <. <. I , I >. , I >. } I ) = ( I { <. <. I , I >. , I >. } I ) ) )
12 11 ralsng 
 |-  ( I e. V -> ( A. b e. { I } ( I { <. <. I , I >. , I >. } b ) = ( b { <. <. I , I >. , I >. } I ) <-> ( I { <. <. I , I >. , I >. } I ) = ( I { <. <. I , I >. , I >. } I ) ) )
13 8 12 bitrd 
 |-  ( I e. V -> ( A. a e. { I } A. b e. { I } ( a { <. <. I , I >. , I >. } b ) = ( b { <. <. I , I >. , I >. } a ) <-> ( I { <. <. I , I >. , I >. } I ) = ( I { <. <. I , I >. , I >. } I ) ) )
14 3 13 mpbird 
 |-  ( I e. V -> A. a e. { I } A. b e. { I } ( a { <. <. I , I >. , I >. } b ) = ( b { <. <. I , I >. , I >. } a ) )
15 snex 
 |-  { I } e. _V
16 1 grpbase 
 |-  ( { I } e. _V -> { I } = ( Base ` M ) )
17 15 16 ax-mp 
 |-  { I } = ( Base ` M )
18 snex 
 |-  { <. <. I , I >. , I >. } e. _V
19 1 grpplusg 
 |-  ( { <. <. I , I >. , I >. } e. _V -> { <. <. I , I >. , I >. } = ( +g ` M ) )
20 18 19 ax-mp 
 |-  { <. <. I , I >. , I >. } = ( +g ` M )
21 17 20 isabl2 
 |-  ( M e. Abel <-> ( M e. Grp /\ A. a e. { I } A. b e. { I } ( a { <. <. I , I >. , I >. } b ) = ( b { <. <. I , I >. , I >. } a ) ) )
22 2 14 21 sylanbrc 
 |-  ( I e. V -> M e. Abel )