Metamath Proof Explorer

Theorem m1m1sr

Description: Minus one times minus one is plus one for signed reals. (Contributed by NM, 14-May-1996) (New usage is discouraged.)

Ref Expression
Assertion m1m1sr 
|- ( -1R .R -1R ) = 1R

Proof

Step Hyp Ref Expression
1 df-m1r 
 |-  -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
2 1 1 oveq12i 
 |-  ( -1R .R -1R ) = ( [ <. 1P , ( 1P +P. 1P ) >. ] ~R .R [ <. 1P , ( 1P +P. 1P ) >. ] ~R )
3 df-1r 
 |-  1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
4 1pr 
 |-  1P e. P.
5 addclpr 
 |-  ( ( 1P e. P. /\ 1P e. P. ) -> ( 1P +P. 1P ) e. P. )
6 4 4 5 mp2an 
 |-  ( 1P +P. 1P ) e. P.
7 mulsrpr 
 |-  ( ( ( 1P e. P. /\ ( 1P +P. 1P ) e. P. ) /\ ( 1P e. P. /\ ( 1P +P. 1P ) e. P. ) ) -> ( [ <. 1P , ( 1P +P. 1P ) >. ] ~R .R [ <. 1P , ( 1P +P. 1P ) >. ] ~R ) = [ <. ( ( 1P .P. 1P ) +P. ( ( 1P +P. 1P ) .P. ( 1P +P. 1P ) ) ) , ( ( 1P .P. ( 1P +P. 1P ) ) +P. ( ( 1P +P. 1P ) .P. 1P ) ) >. ] ~R )
8 4 6 4 6 7 mp4an 
 |-  ( [ <. 1P , ( 1P +P. 1P ) >. ] ~R .R [ <. 1P , ( 1P +P. 1P ) >. ] ~R ) = [ <. ( ( 1P .P. 1P ) +P. ( ( 1P +P. 1P ) .P. ( 1P +P. 1P ) ) ) , ( ( 1P .P. ( 1P +P. 1P ) ) +P. ( ( 1P +P. 1P ) .P. 1P ) ) >. ] ~R
9 addasspr 
 |-  ( ( 1P +P. 1P ) +P. ( ( 1P .P. ( 1P +P. 1P ) ) +P. ( ( 1P +P. 1P ) .P. 1P ) ) ) = ( 1P +P. ( 1P +P. ( ( 1P .P. ( 1P +P. 1P ) ) +P. ( ( 1P +P. 1P ) .P. 1P ) ) ) )
10 1idpr 
 |-  ( 1P e. P. -> ( 1P .P. 1P ) = 1P )
11 4 10 ax-mp 
 |-  ( 1P .P. 1P ) = 1P
12 distrpr 
 |-  ( ( 1P +P. 1P ) .P. ( 1P +P. 1P ) ) = ( ( ( 1P +P. 1P ) .P. 1P ) +P. ( ( 1P +P. 1P ) .P. 1P ) )
13 mulcompr 
 |-  ( 1P .P. ( 1P +P. 1P ) ) = ( ( 1P +P. 1P ) .P. 1P )
14 13 oveq1i 
 |-  ( ( 1P .P. ( 1P +P. 1P ) ) +P. ( ( 1P +P. 1P ) .P. 1P ) ) = ( ( ( 1P +P. 1P ) .P. 1P ) +P. ( ( 1P +P. 1P ) .P. 1P ) )
15 12 14 eqtr4i 
 |-  ( ( 1P +P. 1P ) .P. ( 1P +P. 1P ) ) = ( ( 1P .P. ( 1P +P. 1P ) ) +P. ( ( 1P +P. 1P ) .P. 1P ) )
16 11 15 oveq12i 
 |-  ( ( 1P .P. 1P ) +P. ( ( 1P +P. 1P ) .P. ( 1P +P. 1P ) ) ) = ( 1P +P. ( ( 1P .P. ( 1P +P. 1P ) ) +P. ( ( 1P +P. 1P ) .P. 1P ) ) )
17 16 oveq2i 
 |-  ( 1P +P. ( ( 1P .P. 1P ) +P. ( ( 1P +P. 1P ) .P. ( 1P +P. 1P ) ) ) ) = ( 1P +P. ( 1P +P. ( ( 1P .P. ( 1P +P. 1P ) ) +P. ( ( 1P +P. 1P ) .P. 1P ) ) ) )
18 9 17 eqtr4i 
 |-  ( ( 1P +P. 1P ) +P. ( ( 1P .P. ( 1P +P. 1P ) ) +P. ( ( 1P +P. 1P ) .P. 1P ) ) ) = ( 1P +P. ( ( 1P .P. 1P ) +P. ( ( 1P +P. 1P ) .P. ( 1P +P. 1P ) ) ) )
19 mulclpr 
 |-  ( ( 1P e. P. /\ 1P e. P. ) -> ( 1P .P. 1P ) e. P. )
20 4 4 19 mp2an 
 |-  ( 1P .P. 1P ) e. P.
