Step | Hyp | Ref
| Expression |
1 | | df-nr 7676 |
. 2
⊢
R = ((P × P) /
~R ) |
2 | | addsrpr 7694 |
. 2
⊢ (((𝑧 ∈ P ∧
𝑤 ∈ P)
∧ (𝑣 ∈
P ∧ 𝑢
∈ P)) → ([〈𝑧, 𝑤〉] ~R
+R [〈𝑣, 𝑢〉] ~R ) =
[〈(𝑧
+P 𝑣), (𝑤 +P 𝑢)〉]
~R ) |
3 | | mulsrpr 7695 |
. 2
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ ((𝑧
+P 𝑣) ∈ P ∧ (𝑤 +P
𝑢) ∈ P))
→ ([〈𝑥, 𝑦〉]
~R ·R [〈(𝑧 +P
𝑣), (𝑤 +P 𝑢)〉]
~R ) = [〈((𝑥 ·P (𝑧 +P
𝑣))
+P (𝑦 ·P (𝑤 +P
𝑢))), ((𝑥 ·P (𝑤 +P
𝑢))
+P (𝑦 ·P (𝑧 +P
𝑣)))〉]
~R ) |
4 | | mulsrpr 7695 |
. 2
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → ([〈𝑥, 𝑦〉] ~R
·R [〈𝑧, 𝑤〉] ~R ) =
[〈((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)), ((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧))〉] ~R
) |
5 | | mulsrpr 7695 |
. 2
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑣 ∈
P ∧ 𝑢
∈ P)) → ([〈𝑥, 𝑦〉] ~R
·R [〈𝑣, 𝑢〉] ~R ) =
[〈((𝑥
·P 𝑣) +P (𝑦
·P 𝑢)), ((𝑥 ·P 𝑢) +P
(𝑦
·P 𝑣))〉] ~R
) |
6 | | addsrpr 7694 |
. 2
⊢
(((((𝑥
·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 7486 |
. . . 4
⊢ ((𝑧 ∈ P ∧
𝑣 ∈ P)
→ (𝑧
+P 𝑣) ∈ P) |
8 | 7 | ad2ant2r 506 |
. . 3
⊢ (((𝑧 ∈ P ∧
𝑤 ∈ P)
∧ (𝑣 ∈
P ∧ 𝑢
∈ P)) → (𝑧 +P 𝑣) ∈
P) |
9 | | addclpr 7486 |
. . . 4
⊢ ((𝑤 ∈ P ∧
𝑢 ∈ P)
→ (𝑤
+P 𝑢) ∈ P) |
10 | 9 | ad2ant2l 505 |
. . 3
⊢ (((𝑧 ∈ P ∧
𝑤 ∈ P)
∧ (𝑣 ∈
P ∧ 𝑢
∈ P)) → (𝑤 +P 𝑢) ∈
P) |
11 | 8, 10 | jca 304 |
. 2
⊢ (((𝑧 ∈ P ∧
𝑤 ∈ P)
∧ (𝑣 ∈
P ∧ 𝑢
∈ P)) → ((𝑧 +P 𝑣) ∈ P ∧
(𝑤
+P 𝑢) ∈ P)) |
12 | | mulclpr 7521 |
. . . . 5
⊢ ((𝑥 ∈ P ∧
𝑧 ∈ P)
→ (𝑥
·P 𝑧) ∈ P) |
13 | 12 | ad2ant2r 506 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → (𝑥 ·P 𝑧) ∈
P) |
14 | | mulclpr 7521 |
. . . . 5
⊢ ((𝑦 ∈ P ∧
𝑤 ∈ P)
→ (𝑦
·P 𝑤) ∈ P) |
15 | 14 | ad2ant2l 505 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → (𝑦 ·P 𝑤) ∈
P) |
16 | | addclpr 7486 |
. . . 4
⊢ (((𝑥
·P 𝑧) ∈ P ∧ (𝑦
·P 𝑤) ∈ P) → ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)) ∈ P) |
17 | 13, 15, 16 | syl2anc 409 |
. . 3
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → ((𝑥 ·P 𝑧) +P
(𝑦
·P 𝑤)) ∈ P) |
18 | | mulclpr 7521 |
. . . . 5
⊢ ((𝑥 ∈ P ∧
𝑤 ∈ P)
→ (𝑥
·P 𝑤) ∈ P) |
19 | 18 | ad2ant2rl 508 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → (𝑥 ·P 𝑤) ∈
P) |
20 | | mulclpr 7521 |
. . . . 5
⊢ ((𝑦 ∈ P ∧
𝑧 ∈ P)
→ (𝑦
·P 𝑧) ∈ P) |
21 | 20 | ad2ant2lr 507 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → (𝑦 ·P 𝑧) ∈
P) |
22 | | addclpr 7486 |
. . . 4
⊢ (((𝑥
·P 𝑤) ∈ P ∧ (𝑦
·P 𝑧) ∈ P) → ((𝑥
·P 𝑤) +P (𝑦
·P 𝑧)) ∈ P) |
23 | 19, 21, 22 | syl2anc 409 |
. . 3
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → ((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧)) ∈ P) |
24 | 17, 23 | jca 304 |
. 2
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → (((𝑥 ·P 𝑧) +P
(𝑦
·P 𝑤)) ∈ P ∧ ((𝑥
·P 𝑤) +P (𝑦
·P 𝑧)) ∈ P)) |
25 | | mulclpr 7521 |
. . . . 5
⊢ ((𝑥 ∈ P ∧
𝑣 ∈ P)
→ (𝑥
·P 𝑣) ∈ P) |
26 | 25 | ad2ant2r 506 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑣 ∈
P ∧ 𝑢
∈ P)) → (𝑥 ·P 𝑣) ∈
P) |
27 | | mulclpr 7521 |
. . . . 5
⊢ ((𝑦 ∈ P ∧
𝑢 ∈ P)
→ (𝑦
·P 𝑢) ∈ P) |
28 | 27 | ad2ant2l 505 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑣 ∈
P ∧ 𝑢
∈ P)) → (𝑦 ·P 𝑢) ∈
P) |
29 | | addclpr 7486 |
. . . 4
⊢ (((𝑥
·P 𝑣) ∈ P ∧ (𝑦
·P 𝑢) ∈ P) → ((𝑥
·P 𝑣) +P (𝑦
·P 𝑢)) ∈ P) |
30 | 26, 28, 29 | syl2anc 409 |
. . 3
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑣 ∈
P ∧ 𝑢
∈ P)) → ((𝑥 ·P 𝑣) +P
(𝑦
·P 𝑢)) ∈ P) |
31 | | mulclpr 7521 |
. . . . 5
⊢ ((𝑥 ∈ P ∧
𝑢 ∈ P)
→ (𝑥
·P 𝑢) ∈ P) |
32 | 31 | ad2ant2rl 508 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑣 ∈
P ∧ 𝑢
∈ P)) → (𝑥 ·P 𝑢) ∈
P) |
33 | | mulclpr 7521 |
. . . . 5
⊢ ((𝑦 ∈ P ∧
𝑣 ∈ P)
→ (𝑦
·P 𝑣) ∈ P) |
34 | 33 | ad2ant2lr 507 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑣 ∈
P ∧ 𝑢
∈ P)) → (𝑦 ·P 𝑣) ∈
P) |
35 | | addclpr 7486 |
. . . 4
⊢ (((𝑥
·P 𝑢) ∈ P ∧ (𝑦
·P 𝑣) ∈ P) → ((𝑥
·P 𝑢) +P (𝑦
·P 𝑣)) ∈ P) |
36 | 32, 34, 35 | syl2anc 409 |
. . 3
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑣 ∈
P ∧ 𝑢
∈ P)) → ((𝑥 ·P 𝑢) +P
(𝑦
·P 𝑣)) ∈ P) |
37 | 30, 36 | jca 304 |
. 2
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑣 ∈
P ∧ 𝑢
∈ P)) → (((𝑥 ·P 𝑣) +P
(𝑦
·P 𝑢)) ∈ P ∧ ((𝑥
·P 𝑢) +P (𝑦
·P 𝑣)) ∈ P)) |
38 | | simp1l 1016 |
. . . . 5
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
𝑥 ∈
P) |
39 | | simp2l 1018 |
. . . . 5
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
𝑧 ∈
P) |
40 | | simp3l 1020 |
. . . . 5
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
𝑣 ∈
P) |
41 | | distrprg 7537 |
. . . . 5
⊢ ((𝑥 ∈ P ∧
𝑧 ∈ P
∧ 𝑣 ∈
P) → (𝑥
·P (𝑧 +P 𝑣)) = ((𝑥 ·P 𝑧) +P
(𝑥
·P 𝑣))) |
42 | 38, 39, 40, 41 | syl3anc 1233 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
(𝑥
·P (𝑧 +P 𝑣)) = ((𝑥 ·P 𝑧) +P
(𝑥
·P 𝑣))) |
43 | | simp1r 1017 |
. . . . 5
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
𝑦 ∈
P) |
44 | | simp2r 1019 |
. . . . 5
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
𝑤 ∈
P) |
45 | | simp3r 1021 |
. . . . 5
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
𝑢 ∈
P) |
46 | | distrprg 7537 |
. . . . 5
⊢ ((𝑦 ∈ P ∧
𝑤 ∈ P
∧ 𝑢 ∈
P) → (𝑦
·P (𝑤 +P 𝑢)) = ((𝑦 ·P 𝑤) +P
(𝑦
·P 𝑢))) |
47 | 43, 44, 45, 46 | syl3anc 1233 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
(𝑦
·P (𝑤 +P 𝑢)) = ((𝑦 ·P 𝑤) +P
(𝑦
·P 𝑢))) |
48 | 42, 47 | oveq12d 5868 |
. . 3
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
((𝑥
·P (𝑧 +P 𝑣)) +P
(𝑦
·P (𝑤 +P 𝑢))) = (((𝑥 ·P 𝑧) +P
(𝑥
·P 𝑣)) +P ((𝑦
·P 𝑤) +P (𝑦
·P 𝑢)))) |
49 | 38, 39, 12 | syl2anc 409 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
(𝑥
·P 𝑧) ∈ P) |
50 | 38, 40, 25 | syl2anc 409 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
(𝑥
·P 𝑣) ∈ P) |
51 | 43, 44, 14 | syl2anc 409 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
(𝑦
·P 𝑤) ∈ P) |
52 | | addcomprg 7527 |
. . . . 5
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ (𝑓
+P 𝑔) = (𝑔 +P 𝑓)) |
53 | 52 | adantl 275 |
. . . 4
⊢ ((((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) ∧
(𝑓 ∈ P
∧ 𝑔 ∈
P)) → (𝑓
+P 𝑔) = (𝑔 +P 𝑓)) |
54 | | addassprg 7528 |
. . . . 5
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P
∧ ℎ ∈
P) → ((𝑓
+P 𝑔) +P ℎ) = (𝑓 +P (𝑔 +P
ℎ))) |
55 | 54 | adantl 275 |
. . . 4
⊢ ((((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) ∧
(𝑓 ∈ P
∧ 𝑔 ∈
P ∧ ℎ
∈ P)) → ((𝑓 +P 𝑔) +P
ℎ) = (𝑓 +P (𝑔 +P
ℎ))) |
56 | 43, 45, 27 | syl2anc 409 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
(𝑦
·P 𝑢) ∈ P) |
57 | | addclpr 7486 |
. . . . 5
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ (𝑓
+P 𝑔) ∈ P) |
58 | 57 | adantl 275 |
. . . 4
⊢ ((((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) ∧
(𝑓 ∈ P
∧ 𝑔 ∈
P)) → (𝑓
+P 𝑔) ∈ P) |
59 | 49, 50, 51, 53, 55, 56, 58 | caov4d 6034 |
. . 3
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
(((𝑥
·P 𝑧) +P (𝑥
·P 𝑣)) +P ((𝑦
·P 𝑤) +P (𝑦
·P 𝑢))) = (((𝑥 ·P 𝑧) +P
(𝑦
·P 𝑤)) +P ((𝑥
·P 𝑣) +P (𝑦
·P 𝑢)))) |
60 | 48, 59 | eqtrd 2203 |
. 2
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
((𝑥
·P (𝑧 +P 𝑣)) +P
(𝑦
·P (𝑤 +P 𝑢))) = (((𝑥 ·P 𝑧) +P
(𝑦
·P 𝑤)) +P ((𝑥
·P 𝑣) +P (𝑦
·P 𝑢)))) |
61 | | distrprg 7537 |
. . . . 5
⊢ ((𝑥 ∈ P ∧
𝑤 ∈ P
∧ 𝑢 ∈
P) → (𝑥
·P (𝑤 +P 𝑢)) = ((𝑥 ·P 𝑤) +P
(𝑥
·P 𝑢))) |
62 | 38, 44, 45, 61 | syl3anc 1233 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
(𝑥
·P (𝑤 +P 𝑢)) = ((𝑥 ·P 𝑤) +P
(𝑥
·P 𝑢))) |
63 | | distrprg 7537 |
. . . . 5
⊢ ((𝑦 ∈ P ∧
𝑧 ∈ P
∧ 𝑣 ∈
P) → (𝑦
·P (𝑧 +P 𝑣)) = ((𝑦 ·P 𝑧) +P
(𝑦
·P 𝑣))) |
64 | 43, 39, 40, 63 | syl3anc 1233 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
(𝑦
·P (𝑧 +P 𝑣)) = ((𝑦 ·P 𝑧) +P
(𝑦
·P 𝑣))) |
65 | 62, 64 | oveq12d 5868 |
. . 3
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
((𝑥
·P (𝑤 +P 𝑢)) +P
(𝑦
·P (𝑧 +P 𝑣))) = (((𝑥 ·P 𝑤) +P
(𝑥
·P 𝑢)) +P ((𝑦
·P 𝑧) +P (𝑦
·P 𝑣)))) |
66 | 38, 44, 18 | syl2anc 409 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
(𝑥
·P 𝑤) ∈ P) |
67 | 38, 45, 31 | syl2anc 409 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
(𝑥
·P 𝑢) ∈ P) |
68 | 43, 39, 20 | syl2anc 409 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
(𝑦
·P 𝑧) ∈ P) |
69 | 43, 40, 33 | syl2anc 409 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
(𝑦
·P 𝑣) ∈ P) |
70 | 66, 67, 68, 53, 55, 69, 58 | caov4d 6034 |
. . 3
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
(((𝑥
·P 𝑤) +P (𝑥
·P 𝑢)) +P ((𝑦
·P 𝑧) +P (𝑦
·P 𝑣))) = (((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧)) +P ((𝑥
·P 𝑢) +P (𝑦
·P 𝑣)))) |
71 | 65, 70 | eqtrd 2203 |
. 2
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
((𝑥
·P (𝑤 +P 𝑢)) +P
(𝑦
·P (𝑧 +P 𝑣))) = (((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧)) +P ((𝑥
·P 𝑢) +P (𝑦
·P 𝑣)))) |
72 | 1, 2, 3, 4, 5, 6, 11, 24, 37, 60, 71 | ecovidi 6621 |
1
⊢ ((𝐴 ∈ R ∧
𝐵 ∈ R
∧ 𝐶 ∈
R) → (𝐴
·R (𝐵 +R 𝐶)) = ((𝐴 ·R 𝐵) +R
(𝐴
·R 𝐶))) |