Metamath Proof Explorer

Theorem distrsr

Description: Multiplication of signed reals is distributive. (Contributed by NM, 2-Sep-1995) (Revised by Mario Carneiro, 28-Apr-2015) (New usage is discouraged.)

Ref Expression
Assertion distrsr ⊢A⋅𝑹B+𝑹C=A⋅𝑹B+𝑹A⋅𝑹C

Proof

Step Hyp Ref Expression
1 df-nr ⊢𝑹=𝑷×𝑷/~𝑹
2 addsrpr ⊢z∈𝑷∧w∈𝑷∧v∈𝑷∧u∈𝑷→zw~𝑹+𝑹vu~𝑹=z+𝑷vw+𝑷u~𝑹
3 mulsrpr ⊢x∈𝑷∧y∈𝑷∧z+𝑷v∈𝑷∧w+𝑷u∈𝑷→xy~𝑹⋅𝑹z+𝑷vw+𝑷u~𝑹=x⋅𝑷z+𝑷v+𝑷y⋅𝑷w+𝑷ux⋅𝑷w+𝑷u+𝑷y⋅𝑷z+𝑷v~𝑹
4 mulsrpr ⊢x∈𝑷∧y∈𝑷∧z∈𝑷∧w∈𝑷→xy~𝑹⋅𝑹zw~𝑹=x⋅𝑷z+𝑷y⋅𝑷wx⋅𝑷w+𝑷y⋅𝑷z~𝑹
5 mulsrpr ⊢x∈𝑷∧y∈𝑷∧v∈𝑷∧u∈𝑷→xy~𝑹⋅𝑹vu~𝑹=x⋅𝑷v+𝑷y⋅𝑷ux⋅𝑷u+𝑷y⋅𝑷v~𝑹
6 addsrpr ⊢x⋅𝑷z+𝑷y⋅𝑷w∈𝑷∧x⋅𝑷w+𝑷y⋅𝑷z∈𝑷∧x⋅𝑷v+𝑷y⋅𝑷u∈𝑷∧x⋅𝑷u+𝑷y⋅𝑷v∈𝑷→x⋅𝑷z+𝑷y⋅𝑷wx⋅𝑷w+𝑷y⋅𝑷z~𝑹+𝑹x⋅𝑷v+𝑷y⋅𝑷ux⋅𝑷u+𝑷y⋅𝑷v~𝑹=x⋅𝑷z+𝑷y⋅𝑷w+𝑷x⋅𝑷v+𝑷y⋅𝑷ux⋅𝑷w+𝑷y⋅𝑷z+𝑷x⋅𝑷u+𝑷y⋅𝑷v~𝑹
7 addclpr ⊢z∈𝑷∧v∈𝑷→z+𝑷v∈𝑷
8 addclpr ⊢w∈𝑷∧u∈𝑷→w+𝑷u∈𝑷
9 7 8 anim12i ⊢z∈𝑷∧v∈𝑷∧w∈𝑷∧u∈𝑷→z+𝑷v∈𝑷∧w+𝑷u∈𝑷
10 9 an4s ⊢z∈𝑷∧w∈𝑷∧v∈𝑷∧u∈𝑷→z+𝑷v∈𝑷∧w+𝑷u∈𝑷
11 mulclpr ⊢x∈𝑷∧z∈𝑷→x⋅𝑷z∈𝑷
12 mulclpr ⊢y∈𝑷∧w∈𝑷→y⋅𝑷w∈𝑷
13 addclpr ⊢x⋅𝑷z∈𝑷∧y⋅𝑷w∈𝑷→x⋅𝑷z+𝑷y⋅𝑷w∈𝑷
14 11 12 13 syl2an ⊢x∈𝑷∧z∈𝑷∧y∈𝑷∧w∈𝑷→x⋅𝑷z+𝑷y⋅𝑷w∈𝑷
15 14 an4s ⊢x∈𝑷∧y∈𝑷∧z∈𝑷∧w∈𝑷→x⋅𝑷z+𝑷y⋅𝑷w∈𝑷
16 mulclpr ⊢x∈𝑷∧w∈𝑷→x⋅𝑷w∈𝑷
17 mulclpr ⊢y∈𝑷∧z∈𝑷→y⋅𝑷z∈𝑷
18 addclpr ⊢x⋅𝑷w∈𝑷∧y⋅𝑷z∈𝑷→x⋅𝑷w+𝑷y⋅𝑷z∈𝑷
19 16 17 18 syl2an ⊢x∈𝑷∧w∈𝑷∧y∈𝑷∧z∈𝑷→x⋅𝑷w+𝑷y⋅𝑷z∈𝑷
20 19 an42s ⊢x∈𝑷∧y∈𝑷∧z∈𝑷∧w∈𝑷→x⋅𝑷w+𝑷y⋅𝑷z∈𝑷
21 15 20 jca ⊢x∈𝑷∧y∈𝑷∧z∈𝑷∧w∈𝑷→x⋅𝑷z+𝑷y⋅𝑷w∈𝑷∧x⋅𝑷w+𝑷y⋅𝑷z∈𝑷
22 mulclpr ⊢x∈𝑷∧v∈𝑷→x⋅𝑷v∈𝑷
23 mulclpr ⊢y∈𝑷∧u∈𝑷→y⋅𝑷u∈𝑷
24 addclpr ⊢x⋅𝑷v∈𝑷∧y⋅𝑷u∈𝑷→x⋅𝑷v+𝑷y⋅𝑷u∈𝑷
25 22 23 24 syl2an ⊢x∈𝑷∧v∈𝑷∧y∈𝑷∧u∈𝑷→x⋅𝑷v+𝑷y⋅𝑷u∈𝑷
26 25 an4s ⊢x∈𝑷∧y∈𝑷∧v∈𝑷∧u∈𝑷→x⋅𝑷v+𝑷y⋅𝑷u∈𝑷
27 mulclpr ⊢x∈𝑷∧u∈𝑷→x⋅𝑷u∈𝑷
28 mulclpr ⊢y∈𝑷∧v∈𝑷→y⋅𝑷v∈𝑷
29 addclpr ⊢x⋅𝑷u∈𝑷∧y⋅𝑷v∈𝑷→x⋅𝑷u+𝑷y⋅𝑷v∈𝑷
30 27 28 29 syl2an ⊢x∈𝑷∧u∈𝑷∧y∈𝑷∧v∈𝑷→x⋅𝑷u+𝑷y⋅𝑷v∈𝑷
31 30 an42s ⊢x∈𝑷∧y∈𝑷∧v∈𝑷∧u∈𝑷→x⋅𝑷u+𝑷y⋅𝑷v∈𝑷
32 26 31 jca ⊢x∈𝑷∧y∈𝑷∧v∈𝑷∧u∈𝑷→x⋅𝑷v+𝑷y⋅𝑷u∈𝑷∧x⋅𝑷u+𝑷y⋅𝑷v∈𝑷
33 distrpr ⊢x⋅𝑷z+𝑷v=x⋅𝑷z+𝑷x⋅𝑷v
34 distrpr ⊢y⋅𝑷w+𝑷u=y⋅𝑷w+𝑷y⋅𝑷u
35 33 34 oveq12i ⊢x⋅𝑷z+𝑷v+𝑷y⋅𝑷w+𝑷u=x⋅𝑷z+𝑷x⋅𝑷v+𝑷y⋅𝑷w+𝑷y⋅𝑷u
36 ovex ⊢x⋅𝑷z∈V
37 ovex ⊢x⋅𝑷v∈V
38 ovex ⊢y⋅𝑷w∈V
39 addcompr ⊢f+𝑷g=g+𝑷f
40 addasspr ⊢f+𝑷g+𝑷h=f+𝑷g+𝑷h
41 ovex ⊢y⋅𝑷u∈V
42 36 37 38 39 40 41 caov4 ⊢x⋅𝑷z+𝑷x⋅𝑷v+𝑷y⋅𝑷w+𝑷y⋅𝑷u=x⋅𝑷z+𝑷y⋅𝑷w+𝑷x⋅𝑷v+𝑷y⋅𝑷u
43 35 42 eqtri ⊢x⋅𝑷z+𝑷v+𝑷y⋅𝑷w+𝑷u=x⋅𝑷z+𝑷y⋅𝑷w+𝑷x⋅𝑷v+𝑷y⋅𝑷u
44 distrpr ⊢x⋅𝑷w+𝑷u=x⋅𝑷w+𝑷x⋅𝑷u
45 distrpr ⊢y⋅𝑷z+𝑷v=y⋅𝑷z+𝑷y⋅𝑷v
46 44 45 oveq12i ⊢x⋅𝑷w+𝑷u+𝑷y⋅𝑷z+𝑷v=x⋅𝑷w+𝑷x⋅𝑷u+𝑷y⋅𝑷z+𝑷y⋅𝑷v
47 ovex ⊢x⋅𝑷w∈V
48 ovex ⊢x⋅𝑷u∈V
49 ovex ⊢y⋅𝑷z∈V
50 ovex ⊢y⋅𝑷v∈V
51 47 48 49 39 40 50 caov4 ⊢x⋅𝑷w+𝑷x⋅𝑷u+𝑷y⋅𝑷z+𝑷y⋅𝑷v=x⋅𝑷w+𝑷y⋅𝑷z+𝑷x⋅𝑷u+𝑷y⋅𝑷v
52 46 51 eqtri ⊢x⋅𝑷w+𝑷u+𝑷y⋅𝑷z+𝑷v=x⋅𝑷w+𝑷y⋅𝑷z+𝑷x⋅𝑷u+𝑷y⋅𝑷v
53 1 2 3 4 5 6 10 21 32 43 52 ecovdi ⊢A∈𝑹∧B∈𝑹∧C∈𝑹→A⋅𝑹B+𝑹C=A⋅𝑹B+𝑹A⋅𝑹C
54 dmaddsr ⊢dom⁡+𝑹=𝑹×𝑹
55 0nsr ⊢¬∅∈𝑹
56 dmmulsr ⊢dom⁡⋅𝑹=𝑹×𝑹
57 54 55 56 ndmovdistr ⊢¬A∈𝑹∧B∈𝑹∧C∈𝑹→A⋅𝑹B+𝑹C=A⋅𝑹B+𝑹A⋅𝑹C
58 53 57 pm2.61i ⊢A⋅𝑹B+𝑹C=A⋅𝑹B+𝑹A⋅𝑹C