Metamath Proof Explorer

Theorem mulresr

Description: Multiplication of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996) (New usage is discouraged.)

Ref Expression
Assertion mulresr 
|- ( ( A e. R. /\ B e. R. ) -> ( <. A , 0R >. x. <. B , 0R >. ) = <. ( A .R B ) , 0R >. )

Proof

Step Hyp Ref Expression
1 0r 
 |-  0R e. R.
2 mulcnsr 
 |-  ( ( ( A e. R. /\ 0R e. R. ) /\ ( B e. R. /\ 0R e. R. ) ) -> ( <. A , 0R >. x. <. B , 0R >. ) = <. ( ( A .R B ) +R ( -1R .R ( 0R .R 0R ) ) ) , ( ( 0R .R B ) +R ( A .R 0R ) ) >. )
3 2 an4s 
 |-  ( ( ( A e. R. /\ B e. R. ) /\ ( 0R e. R. /\ 0R e. R. ) ) -> ( <. A , 0R >. x. <. B , 0R >. ) = <. ( ( A .R B ) +R ( -1R .R ( 0R .R 0R ) ) ) , ( ( 0R .R B ) +R ( A .R 0R ) ) >. )
4 1 1 3 mpanr12 
 |-  ( ( A e. R. /\ B e. R. ) -> ( <. A , 0R >. x. <. B , 0R >. ) = <. ( ( A .R B ) +R ( -1R .R ( 0R .R 0R ) ) ) , ( ( 0R .R B ) +R ( A .R 0R ) ) >. )
5 00sr 
 |-  ( 0R e. R. -> ( 0R .R 0R ) = 0R )
6 1 5 ax-mp 
 |-  ( 0R .R 0R ) = 0R
7 6 oveq2i 
 |-  ( -1R .R ( 0R .R 0R ) ) = ( -1R .R 0R )
8 m1r 
 |-  -1R e. R.
9 00sr 
 |-  ( -1R e. R. -> ( -1R .R 0R ) = 0R )
10 8 9 ax-mp 
 |-  ( -1R .R 0R ) = 0R
11 7 10 eqtri 
 |-  ( -1R .R ( 0R .R 0R ) ) = 0R
12 11 oveq2i 
 |-  ( ( A .R B ) +R ( -1R .R ( 0R .R 0R ) ) ) = ( ( A .R B ) +R 0R )
13 mulclsr 
 |-  ( ( A e. R. /\ B e. R. ) -> ( A .R B ) e. R. )
14 0idsr 
 |-  ( ( A .R B ) e. R. -> ( ( A .R B ) +R 0R ) = ( A .R B ) )
15 13 14 syl 
 |-  ( ( A e. R. /\ B e. R. ) -> ( ( A .R B ) +R 0R ) = ( A .R B ) )
16 12 15 syl5eq 
 |-  ( ( A e. R. /\ B e. R. ) -> ( ( A .R B ) +R ( -1R .R ( 0R .R 0R ) ) ) = ( A .R B ) )
17 mulcomsr 
 |-  ( 0R .R B ) = ( B .R 0R )
18 00sr 
 |-  ( B e. R. -> ( B .R 0R ) = 0R )
19 17 18 syl5eq 
 |-  ( B e. R. -> ( 0R .R B ) = 0R )
20 00sr 
 |-  ( A e. R. -> ( A .R 0R ) = 0R )
21 19 20 oveqan12rd 
 |-  ( ( A e. R. /\ B e. R. ) -> ( ( 0R .R B ) +R ( A .R 0R ) ) = ( 0R +R 0R ) )
22 0idsr 
 |-  ( 0R e. R. -> ( 0R +R 0R ) = 0R )
23 1 22 ax-mp 
 |-  ( 0R +R 0R ) = 0R
24 21 23 syl6eq 
 |-  ( ( A e. R. /\ B e. R. ) -> ( ( 0R .R B ) +R ( A .R 0R ) ) = 0R )
25 16 24 opeq12d 
 |-  ( ( A e. R. /\ B e. R. ) -> <. ( ( A .R B ) +R ( -1R .R ( 0R .R 0R ) ) ) , ( ( 0R .R B ) +R ( A .R 0R ) ) >. = <. ( A .R B ) , 0R >. )
26 4 25 eqtrd 
 |-  ( ( A e. R. /\ B e. R. ) -> ( <. A , 0R >. x. <. B , 0R >. ) = <. ( A .R B ) , 0R >. )