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 ∈ P
5 addclpr ⊢ ( ( 1P ∈ P ∧ 1P ∈ P ) → ( 1P +P 1P ) ∈ P )
6 4 4 5 mp2an ⊢ ( 1P +P 1P ) ∈ P
7 mulsrpr ⊢ ( ( ( 1P ∈ P ∧ ( 1P +P 1P ) ∈ P ) ∧ ( 1P ∈ P ∧ ( 1P +P 1P ) ∈ 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 ∈ 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 ∈ P ∧ 1P ∈ P ) → ( 1P ·P 1P ) ∈ P )
20 4 4 19 mp2an ⊢ ( 1P ·P 1P ) ∈ P
21 mulclpr ⊢ ( ( ( 1P +P 1P ) ∈ P ∧ ( 1P +P 1P ) ∈ P ) → ( ( 1P +P 1P ) ·P ( 1P +P 1P ) ) ∈ P )
22 6 6 21 mp2an ⊢ ( ( 1P +P 1P ) ·P ( 1P +P 1P ) ) ∈ P
23 addclpr ⊢ ( ( ( 1P ·P 1P ) ∈ P ∧ ( ( 1P +P 1P ) ·P ( 1P +P 1P ) ) ∈ P ) → ( ( 1P ·P 1P ) +P ( ( 1P +P 1P ) ·P ( 1P +P 1P ) ) ) ∈ P )
24 20 22 23 mp2an ⊢ ( ( 1P ·P 1P ) +P ( ( 1P +P 1P ) ·P ( 1P +P 1P ) ) ) ∈ P
25 mulclpr ⊢ ( ( 1P ∈ P ∧ ( 1P +P 1P ) ∈ P ) → ( 1P ·P ( 1P +P 1P ) ) ∈ P )
26 4 6 25 mp2an ⊢ ( 1P ·P ( 1P +P 1P ) ) ∈ P
27 mulclpr ⊢ ( ( ( 1P +P 1P ) ∈ P ∧ 1P ∈ P ) → ( ( 1P +P 1P ) ·P 1P ) ∈ P )
28 6 4 27 mp2an ⊢ ( ( 1P +P 1P ) ·P 1P ) ∈ P
29 addclpr ⊢ ( ( ( 1P ·P ( 1P +P 1P ) ) ∈ P ∧ ( ( 1P +P 1P ) ·P 1P ) ∈ P ) → ( ( 1P ·P ( 1P +P 1P ) ) +P ( ( 1P +P 1P ) ·P 1P ) ) ∈ P )
30 26 28 29 mp2an ⊢ ( ( 1P ·P ( 1P +P 1P ) ) +P ( ( 1P +P 1P ) ·P 1P ) ) ∈ P
31 enreceq ⊢ ( ( ( ( 1P +P 1P ) ∈ P ∧ 1P ∈ P ) ∧ ( ( ( 1P ·P 1P ) +P ( ( 1P +P 1P ) ·P ( 1P +P 1P ) ) ) ∈ P ∧ ( ( 1P ·P ( 1P +P 1P ) ) +P ( ( 1P +P 1P ) ·P 1P ) ) ∈ 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