Step | Hyp | Ref
| Expression |
1 | | df-nr 6655 |
. 2
⊢
R = ((P × P) /
~R ) |
2 | | addsrpr 6673 |
. 2
⊢
(((z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ([〈z, w〉]
~R +R [〈v, u〉]
~R ) = [〈(z
+P v), (w +P u)〉] ~R
) |
3 | | mulsrpr 6674 |
. 2
⊢
(((x ∈ P ∧ y ∈ P) ∧ ((z
+P v) ∈ P ∧ (w
+P u) ∈ P)) → ([〈x, y〉]
~R ·R [〈(z +P v), (w
+P u)〉]
~R ) = [〈((x
·P (z
+P v))
+P (y
·P (w
+P u))),
((x ·P
(w +P u)) +P (y ·P (z +P v)))〉] ~R
) |
4 | | mulsrpr 6674 |
. 2
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → ([〈x, y〉]
~R ·R [〈z, w〉]
~R ) = [〈((x
·P z)
+P (y
·P w)),
((x ·P
w) +P (y ·P z))〉] ~R
) |
5 | | mulsrpr 6674 |
. 2
⊢
(((x ∈ P ∧ y ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ([〈x, y〉]
~R ·R [〈v, u〉]
~R ) = [〈((x
·P v)
+P (y
·P u)),
((x ·P
u) +P (y ·P v))〉] ~R
) |
6 | | addsrpr 6673 |
. 2
⊢
(((((x
·P z)
+P (y
·P w))
∈ P ∧ ((x
·P w)
+P (y
·P z))
∈ P) ∧ (((x
·P v)
+P (y
·P u))
∈ P ∧ ((x
·P u)
+P (y
·P v))
∈ P)) → ([〈((x ·P z) +P (y ·P w)), ((x
·P w)
+P (y
·P z))〉] ~R
+R [〈((x
·P v)
+P (y
·P u)),
((x ·P
u) +P (y ·P v))〉] ~R ) =
[〈(((x
·P z)
+P (y
·P w))
+P ((x
·P v)
+P (y
·P u))),
(((x ·P
w) +P (y ·P z)) +P ((x ·P u) +P (y ·P v)))〉] ~R
) |
7 | | addclpr 6520 |
. . . 4
⊢
((z ∈ P ∧ v ∈ P) → (z +P v) ∈
P) |
8 | 7 | ad2ant2r 478 |
. . 3
⊢
(((z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (z +P v) ∈
P) |
9 | | addclpr 6520 |
. . . 4
⊢
((w ∈ P ∧ u ∈ P) → (w +P u) ∈
P) |
10 | 9 | ad2ant2l 477 |
. . 3
⊢
(((z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (w +P u) ∈
P) |
11 | 8, 10 | jca 290 |
. 2
⊢
(((z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ((z +P v) ∈
P ∧ (w +P u) ∈
P)) |
12 | | mulclpr 6553 |
. . . . 5
⊢
((x ∈ P ∧ z ∈ P) → (x ·P z) ∈
P) |
13 | 12 | ad2ant2r 478 |
. . . 4
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → (x ·P z) ∈
P) |
14 | | mulclpr 6553 |
. . . . 5
⊢
((y ∈ P ∧ w ∈ P) → (y ·P w) ∈
P) |
15 | 14 | ad2ant2l 477 |
. . . 4
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → (y ·P w) ∈
P) |
16 | | addclpr 6520 |
. . . 4
⊢
(((x
·P z) ∈ P ∧ (y
·P w) ∈ P) → ((x ·P z) +P (y ·P w)) ∈
P) |
17 | 13, 15, 16 | syl2anc 391 |
. . 3
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → ((x ·P z) +P (y ·P w)) ∈
P) |
18 | | mulclpr 6553 |
. . . . 5
⊢
((x ∈ P ∧ w ∈ P) → (x ·P w) ∈
P) |
19 | 18 | ad2ant2rl 480 |
. . . 4
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → (x ·P w) ∈
P) |
20 | | mulclpr 6553 |
. . . . 5
⊢
((y ∈ P ∧ z ∈ P) → (y ·P z) ∈
P) |
21 | 20 | ad2ant2lr 479 |
. . . 4
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → (y ·P z) ∈
P) |
22 | | addclpr 6520 |
. . . 4
⊢
(((x
·P w) ∈ P ∧ (y
·P z) ∈ P) → ((x ·P w) +P (y ·P z)) ∈
P) |
23 | 19, 21, 22 | syl2anc 391 |
. . 3
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → ((x ·P w) +P (y ·P z)) ∈
P) |
24 | 17, 23 | jca 290 |
. 2
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → (((x ·P z) +P (y ·P w)) ∈
P ∧ ((x ·P w) +P (y ·P z)) ∈
P)) |
25 | | mulclpr 6553 |
. . . . 5
⊢
((x ∈ P ∧ v ∈ P) → (x ·P v) ∈
P) |
26 | 25 | ad2ant2r 478 |
. . . 4
⊢
(((x ∈ P ∧ y ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (x ·P v) ∈
P) |
27 | | mulclpr 6553 |
. . . . 5
⊢
((y ∈ P ∧ u ∈ P) → (y ·P u) ∈
P) |
28 | 27 | ad2ant2l 477 |
. . . 4
⊢
(((x ∈ P ∧ y ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (y ·P u) ∈
P) |
29 | | addclpr 6520 |
. . . 4
⊢
(((x
·P v) ∈ P ∧ (y
·P u) ∈ P) → ((x ·P v) +P (y ·P u)) ∈
P) |
30 | 26, 28, 29 | syl2anc 391 |
. . 3
⊢
(((x ∈ P ∧ y ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ((x ·P v) +P (y ·P u)) ∈
P) |
31 | | mulclpr 6553 |
. . . . 5
⊢
((x ∈ P ∧ u ∈ P) → (x ·P u) ∈
P) |
32 | 31 | ad2ant2rl 480 |
. . . 4
⊢
(((x ∈ P ∧ y ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (x ·P u) ∈
P) |
33 | | mulclpr 6553 |
. . . . 5
⊢
((y ∈ P ∧ v ∈ P) → (y ·P v) ∈
P) |
34 | 33 | ad2ant2lr 479 |
. . . 4
⊢
(((x ∈ P ∧ y ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (y ·P v) ∈
P) |
35 | | addclpr 6520 |
. . . 4
⊢
(((x
·P u) ∈ P ∧ (y
·P v) ∈ P) → ((x ·P u) +P (y ·P v)) ∈
P) |
36 | 32, 34, 35 | syl2anc 391 |
. . 3
⊢
(((x ∈ P ∧ y ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ((x ·P u) +P (y ·P v)) ∈
P) |
37 | 30, 36 | jca 290 |
. 2
⊢
(((x ∈ P ∧ y ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (((x ·P v) +P (y ·P u)) ∈
P ∧ ((x ·P u) +P (y ·P v)) ∈
P)) |
38 | | simp1l 927 |
. . . . 5
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → x ∈
P) |
39 | | simp2l 929 |
. . . . 5
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → z ∈
P) |
40 | | simp3l 931 |
. . . . 5
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → v ∈
P) |
41 | | distrprg 6564 |
. . . . 5
⊢
((x ∈ P ∧ z ∈ P ∧ v ∈ P) → (x ·P (z +P v)) = ((x
·P z)
+P (x
·P v))) |
42 | 38, 39, 40, 41 | syl3anc 1134 |
. . . 4
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (x ·P (z +P v)) = ((x
·P z)
+P (x
·P v))) |
43 | | simp1r 928 |
. . . . 5
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → y ∈
P) |
44 | | simp2r 930 |
. . . . 5
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → w ∈
P) |
45 | | simp3r 932 |
. . . . 5
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → u ∈
P) |
46 | | distrprg 6564 |
. . . . 5
⊢
((y ∈ P ∧ w ∈ P ∧ u ∈ P) → (y ·P (w +P u)) = ((y
·P w)
+P (y
·P u))) |
47 | 43, 44, 45, 46 | syl3anc 1134 |
. . . 4
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (y ·P (w +P u)) = ((y
·P w)
+P (y
·P u))) |
48 | 42, 47 | oveq12d 5473 |
. . 3
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ((x ·P (z +P v)) +P (y ·P (w +P u))) = (((x
·P z)
+P (x
·P v))
+P ((y
·P w)
+P (y
·P u)))) |
49 | 38, 39, 12 | syl2anc 391 |
. . . 4
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (x ·P z) ∈
P) |
50 | 38, 40, 25 | syl2anc 391 |
. . . 4
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (x ·P v) ∈
P) |
51 | 43, 44, 14 | syl2anc 391 |
. . . 4
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (y ·P w) ∈
P) |
52 | | addcomprg 6554 |
. . . . 5
⊢
((f ∈ P ∧ g ∈ P) → (f +P g) = (g
+P f)) |
53 | 52 | adantl 262 |
. . . 4
⊢
((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) ∧ (f ∈ P ∧ g ∈ P)) → (f +P g) = (g
+P f)) |
54 | | addassprg 6555 |
. . . . 5
⊢
((f ∈ P ∧ g ∈ P ∧ ℎ
∈ P) → ((f +P g) +P ℎ) = (f
+P (g
+P ℎ))) |
55 | 54 | adantl 262 |
. . . 4
⊢
((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) ∧ (f ∈ P ∧ g ∈ P ∧ ℎ
∈ P)) → ((f +P g) +P ℎ) = (f
+P (g
+P ℎ))) |
56 | 43, 45, 27 | syl2anc 391 |
. . . 4
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (y ·P u) ∈
P) |
57 | | addclpr 6520 |
. . . . 5
⊢
((f ∈ P ∧ g ∈ P) → (f +P g) ∈
P) |
58 | 57 | adantl 262 |
. . . 4
⊢
((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) ∧ (f ∈ P ∧ g ∈ P)) → (f +P g) ∈
P) |
59 | 49, 50, 51, 53, 55, 56, 58 | caov4d 5627 |
. . 3
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (((x ·P z) +P (x ·P v)) +P ((y ·P w) +P (y ·P u))) = (((x
·P z)
+P (y
·P w))
+P ((x
·P v)
+P (y
·P u)))) |
60 | 48, 59 | eqtrd 2069 |
. 2
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ((x ·P (z +P v)) +P (y ·P (w +P u))) = (((x
·P z)
+P (y
·P w))
+P ((x
·P v)
+P (y
·P u)))) |
61 | | distrprg 6564 |
. . . . 5
⊢
((x ∈ P ∧ w ∈ P ∧ u ∈ P) → (x ·P (w +P u)) = ((x
·P w)
+P (x
·P u))) |
62 | 38, 44, 45, 61 | syl3anc 1134 |
. . . 4
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (x ·P (w +P u)) = ((x
·P w)
+P (x
·P u))) |
63 | | distrprg 6564 |
. . . . 5
⊢
((y ∈ P ∧ z ∈ P ∧ v ∈ P) → (y ·P (z +P v)) = ((y
·P z)
+P (y
·P v))) |
64 | 43, 39, 40, 63 | syl3anc 1134 |
. . . 4
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (y ·P (z +P v)) = ((y
·P z)
+P (y
·P v))) |
65 | 62, 64 | oveq12d 5473 |
. . 3
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ((x ·P (w +P u)) +P (y ·P (z +P v))) = (((x
·P w)
+P (x
·P u))
+P ((y
·P z)
+P (y
·P v)))) |
66 | 38, 44, 18 | syl2anc 391 |
. . . 4
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (x ·P w) ∈
P) |
67 | 38, 45, 31 | syl2anc 391 |
. . . 4
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (x ·P u) ∈
P) |
68 | 43, 39, 20 | syl2anc 391 |
. . . 4
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (y ·P z) ∈
P) |
69 | 43, 40, 33 | syl2anc 391 |
. . . 4
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (y ·P v) ∈
P) |
70 | 66, 67, 68, 53, 55, 69, 58 | caov4d 5627 |
. . 3
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (((x ·P w) +P (x ·P u)) +P ((y ·P z) +P (y ·P v))) = (((x
·P w)
+P (y
·P z))
+P ((x
·P u)
+P (y
·P v)))) |
71 | 65, 70 | eqtrd 2069 |
. 2
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ((x ·P (w +P u)) +P (y ·P (z +P v))) = (((x
·P w)
+P (y
·P z))
+P ((x
·P u)
+P (y
·P v)))) |
72 | 1, 2, 3, 4, 5, 6, 11, 24, 37, 60, 71 | ecovidi 6154 |
1
⊢
((A ∈ R ∧ B ∈ R ∧ 𝐶 ∈
R) → (A
·R (B
+R 𝐶)) = ((A
·R B)
+R (A
·R 𝐶))) |