21 mulclpr 
 |-  ( ( ( 1P +P. 1P ) e. P. /\ ( 1P +P. 1P ) e. P. ) -> ( ( 1P +P. 1P ) .P. ( 1P +P. 1P ) ) e. P. )
22 6 6 21 mp2an 
 |-  ( ( 1P +P. 1P ) .P. ( 1P +P. 1P ) ) e. P.
23 addclpr 
 |-  ( ( ( 1P .P. 1P ) e. P. /\ ( ( 1P +P. 1P ) .P. ( 1P +P. 1P ) ) e. P. ) -> ( ( 1P .P. 1P ) +P. ( ( 1P +P. 1P ) .P. ( 1P +P. 1P ) ) ) e. P. )
24 20 22 23 mp2an 
 |-  ( ( 1P .P. 1P ) +P. ( ( 1P +P. 1P ) .P. ( 1P +P. 1P ) ) ) e. P.
25 mulclpr 
 |-  ( ( 1P e. P. /\ ( 1P +P. 1P ) e. P. ) -> ( 1P .P. ( 1P +P. 1P ) ) e. P. )
26 4 6 25 mp2an 
 |-  ( 1P .P. ( 1P +P. 1P ) ) e. P.
27 mulclpr 
 |-  ( ( ( 1P +P. 1P ) e. P. /\ 1P e. P. ) -> ( ( 1P +P. 1P ) .P. 1P ) e. P. )
28 6 4 27 mp2an 
 |-  ( ( 1P +P. 1P ) .P. 1P ) e. P.
29 addclpr 
 |-  ( ( ( 1P .P. ( 1P +P. 1P ) ) e. P. /\ ( ( 1P +P. 1P ) .P. 1P ) e. P. ) -> ( ( 1P .P. ( 1P +P. 1P ) ) +P. ( ( 1P +P. 1P ) .P. 1P ) ) e. P. )
30 26 28 29 mp2an 
 |-  ( ( 1P .P. ( 1P +P. 1P ) ) +P. ( ( 1P +P. 1P ) .P. 1P ) ) e. P.
31 enreceq 
 |-  ( ( ( ( 1P +P. 1P ) e. P. /\ 1P e. P. ) /\ ( ( ( 1P .P. 1P ) +P. ( ( 1P +P. 1P ) .P. ( 1P +P. 1P ) ) ) e. P. /\ ( ( 1P .P. ( 1P +P. 1P ) ) +P. ( ( 1P +P. 1P ) .P. 1P ) ) e. P. ) ) -> ( [ <. ( 1P +P. 1P ) , 1P >. ] ~R = [ <. ( ( 1P .P. 1P ) +P. ( ( 1P +P. 1P ) .P. ( 1P +P. 1P ) ) ) , ( ( 1P .P. ( 1P +P. 1P ) ) +P. ( ( 1P +P. 1P ) .P. 1P ) ) >. ] ~R <-> ( ( 1P +P. 1P ) +P. ( ( 1P .P. ( 1P +P. 1P ) ) +P. ( ( 1P +P. 1P ) .P. 1P ) ) ) = ( 1P +P. ( ( 1P .P. 1P ) +P. ( ( 1P +P. 1P ) .P. ( 1P +P. 1P ) ) ) ) ) )
32 6 4 24 30 31 mp4an 
 |-  ( [ <. ( 1P +P. 1P ) , 1P >. ] ~R = [ <. ( ( 1P .P. 1P ) +P. ( ( 1P +P. 1P ) .P. ( 1P +P. 1P ) ) ) , ( ( 1P .P. ( 1P +P. 1P ) ) +P. ( ( 1P +P. 1P ) .P. 1P ) ) >. ] ~R <-> ( ( 1P +P. 1P ) +P. ( ( 1P .P. ( 1P +P. 1P ) ) +P. ( ( 1P +P. 1P ) .P. 1P ) ) ) = ( 1P +P. ( ( 1P .P. 1P ) +P. ( ( 1P +P. 1P ) .P. ( 1P +P. 1P ) ) ) ) )
33 18 32 mpbir 
 |-  [ <. ( 1P +P. 1P ) , 1P >. ] ~R = [ <. ( ( 1P .P. 1P ) +P. ( ( 1P +P. 1P ) .P. ( 1P +P. 1P ) ) ) , ( ( 1P .P. ( 1P +P. 1P ) ) +P. ( ( 1P +P. 1P ) .P. 1P ) ) >. ] ~R
34 8 33 eqtr4i 
 |-  ( [ <. 1P , ( 1P +P. 1P ) >. ] ~R .R [ <. 1P , ( 1P +P. 1P ) >. ] ~R ) = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
35 3 34 eqtr4i 
 |-  1R = ( [ <. 1P , ( 1P +P. 1P ) >. ] ~R .R [ <. 1P , ( 1P +P. 1P ) >. ] ~R )
36 2 35 eqtr4i 
 |-  ( -1R .R -1R ) = 1R