Metamath Proof Explorer

Theorem 00sr

Description: A signed real times 0 is 0. (Contributed by NM, 10-Apr-1996) (New usage is discouraged.)

Ref Expression
Assertion 00sr 
|- ( A e. R. -> ( A .R 0R ) = 0R )

Proof

Step Hyp Ref Expression
1 df-nr 
 |-  R. = ( ( P. X. P. ) /. ~R )
2 oveq1 
 |-  ( [ <. x , y >. ] ~R = A -> ( [ <. x , y >. ] ~R .R 0R ) = ( A .R 0R ) )
3 2 eqeq1d 
 |-  ( [ <. x , y >. ] ~R = A -> ( ( [ <. x , y >. ] ~R .R 0R ) = 0R <-> ( A .R 0R ) = 0R ) )
4 1pr 
 |-  1P e. P.
5 mulsrpr 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( 1P e. P. /\ 1P e. P. ) ) -> ( [ <. x , y >. ] ~R .R [ <. 1P , 1P >. ] ~R ) = [ <. ( ( x .P. 1P ) +P. ( y .P. 1P ) ) , ( ( x .P. 1P ) +P. ( y .P. 1P ) ) >. ] ~R )
6 4 4 5 mpanr12 
 |-  ( ( x e. P. /\ y e. P. ) -> ( [ <. x , y >. ] ~R .R [ <. 1P , 1P >. ] ~R ) = [ <. ( ( x .P. 1P ) +P. ( y .P. 1P ) ) , ( ( x .P. 1P ) +P. ( y .P. 1P ) ) >. ] ~R )
7 mulclpr 
 |-  ( ( x e. P. /\ 1P e. P. ) -> ( x .P. 1P ) e. P. )
8 4 7 mpan2 
 |-  ( x e. P. -> ( x .P. 1P ) e. P. )
9 mulclpr 
 |-  ( ( y e. P. /\ 1P e. P. ) -> ( y .P. 1P ) e. P. )
10 4 9 mpan2 
 |-  ( y e. P. -> ( y .P. 1P ) e. P. )
11 addclpr 
 |-  ( ( ( x .P. 1P ) e. P. /\ ( y .P. 1P ) e. P. ) -> ( ( x .P. 1P ) +P. ( y .P. 1P ) ) e. P. )
12 8 10 11 syl2an 
 |-  ( ( x e. P. /\ y e. P. ) -> ( ( x .P. 1P ) +P. ( y .P. 1P ) ) e. P. )
13 12 12 anim12i 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( x e. P. /\ y e. P. ) ) -> ( ( ( x .P. 1P ) +P. ( y .P. 1P ) ) e. P. /\ ( ( x .P. 1P ) +P. ( y .P. 1P ) ) e. P. ) )
14 eqid 
 |-  ( ( ( x .P. 1P ) +P. ( y .P. 1P ) ) +P. 1P ) = ( ( ( x .P. 1P ) +P. ( y .P. 1P ) ) +P. 1P )
15 enreceq 
 |-  ( ( ( ( ( x .P. 1P ) +P. ( y .P. 1P ) ) e. P. /\ ( ( x .P. 1P ) +P. ( y .P. 1P ) ) e. P. ) /\ ( 1P e. P. /\ 1P e. P. ) ) -> ( [ <. ( ( x .P. 1P ) +P. ( y .P. 1P ) ) , ( ( x .P. 1P ) +P. ( y .P. 1P ) ) >. ] ~R = [ <. 1P , 1P >. ] ~R <-> ( ( ( x .P. 1P ) +P. ( y .P. 1P ) ) +P. 1P ) = ( ( ( x .P. 1P ) +P. ( y .P. 1P ) ) +P. 1P ) ) )
16 14 15 mpbiri 
 |-  ( ( ( ( ( x .P. 1P ) +P. ( y .P. 1P ) ) e. P. /\ ( ( x .P. 1P ) +P. ( y .P. 1P ) ) e. P. ) /\ ( 1P e. P. /\ 1P e. P. ) ) -> [ <. ( ( x .P. 1P ) +P. ( y .P. 1P ) ) , ( ( x .P. 1P ) +P. ( y .P. 1P ) ) >. ] ~R = [ <. 1P , 1P >. ] ~R )
17 13 16 sylan 
 |-  ( ( ( ( x e. P. /\ y e. P. ) /\ ( x e. P. /\ y e. P. ) ) /\ ( 1P e. P. /\ 1P e. P. ) ) -> [ <. ( ( x .P. 1P ) +P. ( y .P. 1P ) ) , ( ( x .P. 1P ) +P. ( y .P. 1P ) ) >. ] ~R = [ <. 1P , 1P >. ] ~R )
18 4 4 17 mpanr12 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( x e. P. /\ y e. P. ) ) -> [ <. ( ( x .P. 1P ) +P. ( y .P. 1P ) ) , ( ( x .P. 1P ) +P. ( y .P. 1P ) ) >. ] ~R = [ <. 1P , 1P >. ] ~R )
19 18 anidms 
 |-  ( ( x e. P. /\ y e. P. ) -> [ <. ( ( x .P. 1P ) +P. ( y .P. 1P ) ) , ( ( x .P. 1P ) +P. ( y .P. 1P ) ) >. ] ~R = [ <. 1P , 1P >. ] ~R )
20 6 19 eqtrd 
 |-  ( ( x e. P. /\ y e. P. ) -> ( [ <. x , y >. ] ~R .R [ <. 1P , 1P >. ] ~R ) = [ <. 1P , 1P >. ] ~R )
21 df-0r 
 |-  0R = [ <. 1P , 1P >. ] ~R
22 21 oveq2i 
 |-  ( [ <. x , y >. ] ~R .R 0R ) = ( [ <. x , y >. ] ~R .R [ <. 1P , 1P >. ] ~R )
23 20 22 21 3eqtr4g 
 |-  ( ( x e. P. /\ y e. P. ) -> ( [ <. x , y >. ] ~R .R 0R ) = 0R )
24 1 3 23 ecoptocl 
 |-  ( A e. R. -> ( A .R 0R ) = 0R )