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 ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( ⟨ 𝐴 , 0R ⟩ · ⟨ 𝐵 , 0R ⟩ ) = ⟨ ( 𝐴 ·R 𝐵 ) , 0R ⟩ )

Proof

Step Hyp Ref Expression
1 0r ⊢ 0R ∈ R
2 mulcnsr ⊢ ( ( ( 𝐴 ∈ R ∧ 0R ∈ R ) ∧ ( 𝐵 ∈ R ∧ 0R ∈ R ) ) → ( ⟨ 𝐴 , 0R ⟩ · ⟨ 𝐵 , 0R ⟩ ) = ⟨ ( ( 𝐴 ·R 𝐵 ) +R ( -1R ·R ( 0R ·R 0R ) ) ) , ( ( 0R ·R 𝐵 ) +R ( 𝐴 ·R 0R ) ) ⟩ )
3 2 an4s ⊢ ( ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) ∧ ( 0R ∈ R ∧ 0R ∈ R ) ) → ( ⟨ 𝐴 , 0R ⟩ · ⟨ 𝐵 , 0R ⟩ ) = ⟨ ( ( 𝐴 ·R 𝐵 ) +R ( -1R ·R ( 0R ·R 0R ) ) ) , ( ( 0R ·R 𝐵 ) +R ( 𝐴 ·R 0R ) ) ⟩ )
4 1 1 3 mpanr12 ⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( ⟨ 𝐴 , 0R ⟩ · ⟨ 𝐵 , 0R ⟩ ) = ⟨ ( ( 𝐴 ·R 𝐵 ) +R ( -1R ·R ( 0R ·R 0R ) ) ) , ( ( 0R ·R 𝐵 ) +R ( 𝐴 ·R 0R ) ) ⟩ )
5 00sr ⊢ ( 0R ∈ 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 ∈ R
9 00sr ⊢ ( -1R ∈ 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 ⊢ ( ( 𝐴 ·R 𝐵 ) +R ( -1R ·R ( 0R ·R 0R ) ) ) = ( ( 𝐴 ·R 𝐵 ) +R 0R )
13 mulclsr ⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( 𝐴 ·R 𝐵 ) ∈ R )
14 0idsr ⊢ ( ( 𝐴 ·R 𝐵 ) ∈ R → ( ( 𝐴 ·R 𝐵 ) +R 0R ) = ( 𝐴 ·R 𝐵 ) )
15 13 14 syl ⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( ( 𝐴 ·R 𝐵 ) +R 0R ) = ( 𝐴 ·R 𝐵 ) )
16 12 15 syl5eq ⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( ( 𝐴 ·R 𝐵 ) +R ( -1R ·R ( 0R ·R 0R ) ) ) = ( 𝐴 ·R 𝐵 ) )
17 mulcomsr ⊢ ( 0R ·R 𝐵 ) = ( 𝐵 ·R 0R )
18 00sr ⊢ ( 𝐵 ∈ R → ( 𝐵 ·R 0R ) = 0R )
19 17 18 syl5eq ⊢ ( 𝐵 ∈ R → ( 0R ·R 𝐵 ) = 0R )
20 00sr ⊢ ( 𝐴 ∈ R → ( 𝐴 ·R 0R ) = 0R )
21 19 20 oveqan12rd ⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( ( 0R ·R 𝐵 ) +R ( 𝐴 ·R 0R ) ) = ( 0R +R 0R ) )
22 0idsr ⊢ ( 0R ∈ R → ( 0R +R 0R ) = 0R )
23 1 22 ax-mp ⊢ ( 0R +R 0R ) = 0R
24 21 23 syl6eq ⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( ( 0R ·R 𝐵 ) +R ( 𝐴 ·R 0R ) ) = 0R )
25 16 24 opeq12d ⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ⟨ ( ( 𝐴 ·R 𝐵 ) +R ( -1R ·R ( 0R ·R 0R ) ) ) , ( ( 0R ·R 𝐵 ) +R ( 𝐴 ·R 0R ) ) ⟩ = ⟨ ( 𝐴 ·R 𝐵 ) , 0R ⟩ )
26 4 25 eqtrd ⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( ⟨ 𝐴 , 0R ⟩ · ⟨ 𝐵 , 0R ⟩ ) = ⟨ ( 𝐴 ·R 𝐵 ) , 0R ⟩ )