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 ( 𝐴 ·R ( 𝐵 +R 𝐶 ) ) = ( ( 𝐴 ·R 𝐵 ) +R ( 𝐴 ·R 𝐶 ) )

Proof

Step Hyp Ref Expression
1 df-nr ⊢ R = ( ( P × P ) / ~R )
2 addsrpr ⊢ ( ( ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ∧ ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ) → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R +R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) = [ ⟨ ( 𝑧 +P 𝑣 ) , ( 𝑤 +P 𝑢 ) ⟩ ] ~R )
3 mulsrpr ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( ( 𝑧 +P 𝑣 ) ∈ P ∧ ( 𝑤 +P 𝑢 ) ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ ( 𝑧 +P 𝑣 ) , ( 𝑤 +P 𝑢 ) ⟩ ] ~R ) = [ ⟨ ( ( 𝑥 ·P ( 𝑧 +P 𝑣 ) ) +P ( 𝑦 ·P ( 𝑤 +P 𝑢 ) ) ) , ( ( 𝑥 ·P ( 𝑤 +P 𝑢 ) ) +P ( 𝑦 ·P ( 𝑧 +P 𝑣 ) ) ) ⟩ ] ~R )
4 mulsrpr ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) = [ ⟨ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) , ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ⟩ ] ~R )
5 mulsrpr ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) = [ ⟨ ( ( 𝑥 ·P 𝑣 ) +P ( 𝑦 ·P 𝑢 ) ) , ( ( 𝑥 ·P 𝑢 ) +P ( 𝑦 ·P 𝑣 ) ) ⟩ ] ~R )
6 addsrpr ⊢ ( ( ( ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P ∧ ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ∈ P ) ∧ ( ( ( 𝑥 ·P 𝑣 ) +P ( 𝑦 ·P 𝑢 ) ) ∈ P ∧ ( ( 𝑥 ·P 𝑢 ) +P ( 𝑦 ·P 𝑣 ) ) ∈ P ) ) → ( [ ⟨ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) , ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ⟩ ] ~R +R [ ⟨ ( ( 𝑥 ·P 𝑣 ) +P ( 𝑦 ·P 𝑢 ) ) , ( ( 𝑥 ·P 𝑢 ) +P ( 𝑦 ·P 𝑣 ) ) ⟩ ] ~R ) = [ ⟨ ( ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) +P ( ( 𝑥 ·P 𝑣 ) +P ( 𝑦 ·P 𝑢 ) ) ) , ( ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) +P ( ( 𝑥 ·P 𝑢 ) +P ( 𝑦 ·P 𝑣 ) ) ) ⟩ ] ~R )
7 addclpr ⊢ ( ( 𝑧 ∈ P ∧ 𝑣 ∈ P ) → ( 𝑧 +P 𝑣 ) ∈ P )
8 addclpr ⊢ ( ( 𝑤 ∈ P ∧ 𝑢 ∈ P ) → ( 𝑤 +P 𝑢 ) ∈ P )
9 7 8 anim12i ⊢ ( ( ( 𝑧 ∈ P ∧ 𝑣 ∈ P ) ∧ ( 𝑤 ∈ P ∧ 𝑢 ∈ P ) ) → ( ( 𝑧 +P 𝑣 ) ∈ P ∧ ( 𝑤 +P 𝑢 ) ∈ P ) )
10 9 an4s ⊢ ( ( ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ∧ ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ) → ( ( 𝑧 +P 𝑣 ) ∈ P ∧ ( 𝑤 +P 𝑢 ) ∈ P ) )
11 mulclpr ⊢ ( ( 𝑥 ∈ P ∧ 𝑧 ∈ P ) → ( 𝑥 ·P 𝑧 ) ∈ P )
12 mulclpr ⊢ ( ( 𝑦 ∈ P ∧ 𝑤 ∈ P ) → ( 𝑦 ·P 𝑤 ) ∈ P )
13 addclpr ⊢ ( ( ( 𝑥 ·P 𝑧 ) ∈ P ∧ ( 𝑦 ·P 𝑤 ) ∈ P ) → ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P )
14 11 12 13 syl2an ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑧 ∈ P ) ∧ ( 𝑦 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P )
15 14 an4s ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P )
16 mulclpr ⊢ ( ( 𝑥 ∈ P ∧ 𝑤 ∈ P ) → ( 𝑥 ·P 𝑤 ) ∈ P )
17 mulclpr ⊢ ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( 𝑦 ·P 𝑧 ) ∈ P )
18 addclpr ⊢ ( ( ( 𝑥 ·P 𝑤 ) ∈ P ∧ ( 𝑦 ·P 𝑧 ) ∈ P ) → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ∈ P )
19 16 17 18 syl2an ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑤 ∈ P ) ∧ ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ) → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ∈ P )
20 19 an42s ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ∈ P )
21 15 20 jca ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P ∧ ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ∈ P ) )
22 mulclpr ⊢ ( ( 𝑥 ∈ P ∧ 𝑣 ∈ P ) → ( 𝑥 ·P 𝑣 ) ∈ P )
23 mulclpr ⊢ ( ( 𝑦 ∈ P ∧ 𝑢 ∈ P ) → ( 𝑦 ·P 𝑢 ) ∈ P )
24 addclpr ⊢ ( ( ( 𝑥 ·P 𝑣 ) ∈ P ∧ ( 𝑦 ·P 𝑢 ) ∈ P ) → ( ( 𝑥 ·P 𝑣 ) +P ( 𝑦 ·P 𝑢 ) ) ∈ P )
25 22 23 24 syl2an ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑣 ∈ P ) ∧ ( 𝑦 ∈ P ∧ 𝑢 ∈ P ) ) → ( ( 𝑥 ·P 𝑣 ) +P ( 𝑦 ·P 𝑢 ) ) ∈ P )
26 25 an4s ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ) → ( ( 𝑥 ·P 𝑣 ) +P ( 𝑦 ·P 𝑢 ) ) ∈ P )
27 mulclpr ⊢ ( ( 𝑥 ∈ P ∧ 𝑢 ∈ P ) → ( 𝑥 ·P 𝑢 ) ∈ P )
28 mulclpr ⊢ ( ( 𝑦 ∈ P ∧ 𝑣 ∈ P ) → ( 𝑦 ·P 𝑣 ) ∈ P )
29 addclpr ⊢ ( ( ( 𝑥 ·P 𝑢 ) ∈ P ∧ ( 𝑦 ·P 𝑣 ) ∈ P ) → ( ( 𝑥 ·P 𝑢 ) +P ( 𝑦 ·P 𝑣 ) ) ∈ P )
30 27 28 29 syl2an ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑢 ∈ P ) ∧ ( 𝑦 ∈ P ∧ 𝑣 ∈ P ) ) → ( ( 𝑥 ·P 𝑢 ) +P ( 𝑦 ·P 𝑣 ) ) ∈ P )
31 30 an42s ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ) → ( ( 𝑥 ·P 𝑢 ) +P ( 𝑦 ·P 𝑣 ) ) ∈ P )
32 26 31 jca ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ) → ( ( ( 𝑥 ·P 𝑣 ) +P ( 𝑦 ·P 𝑢 ) ) ∈ P ∧ ( ( 𝑥 ·P 𝑢 ) +P ( 𝑦 ·P 𝑣 ) ) ∈ P ) )
33 distrpr ⊢ ( 𝑥 ·P ( 𝑧 +P 𝑣 ) ) = ( ( 𝑥 ·P 𝑧 ) +P ( 𝑥 ·P 𝑣 ) )
34 distrpr ⊢ ( 𝑦 ·P ( 𝑤 +P 𝑢 ) ) = ( ( 𝑦 ·P 𝑤 ) +P ( 𝑦 ·P 𝑢 ) )
35 33 34 oveq12i ⊢ ( ( 𝑥 ·P ( 𝑧 +P 𝑣 ) ) +P ( 𝑦 ·P ( 𝑤 +P 𝑢 ) ) ) = ( ( ( 𝑥 ·P 𝑧 ) +P ( 𝑥 ·P 𝑣 ) ) +P ( ( 𝑦 ·P 𝑤 ) +P ( 𝑦 ·P 𝑢 ) ) )
36 ovex ⊢ ( 𝑥 ·P 𝑧 ) ∈ V
37 ovex ⊢ ( 𝑥 ·P 𝑣 ) ∈ V
38 ovex ⊢ ( 𝑦 ·P 𝑤 ) ∈ V
39 addcompr ⊢ ( 𝑓 +P 𝑔 ) = ( 𝑔 +P 𝑓 )
40 addasspr ⊢ ( ( 𝑓 +P 𝑔 ) +P ℎ ) = ( 𝑓 +P ( 𝑔 +P ℎ ) )
41 ovex ⊢ ( 𝑦 ·P 𝑢 ) ∈ V
42 36 37 38 39 40 41 caov4 ⊢ ( ( ( 𝑥 ·P 𝑧 ) +P ( 𝑥 ·P 𝑣 ) ) +P ( ( 𝑦 ·P 𝑤 ) +P ( 𝑦 ·P 𝑢 ) ) ) = ( ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) +P ( ( 𝑥 ·P 𝑣 ) +P ( 𝑦 ·P 𝑢 ) ) )
43 35 42 eqtri ⊢ ( ( 𝑥 ·P ( 𝑧 +P 𝑣 ) ) +P ( 𝑦 ·P ( 𝑤 +P 𝑢 ) ) ) = ( ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) +P ( ( 𝑥 ·P 𝑣 ) +P ( 𝑦 ·P 𝑢 ) ) )
44 distrpr ⊢ ( 𝑥 ·P ( 𝑤 +P 𝑢 ) ) = ( ( 𝑥 ·P 𝑤 ) +P ( 𝑥 ·P 𝑢 ) )
45 distrpr ⊢ ( 𝑦 ·P ( 𝑧 +P 𝑣 ) ) = ( ( 𝑦 ·P 𝑧 ) +P ( 𝑦 ·P 𝑣 ) )
46 44 45 oveq12i ⊢ ( ( 𝑥 ·P ( 𝑤 +P 𝑢 ) ) +P ( 𝑦 ·P ( 𝑧 +P 𝑣 ) ) ) = ( ( ( 𝑥 ·P 𝑤 ) +P ( 𝑥 ·P 𝑢 ) ) +P ( ( 𝑦 ·P 𝑧 ) +P ( 𝑦 ·P 𝑣 ) ) )
47 ovex ⊢ ( 𝑥 ·P 𝑤 ) ∈ V
48 ovex ⊢ ( 𝑥 ·P 𝑢 ) ∈ V
49 ovex ⊢ ( 𝑦 ·P 𝑧 ) ∈ V
50 ovex ⊢ ( 𝑦 ·P 𝑣 ) ∈ V
51 47 48 49 39 40 50 caov4 ⊢ ( ( ( 𝑥 ·P 𝑤 ) +P ( 𝑥 ·P 𝑢 ) ) +P ( ( 𝑦 ·P 𝑧 ) +P ( 𝑦 ·P 𝑣 ) ) ) = ( ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) +P ( ( 𝑥 ·P 𝑢 ) +P ( 𝑦 ·P 𝑣 ) ) )
52 46 51 eqtri ⊢ ( ( 𝑥 ·P ( 𝑤 +P 𝑢 ) ) +P ( 𝑦 ·P ( 𝑧 +P 𝑣 ) ) ) = ( ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) +P ( ( 𝑥 ·P 𝑢 ) +P ( 𝑦 ·P 𝑣 ) ) )
53 1 2 3 4 5 6 10 21 32 43 52 ecovdi ⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ∧ 𝐶 ∈ R ) → ( 𝐴 ·R ( 𝐵 +R 𝐶 ) ) = ( ( 𝐴 ·R 𝐵 ) +R ( 𝐴 ·R 𝐶 ) ) )
54 dmaddsr ⊢ dom +R = ( R × R )
55 0nsr ⊢ ¬ ∅ ∈ R
56 dmmulsr ⊢ dom ·R = ( R × R )
57 54 55 56 ndmovdistr ⊢ ( ¬ ( 𝐴 ∈ R ∧ 𝐵 ∈ R ∧ 𝐶 ∈ R ) → ( 𝐴 ·R ( 𝐵 +R 𝐶 ) ) = ( ( 𝐴 ·R 𝐵 ) +R ( 𝐴 ·R 𝐶 ) ) )
58 53 57 pm2.61i ⊢ ( 𝐴 ·R ( 𝐵 +R 𝐶 ) ) = ( ( 𝐴 ·R 𝐵 ) +R ( 𝐴 ·R 𝐶 ) )