Metamath Proof Explorer

Theorem mulcnsr

Description: Multiplication of complex numbers in terms of signed reals. (Contributed by NM, 9-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion mulcnsr ⊢A∈𝑹∧B∈𝑹∧C∈𝑹∧D∈𝑹→AB⁢CD=A⋅𝑹C+𝑹-1𝑹⋅𝑹B⋅𝑹DB⋅𝑹C+𝑹A⋅𝑹D

Proof

Step Hyp Ref Expression
1 opex ⊢A⋅𝑹C+𝑹-1𝑹⋅𝑹B⋅𝑹DB⋅𝑹C+𝑹A⋅𝑹D∈V
2 oveq1 ⊢w=A→w⋅𝑹u=A⋅𝑹u
3 oveq1 ⊢v=B→v⋅𝑹f=B⋅𝑹f
4 3 oveq2d ⊢v=B→-1𝑹⋅𝑹v⋅𝑹f=-1𝑹⋅𝑹B⋅𝑹f
5 2 4 oveqan12d ⊢w=A∧v=B→w⋅𝑹u+𝑹-1𝑹⋅𝑹v⋅𝑹f=A⋅𝑹u+𝑹-1𝑹⋅𝑹B⋅𝑹f
6 oveq1 ⊢v=B→v⋅𝑹u=B⋅𝑹u
7 oveq1 ⊢w=A→w⋅𝑹f=A⋅𝑹f
8 6 7 oveqan12rd ⊢w=A∧v=B→v⋅𝑹u+𝑹w⋅𝑹f=B⋅𝑹u+𝑹A⋅𝑹f
9 5 8 opeq12d ⊢w=A∧v=B→w⋅𝑹u+𝑹-1𝑹⋅𝑹v⋅𝑹fv⋅𝑹u+𝑹w⋅𝑹f=A⋅𝑹u+𝑹-1𝑹⋅𝑹B⋅𝑹fB⋅𝑹u+𝑹A⋅𝑹f
10 oveq2 ⊢u=C→A⋅𝑹u=A⋅𝑹C
11 oveq2 ⊢f=D→B⋅𝑹f=B⋅𝑹D
12 11 oveq2d ⊢f=D→-1𝑹⋅𝑹B⋅𝑹f=-1𝑹⋅𝑹B⋅𝑹D
13 10 12 oveqan12d ⊢u=C∧f=D→A⋅𝑹u+𝑹-1𝑹⋅𝑹B⋅𝑹f=A⋅𝑹C+𝑹-1𝑹⋅𝑹B⋅𝑹D
14 oveq2 ⊢u=C→B⋅𝑹u=B⋅𝑹C
15 oveq2 ⊢f=D→A⋅𝑹f=A⋅𝑹D
16 14 15 oveqan12d ⊢u=C∧f=D→B⋅𝑹u+𝑹A⋅𝑹f=B⋅𝑹C+𝑹A⋅𝑹D
17 13 16 opeq12d ⊢u=C∧f=D→A⋅𝑹u+𝑹-1𝑹⋅𝑹B⋅𝑹fB⋅𝑹u+𝑹A⋅𝑹f=A⋅𝑹C+𝑹-1𝑹⋅𝑹B⋅𝑹DB⋅𝑹C+𝑹A⋅𝑹D
18 9 17 sylan9eq ⊢w=A∧v=B∧u=C∧f=D→w⋅𝑹u+𝑹-1𝑹⋅𝑹v⋅𝑹fv⋅𝑹u+𝑹w⋅𝑹f=A⋅𝑹C+𝑹-1𝑹⋅𝑹B⋅𝑹DB⋅𝑹C+𝑹A⋅𝑹D
19 df-mul ⊢×=xyz|x∈ℂ∧y∈ℂ∧∃w∃v∃u∃fx=wv∧y=uf∧z=w⋅𝑹u+𝑹-1𝑹⋅𝑹v⋅𝑹fv⋅𝑹u+𝑹w⋅𝑹f
20 df-c ⊢ℂ=𝑹×𝑹
21 20 eleq2i ⊢x∈ℂ↔x∈𝑹×𝑹
22 20 eleq2i ⊢y∈ℂ↔y∈𝑹×𝑹
23 21 22 anbi12i ⊢x∈ℂ∧y∈ℂ↔x∈𝑹×𝑹∧y∈𝑹×𝑹
24 23 anbi1i ⊢x∈ℂ∧y∈ℂ∧∃w∃v∃u∃fx=wv∧y=uf∧z=w⋅𝑹u+𝑹-1𝑹⋅𝑹v⋅𝑹fv⋅𝑹u+𝑹w⋅𝑹f↔x∈𝑹×𝑹∧y∈𝑹×𝑹∧∃w∃v∃u∃fx=wv∧y=uf∧z=w⋅𝑹u+𝑹-1𝑹⋅𝑹v⋅𝑹fv⋅𝑹u+𝑹w⋅𝑹f
25 24 oprabbii ⊢xyz|x∈ℂ∧y∈ℂ∧∃w∃v∃u∃fx=wv∧y=uf∧z=w⋅𝑹u+𝑹-1𝑹⋅𝑹v⋅𝑹fv⋅𝑹u+𝑹w⋅𝑹f=xyz|x∈𝑹×𝑹∧y∈𝑹×𝑹∧∃w∃v∃u∃fx=wv∧y=uf∧z=w⋅𝑹u+𝑹-1𝑹⋅𝑹v⋅𝑹fv⋅𝑹u+𝑹w⋅𝑹f
26 19 25 eqtri ⊢×=xyz|x∈𝑹×𝑹∧y∈𝑹×𝑹∧∃w∃v∃u∃fx=wv∧y=uf∧z=w⋅𝑹u+𝑹-1𝑹⋅𝑹v⋅𝑹fv⋅𝑹u+𝑹w⋅𝑹f
27 1 18 26 ov3 ⊢A∈𝑹∧B∈𝑹∧C∈𝑹∧D∈𝑹→AB⁢CD=A⋅𝑹C+𝑹-1𝑹⋅𝑹B⋅𝑹DB⋅𝑹C+𝑹A⋅𝑹D