| Step | Hyp | Ref
| Expression |
| 1 | | df-nr 11096 |
. . 3
⊢
R = ((P × P) /
~R ) |
| 2 | | addsrpr 11115 |
. . 3
⊢ (((𝑧 ∈ P ∧
𝑤 ∈ P)
∧ (𝑣 ∈
P ∧ 𝑢
∈ P)) → ([〈𝑧, 𝑤〉] ~R
+R [〈𝑣, 𝑢〉] ~R ) =
[〈(𝑧
+P 𝑣), (𝑤 +P 𝑢)〉]
~R ) |
| 3 | | mulsrpr 11116 |
. . 3
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ ((𝑧
+P 𝑣) ∈ P ∧ (𝑤 +P
𝑢) ∈ P))
→ ([〈𝑥, 𝑦〉]
~R ·R [〈(𝑧 +P
𝑣), (𝑤 +P 𝑢)〉]
~R ) = [〈((𝑥 ·P (𝑧 +P
𝑣))
+P (𝑦 ·P (𝑤 +P
𝑢))), ((𝑥 ·P (𝑤 +P
𝑢))
+P (𝑦 ·P (𝑧 +P
𝑣)))〉]
~R ) |
| 4 | | mulsrpr 11116 |
. . 3
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → ([〈𝑥, 𝑦〉] ~R
·R [〈𝑧, 𝑤〉] ~R ) =
[〈((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)), ((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧))〉] ~R
) |
| 5 | | mulsrpr 11116 |
. . 3
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑣 ∈
P ∧ 𝑢
∈ P)) → ([〈𝑥, 𝑦〉] ~R
·R [〈𝑣, 𝑢〉] ~R ) =
[〈((𝑥
·P 𝑣) +P (𝑦
·P 𝑢)), ((𝑥 ·P 𝑢) +P
(𝑦
·P 𝑣))〉] ~R
) |
| 6 | | addsrpr 11115 |
. . 3
⊢
(((((𝑥
·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 11058 |
. . . . 5
⊢ ((𝑧 ∈ P ∧
𝑣 ∈ P)
→ (𝑧
+P 𝑣) ∈ P) |
| 8 | | addclpr 11058 |
. . . . 5
⊢ ((𝑤 ∈ P ∧
𝑢 ∈ P)
→ (𝑤
+P 𝑢) ∈ P) |
| 9 | 7, 8 | anim12i 613 |
. . . 4
⊢ (((𝑧 ∈ P ∧
𝑣 ∈ P)
∧ (𝑤 ∈
P ∧ 𝑢
∈ P)) → ((𝑧 +P 𝑣) ∈ P ∧
(𝑤
+P 𝑢) ∈ P)) |
| 10 | 9 | an4s 660 |
. . 3
⊢ (((𝑧 ∈ P ∧
𝑤 ∈ P)
∧ (𝑣 ∈
P ∧ 𝑢
∈ P)) → ((𝑧 +P 𝑣) ∈ P ∧
(𝑤
+P 𝑢) ∈ P)) |
| 11 | | mulclpr 11060 |
. . . . . 6
⊢ ((𝑥 ∈ P ∧
𝑧 ∈ P)
→ (𝑥
·P 𝑧) ∈ P) |
| 12 | | mulclpr 11060 |
. . . . . 6
⊢ ((𝑦 ∈ P ∧
𝑤 ∈ P)
→ (𝑦
·P 𝑤) ∈ P) |
| 13 | | addclpr 11058 |
. . . . . 6
⊢ (((𝑥
·P 𝑧) ∈ P ∧ (𝑦
·P 𝑤) ∈ P) → ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)) ∈ P) |
| 14 | 11, 12, 13 | syl2an 596 |
. . . . 5
⊢ (((𝑥 ∈ P ∧
𝑧 ∈ P)
∧ (𝑦 ∈
P ∧ 𝑤
∈ P)) → ((𝑥 ·P 𝑧) +P
(𝑦
·P 𝑤)) ∈ P) |
| 15 | 14 | an4s 660 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → ((𝑥 ·P 𝑧) +P
(𝑦
·P 𝑤)) ∈ P) |
| 16 | | mulclpr 11060 |
. . . . . 6
⊢ ((𝑥 ∈ P ∧
𝑤 ∈ P)
→ (𝑥
·P 𝑤) ∈ P) |
| 17 | | mulclpr 11060 |
. . . . . 6
⊢ ((𝑦 ∈ P ∧
𝑧 ∈ P)
→ (𝑦
·P 𝑧) ∈ P) |
| 18 | | addclpr 11058 |
. . . . . 6
⊢ (((𝑥
·P 𝑤) ∈ P ∧ (𝑦
·P 𝑧) ∈ P) → ((𝑥
·P 𝑤) +P (𝑦
·P 𝑧)) ∈ P) |
| 19 | 16, 17, 18 | syl2an 596 |
. . . . 5
⊢ (((𝑥 ∈ P ∧
𝑤 ∈ P)
∧ (𝑦 ∈
P ∧ 𝑧
∈ P)) → ((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧)) ∈ P) |
| 20 | 19 | an42s 661 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → ((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧)) ∈ P) |
| 21 | 15, 20 | jca 511 |
. . 3
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → (((𝑥 ·P 𝑧) +P
(𝑦
·P 𝑤)) ∈ P ∧ ((𝑥
·P 𝑤) +P (𝑦
·P 𝑧)) ∈ P)) |
| 22 | | mulclpr 11060 |
. . . . . 6
⊢ ((𝑥 ∈ P ∧
𝑣 ∈ P)
→ (𝑥
·P 𝑣) ∈ P) |
| 23 | | mulclpr 11060 |
. . . . . 6
⊢ ((𝑦 ∈ P ∧
𝑢 ∈ P)
→ (𝑦
·P 𝑢) ∈ P) |
| 24 | | addclpr 11058 |
. . . . . 6
⊢ (((𝑥
·P 𝑣) ∈ P ∧ (𝑦
·P 𝑢) ∈ P) → ((𝑥
·P 𝑣) +P (𝑦
·P 𝑢)) ∈ P) |
| 25 | 22, 23, 24 | syl2an 596 |
. . . . 5
⊢ (((𝑥 ∈ P ∧
𝑣 ∈ P)
∧ (𝑦 ∈
P ∧ 𝑢
∈ P)) → ((𝑥 ·P 𝑣) +P
(𝑦
·P 𝑢)) ∈ P) |
| 26 | 25 | an4s 660 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑣 ∈
P ∧ 𝑢
∈ P)) → ((𝑥 ·P 𝑣) +P
(𝑦
·P 𝑢)) ∈ P) |
| 27 | | mulclpr 11060 |
. . . . . 6
⊢ ((𝑥 ∈ P ∧
𝑢 ∈ P)
→ (𝑥
·P 𝑢) ∈ P) |
| 28 | | mulclpr 11060 |
. . . . . 6
⊢ ((𝑦 ∈ P ∧
𝑣 ∈ P)
→ (𝑦
·P 𝑣) ∈ P) |
| 29 | | addclpr 11058 |
. . . . . 6
⊢ (((𝑥
·P 𝑢) ∈ P ∧ (𝑦
·P 𝑣) ∈ P) → ((𝑥
·P 𝑢) +P (𝑦
·P 𝑣)) ∈ P) |
| 30 | 27, 28, 29 | syl2an 596 |
. . . . 5
⊢ (((𝑥 ∈ P ∧
𝑢 ∈ P)
∧ (𝑦 ∈
P ∧ 𝑣
∈ P)) → ((𝑥 ·P 𝑢) +P
(𝑦
·P 𝑣)) ∈ P) |
| 31 | 30 | an42s 661 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑣 ∈
P ∧ 𝑢
∈ P)) → ((𝑥 ·P 𝑢) +P
(𝑦
·P 𝑣)) ∈ P) |
| 32 | 26, 31 | jca 511 |
. . 3
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑣 ∈
P ∧ 𝑢
∈ P)) → (((𝑥 ·P 𝑣) +P
(𝑦
·P 𝑢)) ∈ P ∧ ((𝑥
·P 𝑢) +P (𝑦
·P 𝑣)) ∈ P)) |
| 33 | | distrpr 11068 |
. . . . 5
⊢ (𝑥
·P (𝑧 +P 𝑣)) = ((𝑥 ·P 𝑧) +P
(𝑥
·P 𝑣)) |
| 34 | | distrpr 11068 |
. . . . 5
⊢ (𝑦
·P (𝑤 +P 𝑢)) = ((𝑦 ·P 𝑤) +P
(𝑦
·P 𝑢)) |
| 35 | 33, 34 | oveq12i 7443 |
. . . 4
⊢ ((𝑥
·P (𝑧 +P 𝑣)) +P
(𝑦
·P (𝑤 +P 𝑢))) = (((𝑥 ·P 𝑧) +P
(𝑥
·P 𝑣)) +P ((𝑦
·P 𝑤) +P (𝑦
·P 𝑢))) |
| 36 | | ovex 7464 |
. . . . 5
⊢ (𝑥
·P 𝑧) ∈ V |
| 37 | | ovex 7464 |
. . . . 5
⊢ (𝑥
·P 𝑣) ∈ V |
| 38 | | ovex 7464 |
. . . . 5
⊢ (𝑦
·P 𝑤) ∈ V |
| 39 | | addcompr 11061 |
. . . . 5
⊢ (𝑓 +P
𝑔) = (𝑔 +P 𝑓) |
| 40 | | addasspr 11062 |
. . . . 5
⊢ ((𝑓 +P
𝑔)
+P ℎ) = (𝑓 +P (𝑔 +P
ℎ)) |
| 41 | | ovex 7464 |
. . . . 5
⊢ (𝑦
·P 𝑢) ∈ V |
| 42 | 36, 37, 38, 39, 40, 41 | caov4 7664 |
. . . 4
⊢ (((𝑥
·P 𝑧) +P (𝑥
·P 𝑣)) +P ((𝑦
·P 𝑤) +P (𝑦
·P 𝑢))) = (((𝑥 ·P 𝑧) +P
(𝑦
·P 𝑤)) +P ((𝑥
·P 𝑣) +P (𝑦
·P 𝑢))) |
| 43 | 35, 42 | eqtri 2765 |
. . 3
⊢ ((𝑥
·P (𝑧 +P 𝑣)) +P
(𝑦
·P (𝑤 +P 𝑢))) = (((𝑥 ·P 𝑧) +P
(𝑦
·P 𝑤)) +P ((𝑥
·P 𝑣) +P (𝑦
·P 𝑢))) |
| 44 | | distrpr 11068 |
. . . . 5
⊢ (𝑥
·P (𝑤 +P 𝑢)) = ((𝑥 ·P 𝑤) +P
(𝑥
·P 𝑢)) |
| 45 | | distrpr 11068 |
. . . . 5
⊢ (𝑦
·P (𝑧 +P 𝑣)) = ((𝑦 ·P 𝑧) +P
(𝑦
·P 𝑣)) |
| 46 | 44, 45 | oveq12i 7443 |
. . . 4
⊢ ((𝑥
·P (𝑤 +P 𝑢)) +P
(𝑦
·P (𝑧 +P 𝑣))) = (((𝑥 ·P 𝑤) +P
(𝑥
·P 𝑢)) +P ((𝑦
·P 𝑧) +P (𝑦
·P 𝑣))) |
| 47 | | ovex 7464 |
. . . . 5
⊢ (𝑥
·P 𝑤) ∈ V |
| 48 | | ovex 7464 |
. . . . 5
⊢ (𝑥
·P 𝑢) ∈ V |
| 49 | | ovex 7464 |
. . . . 5
⊢ (𝑦
·P 𝑧) ∈ V |
| 50 | | ovex 7464 |
. . . . 5
⊢ (𝑦
·P 𝑣) ∈ V |
| 51 | 47, 48, 49, 39, 40, 50 | caov4 7664 |
. . . 4
⊢ (((𝑥
·P 𝑤) +P (𝑥
·P 𝑢)) +P ((𝑦
·P 𝑧) +P (𝑦
·P 𝑣))) = (((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧)) +P ((𝑥
·P 𝑢) +P (𝑦
·P 𝑣))) |
| 52 | 46, 51 | eqtri 2765 |
. . 3
⊢ ((𝑥
·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 8865 |
. 2
⊢ ((𝐴 ∈ R ∧
𝐵 ∈ R
∧ 𝐶 ∈
R) → (𝐴
·R (𝐵 +R 𝐶)) = ((𝐴 ·R 𝐵) +R
(𝐴
·R 𝐶))) |
| 54 | | dmaddsr 11125 |
. . 3
⊢ dom
+R = (R ×
R) |
| 55 | | 0nsr 11119 |
. . 3
⊢ ¬
∅ ∈ R |
| 56 | | dmmulsr 11126 |
. . 3
⊢ dom
·R = (R ×
R) |
| 57 | 54, 55, 56 | ndmovdistr 7622 |
. 2
⊢ (¬
(𝐴 ∈ R
∧ 𝐵 ∈
R ∧ 𝐶
∈ R) → (𝐴 ·R (𝐵 +R
𝐶)) = ((𝐴 ·R 𝐵) +R
(𝐴
·R 𝐶))) |
| 58 | 53, 57 | pm2.61i 182 |
1
⊢ (𝐴
·R (𝐵 +R 𝐶)) = ((𝐴 ·R 𝐵) +R
(𝐴
·R 𝐶)) |