Metamath Proof Explorer

Theorem signsw0glem

Description: Neutral element property of .+^ . (Contributed by Thierry Arnoux, 9-Sep-2018)

Ref Expression
Hypothesis signsw.p 
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )
Assertion signsw0glem 
|- A. u e. { -u 1 , 0 , 1 } ( ( 0 .+^ u ) = u /\ ( u .+^ 0 ) = u )

Proof

Step Hyp Ref Expression
1 signsw.p 
 |-  .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )
2 c0ex 
 |-  0 e. _V
3 2 tpid2 
 |-  0 e. { -u 1 , 0 , 1 }
4 1 signspval 
 |-  ( ( 0 e. { -u 1 , 0 , 1 } /\ u e. { -u 1 , 0 , 1 } ) -> ( 0 .+^ u ) = if ( u = 0 , 0 , u ) )
5 3 4 mpan 
 |-  ( u e. { -u 1 , 0 , 1 } -> ( 0 .+^ u ) = if ( u = 0 , 0 , u ) )
6 iftrue 
 |-  ( u = 0 -> if ( u = 0 , 0 , u ) = 0 )
7 id 
 |-  ( u = 0 -> u = 0 )
8 6 7 eqtr4d 
 |-  ( u = 0 -> if ( u = 0 , 0 , u ) = u )
9 iffalse 
 |-  ( -. u = 0 -> if ( u = 0 , 0 , u ) = u )
10 8 9 pm2.61i 
 |-  if ( u = 0 , 0 , u ) = u
11 5 10 eqtrdi 
 |-  ( u e. { -u 1 , 0 , 1 } -> ( 0 .+^ u ) = u )
12 1 signspval 
 |-  ( ( u e. { -u 1 , 0 , 1 } /\ 0 e. { -u 1 , 0 , 1 } ) -> ( u .+^ 0 ) = if ( 0 = 0 , u , 0 ) )
13 3 12 mpan2 
 |-  ( u e. { -u 1 , 0 , 1 } -> ( u .+^ 0 ) = if ( 0 = 0 , u , 0 ) )
14 eqid 
 |-  0 = 0
15 14 iftruei 
 |-  if ( 0 = 0 , u , 0 ) = u
16 13 15 eqtrdi 
 |-  ( u e. { -u 1 , 0 , 1 } -> ( u .+^ 0 ) = u )
17 11 16 jca 
 |-  ( u e. { -u 1 , 0 , 1 } -> ( ( 0 .+^ u ) = u /\ ( u .+^ 0 ) = u ) )
18 17 rgen 
 |-  A. u e. { -u 1 , 0 , 1 } ( ( 0 .+^ u ) = u /\ ( u .+^ 0 ) = u )