Metamath Proof Explorer

Theorem mulsrpr

Description: Multiplication of signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995) (Revised by Mario Carneiro, 12-Aug-2015) (New usage is discouraged.)

Ref Expression
Assertion mulsrpr ⊢A∈𝑷∧B∈𝑷∧C∈𝑷∧D∈𝑷→AB~𝑹⋅𝑹CD~𝑹=A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹

Proof

Step Hyp Ref Expression
1 opelxpi ⊢A∈𝑷∧B∈𝑷→AB∈𝑷×𝑷
2 enrex ⊢~𝑹∈V
3 2 ecelqsi ⊢AB∈𝑷×𝑷→AB~𝑹∈𝑷×𝑷/~𝑹
4 1 3 syl ⊢A∈𝑷∧B∈𝑷→AB~𝑹∈𝑷×𝑷/~𝑹
5 opelxpi ⊢C∈𝑷∧D∈𝑷→CD∈𝑷×𝑷
6 2 ecelqsi ⊢CD∈𝑷×𝑷→CD~𝑹∈𝑷×𝑷/~𝑹
7 5 6 syl ⊢C∈𝑷∧D∈𝑷→CD~𝑹∈𝑷×𝑷/~𝑹
8 4 7 anim12i ⊢A∈𝑷∧B∈𝑷∧C∈𝑷∧D∈𝑷→AB~𝑹∈𝑷×𝑷/~𝑹∧CD~𝑹∈𝑷×𝑷/~𝑹
9 eqid ⊢AB~𝑹=AB~𝑹
10 eqid ⊢CD~𝑹=CD~𝑹
11 9 10 pm3.2i ⊢AB~𝑹=AB~𝑹∧CD~𝑹=CD~𝑹
12 eqid ⊢A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹=A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹
13 opeq12 ⊢w=A∧v=B→wv=AB
14 13 eceq1d ⊢w=A∧v=B→wv~𝑹=AB~𝑹
15 14 eqeq2d ⊢w=A∧v=B→AB~𝑹=wv~𝑹↔AB~𝑹=AB~𝑹
16 15 anbi1d ⊢w=A∧v=B→AB~𝑹=wv~𝑹∧CD~𝑹=CD~𝑹↔AB~𝑹=AB~𝑹∧CD~𝑹=CD~𝑹
17 simpl ⊢w=A∧v=B→w=A
18 17 oveq1d ⊢w=A∧v=B→w⋅𝑷C=A⋅𝑷C
19 simpr ⊢w=A∧v=B→v=B
20 19 oveq1d ⊢w=A∧v=B→v⋅𝑷D=B⋅𝑷D
21 18 20 oveq12d ⊢w=A∧v=B→w⋅𝑷C+𝑷v⋅𝑷D=A⋅𝑷C+𝑷B⋅𝑷D
22 17 oveq1d ⊢w=A∧v=B→w⋅𝑷D=A⋅𝑷D
23 19 oveq1d ⊢w=A∧v=B→v⋅𝑷C=B⋅𝑷C
24 22 23 oveq12d ⊢w=A∧v=B→w⋅𝑷D+𝑷v⋅𝑷C=A⋅𝑷D+𝑷B⋅𝑷C
25 21 24 opeq12d ⊢w=A∧v=B→w⋅𝑷C+𝑷v⋅𝑷Dw⋅𝑷D+𝑷v⋅𝑷C=A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C
26 25 eceq1d ⊢w=A∧v=B→w⋅𝑷C+𝑷v⋅𝑷Dw⋅𝑷D+𝑷v⋅𝑷C~𝑹=A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹
27 26 eqeq2d ⊢w=A∧v=B→A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹=w⋅𝑷C+𝑷v⋅𝑷Dw⋅𝑷D+𝑷v⋅𝑷C~𝑹↔A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹=A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹
28 16 27 anbi12d ⊢w=A∧v=B→AB~𝑹=wv~𝑹∧CD~𝑹=CD~𝑹∧A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹=w⋅𝑷C+𝑷v⋅𝑷Dw⋅𝑷D+𝑷v⋅𝑷C~𝑹↔AB~𝑹=AB~𝑹∧CD~𝑹=CD~𝑹∧A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹=A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹
29 28 spc2egv ⊢A∈𝑷∧B∈𝑷→AB~𝑹=AB~𝑹∧CD~𝑹=CD~𝑹∧A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹=A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹→∃w∃vAB~𝑹=wv~𝑹∧CD~𝑹=CD~𝑹∧A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹=w⋅𝑷C+𝑷v⋅𝑷Dw⋅𝑷D+𝑷v⋅𝑷C~𝑹
30 opeq12 ⊢u=C∧t=D→ut=CD
31 30 eceq1d ⊢u=C∧t=D→ut~𝑹=CD~𝑹
32 31 eqeq2d ⊢u=C∧t=D→CD~𝑹=ut~𝑹↔CD~𝑹=CD~𝑹
33 32 anbi2d ⊢u=C∧t=D→AB~𝑹=wv~𝑹∧CD~𝑹=ut~𝑹↔AB~𝑹=wv~𝑹∧CD~𝑹=CD~𝑹
34 simpl ⊢u=C∧t=D→u=C
35 34 oveq2d ⊢u=C∧t=D→w⋅𝑷u=w⋅𝑷C
36 simpr ⊢u=C∧t=D→t=D
37 36 oveq2d ⊢u=C∧t=D→v⋅𝑷t=v⋅𝑷D
38 35 37 oveq12d ⊢u=C∧t=D→w⋅𝑷u+𝑷v⋅𝑷t=w⋅𝑷C+𝑷v⋅𝑷D
39 36 oveq2d ⊢u=C∧t=D→w⋅𝑷t=w⋅𝑷D
40 34 oveq2d ⊢u=C∧t=D→v⋅𝑷u=v⋅𝑷C
41 39 40 oveq12d ⊢u=C∧t=D→w⋅𝑷t+𝑷v⋅𝑷u=w⋅𝑷D+𝑷v⋅𝑷C
42 38 41 opeq12d ⊢u=C∧t=D→w⋅𝑷u+𝑷v⋅𝑷tw⋅𝑷t+𝑷v⋅𝑷u=w⋅𝑷C+𝑷v⋅𝑷Dw⋅𝑷D+𝑷v⋅𝑷C
43 42 eceq1d ⊢u=C∧t=D→w⋅𝑷u+𝑷v⋅𝑷tw⋅𝑷t+𝑷v⋅𝑷u~𝑹=w⋅𝑷C+𝑷v⋅𝑷Dw⋅𝑷D+𝑷v⋅𝑷C~𝑹
44 43 eqeq2d ⊢u=C∧t=D→A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹=w⋅𝑷u+𝑷v⋅𝑷tw⋅𝑷t+𝑷v⋅𝑷u~𝑹↔A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹=w⋅𝑷C+𝑷v⋅𝑷Dw⋅𝑷D+𝑷v⋅𝑷C~𝑹
45 33 44 anbi12d ⊢u=C∧t=D→AB~𝑹=wv~𝑹∧CD~𝑹=ut~𝑹∧A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹=w⋅𝑷u+𝑷v⋅𝑷tw⋅𝑷t+𝑷v⋅𝑷u~𝑹↔AB~𝑹=wv~𝑹∧CD~𝑹=CD~𝑹∧A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹=w⋅𝑷C+𝑷v⋅𝑷Dw⋅𝑷D+𝑷v⋅𝑷C~𝑹
46 45 spc2egv ⊢C∈𝑷∧D∈𝑷→AB~𝑹=wv~𝑹∧CD~𝑹=CD~𝑹∧A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹=w⋅𝑷C+𝑷v⋅𝑷Dw⋅𝑷D+𝑷v⋅𝑷C~𝑹→∃u∃tAB~𝑹=wv~𝑹∧CD~𝑹=ut~𝑹∧A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹=w⋅𝑷u+𝑷v⋅𝑷tw⋅𝑷t+𝑷v⋅𝑷u~𝑹
47 46 2eximdv ⊢C∈𝑷∧D∈𝑷→∃w∃vAB~𝑹=wv~𝑹∧CD~𝑹=CD~𝑹∧A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹=w⋅𝑷C+𝑷v⋅𝑷Dw⋅𝑷D+𝑷v⋅𝑷C~𝑹→∃w∃v∃u∃tAB~𝑹=wv~𝑹∧CD~𝑹=ut~𝑹∧A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹=w⋅𝑷u+𝑷v⋅𝑷tw⋅𝑷t+𝑷v⋅𝑷u~𝑹
48 29 47 sylan9 ⊢A∈𝑷∧B∈𝑷∧C∈𝑷∧D∈𝑷→AB~𝑹=AB~𝑹∧CD~𝑹=CD~𝑹∧A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹=A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹→∃w∃v∃u∃tAB~𝑹=wv~𝑹∧CD~𝑹=ut~𝑹∧A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹=w⋅𝑷u+𝑷v⋅𝑷tw⋅𝑷t+𝑷v⋅𝑷u~𝑹
49 11 12 48 mp2ani ⊢A∈𝑷∧B∈𝑷∧C∈𝑷∧D∈𝑷→∃w∃v∃u∃tAB~𝑹=wv~𝑹∧CD~𝑹=ut~𝑹∧A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹=w⋅𝑷u+𝑷v⋅𝑷tw⋅𝑷t+𝑷v⋅𝑷u~𝑹
50 ecexg ⊢~𝑹∈V→A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹∈V
51 2 50 ax-mp ⊢A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹∈V
52 simp1 ⊢x=AB~𝑹∧y=CD~𝑹∧z=A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹→x=AB~𝑹
53 52 eqeq1d ⊢x=AB~𝑹∧y=CD~𝑹∧z=A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹→x=wv~𝑹↔AB~𝑹=wv~𝑹
54 simp2 ⊢x=AB~𝑹∧y=CD~𝑹∧z=A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹→y=CD~𝑹
55 54 eqeq1d ⊢x=AB~𝑹∧y=CD~𝑹∧z=A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹→y=ut~𝑹↔CD~𝑹=ut~𝑹
56 53 55 anbi12d ⊢x=AB~𝑹∧y=CD~𝑹∧z=A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹→x=wv~𝑹∧y=ut~𝑹↔AB~𝑹=wv~𝑹∧CD~𝑹=ut~𝑹
57 simp3 ⊢x=AB~𝑹∧y=CD~𝑹∧z=A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹→z=A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹
58 57 eqeq1d ⊢x=AB~𝑹∧y=CD~𝑹∧z=A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹→z=w⋅𝑷u+𝑷v⋅𝑷tw⋅𝑷t+𝑷v⋅𝑷u~𝑹↔A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹=w⋅𝑷u+𝑷v⋅𝑷tw⋅𝑷t+𝑷v⋅𝑷u~𝑹
59 56 58 anbi12d ⊢x=AB~𝑹∧y=CD~𝑹∧z=A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹→x=wv~𝑹∧y=ut~𝑹∧z=w⋅𝑷u+𝑷v⋅𝑷tw⋅𝑷t+𝑷v⋅𝑷u~𝑹↔AB~𝑹=wv~𝑹∧CD~𝑹=ut~𝑹∧A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹=w⋅𝑷u+𝑷v⋅𝑷tw⋅𝑷t+𝑷v⋅𝑷u~𝑹
60 59 4exbidv ⊢x=AB~𝑹∧y=CD~𝑹∧z=A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹→∃w∃v∃u∃tx=wv~𝑹∧y=ut~𝑹∧z=w⋅𝑷u+𝑷v⋅𝑷tw⋅𝑷t+𝑷v⋅𝑷u~𝑹↔∃w∃v∃u∃tAB~𝑹=wv~𝑹∧CD~𝑹=ut~𝑹∧A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹=w⋅𝑷u+𝑷v⋅𝑷tw⋅𝑷t+𝑷v⋅𝑷u~𝑹
61 mulsrmo ⊢x∈𝑷×𝑷/~𝑹∧y∈𝑷×𝑷/~𝑹→∃*z∃w∃v∃u∃tx=wv~𝑹∧y=ut~𝑹∧z=w⋅𝑷u+𝑷v⋅𝑷tw⋅𝑷t+𝑷v⋅𝑷u~𝑹
62 df-mr ⊢⋅𝑹=xyz|x∈𝑹∧y∈𝑹∧∃w∃v∃u∃tx=wv~𝑹∧y=ut~𝑹∧z=w⋅𝑷u+𝑷v⋅𝑷tw⋅𝑷t+𝑷v⋅𝑷u~𝑹
63 df-nr ⊢𝑹=𝑷×𝑷/~𝑹
64 63 eleq2i ⊢x∈𝑹↔x∈𝑷×𝑷/~𝑹
65 63 eleq2i ⊢y∈𝑹↔y∈𝑷×𝑷/~𝑹
66 64 65 anbi12i ⊢x∈𝑹∧y∈𝑹↔x∈𝑷×𝑷/~𝑹∧y∈𝑷×𝑷/~𝑹
67 66 anbi1i ⊢x∈𝑹∧y∈𝑹∧∃w∃v∃u∃tx=wv~𝑹∧y=ut~𝑹∧z=w⋅𝑷u+𝑷v⋅𝑷tw⋅𝑷t+𝑷v⋅𝑷u~𝑹↔x∈𝑷×𝑷/~𝑹∧y∈𝑷×𝑷/~𝑹∧∃w∃v∃u∃tx=wv~𝑹∧y=ut~𝑹∧z=w⋅𝑷u+𝑷v⋅𝑷tw⋅𝑷t+𝑷v⋅𝑷u~𝑹
68 67 oprabbii ⊢xyz|x∈𝑹∧y∈𝑹∧∃w∃v∃u∃tx=wv~𝑹∧y=ut~𝑹∧z=w⋅𝑷u+𝑷v⋅𝑷tw⋅𝑷t+𝑷v⋅𝑷u~𝑹=xyz|x∈𝑷×𝑷/~𝑹∧y∈𝑷×𝑷/~𝑹∧∃w∃v∃u∃tx=wv~𝑹∧y=ut~𝑹∧z=w⋅𝑷u+𝑷v⋅𝑷tw⋅𝑷t+𝑷v⋅𝑷u~𝑹
69 62 68 eqtri ⊢⋅𝑹=xyz|x∈𝑷×𝑷/~𝑹∧y∈𝑷×𝑷/~𝑹∧∃w∃v∃u∃tx=wv~𝑹∧y=ut~𝑹∧z=w⋅𝑷u+𝑷v⋅𝑷tw⋅𝑷t+𝑷v⋅𝑷u~𝑹
70 60 61 69 ovig ⊢AB~𝑹∈𝑷×𝑷/~𝑹∧CD~𝑹∈𝑷×𝑷/~𝑹∧A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹∈V→∃w∃v∃u∃tAB~𝑹=wv~𝑹∧CD~𝑹=ut~𝑹∧A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹=w⋅𝑷u+𝑷v⋅𝑷tw⋅𝑷t+𝑷v⋅𝑷u~𝑹→AB~𝑹⋅𝑹CD~𝑹=A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹
71 51 70 mp3an3 ⊢AB~𝑹∈𝑷×𝑷/~𝑹∧CD~𝑹∈𝑷×𝑷/~𝑹→∃w∃v∃u∃tAB~𝑹=wv~𝑹∧CD~𝑹=ut~𝑹∧A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹=w⋅𝑷u+𝑷v⋅𝑷tw⋅𝑷t+𝑷v⋅𝑷u~𝑹→AB~𝑹⋅𝑹CD~𝑹=A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹
72 8 49 71 sylc ⊢A∈𝑷∧B∈𝑷∧C∈𝑷∧D∈𝑷→AB~𝑹⋅𝑹CD~𝑹=A⋅𝑷C+𝑷B⋅𝑷DA⋅𝑷D+𝑷B⋅𝑷C~𝑹