Step | Hyp | Ref
| Expression |
1 | | df-nr 11051 |
. . 3
โข
R = ((P ร P) /
~R ) |
2 | | addsrpr 11070 |
. . 3
โข (((๐ง โ P โง
๐ค โ P)
โง (๐ฃ โ
P โง ๐ข
โ P)) โ ([โจ๐ง, ๐คโฉ] ~R
+R [โจ๐ฃ, ๐ขโฉ] ~R ) =
[โจ(๐ง
+P ๐ฃ), (๐ค +P ๐ข)โฉ]
~R ) |
3 | | mulsrpr 11071 |
. . 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 11071 |
. . 3
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P)) โ ([โจ๐ฅ, ๐ฆโฉ] ~R
ยทR [โจ๐ง, ๐คโฉ] ~R ) =
[โจ((๐ฅ
ยทP ๐ง) +P (๐ฆ
ยทP ๐ค)), ((๐ฅ ยทP ๐ค) +P
(๐ฆ
ยทP ๐ง))โฉ] ~R
) |
5 | | mulsrpr 11071 |
. . 3
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ฃ โ
P โง ๐ข
โ P)) โ ([โจ๐ฅ, ๐ฆโฉ] ~R
ยทR [โจ๐ฃ, ๐ขโฉ] ~R ) =
[โจ((๐ฅ
ยทP ๐ฃ) +P (๐ฆ
ยทP ๐ข)), ((๐ฅ ยทP ๐ข) +P
(๐ฆ
ยทP ๐ฃ))โฉ] ~R
) |
6 | | addsrpr 11070 |
. . 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 11013 |
. . . . 5
โข ((๐ง โ P โง
๐ฃ โ P)
โ (๐ง
+P ๐ฃ) โ P) |
8 | | addclpr 11013 |
. . . . 5
โข ((๐ค โ P โง
๐ข โ P)
โ (๐ค
+P ๐ข) โ P) |
9 | 7, 8 | anim12i 614 |
. . . 4
โข (((๐ง โ P โง
๐ฃ โ P)
โง (๐ค โ
P โง ๐ข
โ P)) โ ((๐ง +P ๐ฃ) โ P โง
(๐ค
+P ๐ข) โ P)) |
10 | 9 | an4s 659 |
. . 3
โข (((๐ง โ P โง
๐ค โ P)
โง (๐ฃ โ
P โง ๐ข
โ P)) โ ((๐ง +P ๐ฃ) โ P โง
(๐ค
+P ๐ข) โ P)) |
11 | | mulclpr 11015 |
. . . . . 6
โข ((๐ฅ โ P โง
๐ง โ P)
โ (๐ฅ
ยทP ๐ง) โ P) |
12 | | mulclpr 11015 |
. . . . . 6
โข ((๐ฆ โ P โง
๐ค โ P)
โ (๐ฆ
ยทP ๐ค) โ P) |
13 | | addclpr 11013 |
. . . . . 6
โข (((๐ฅ
ยทP ๐ง) โ P โง (๐ฆ
ยทP ๐ค) โ P) โ ((๐ฅ
ยทP ๐ง) +P (๐ฆ
ยทP ๐ค)) โ P) |
14 | 11, 12, 13 | syl2an 597 |
. . . . 5
โข (((๐ฅ โ P โง
๐ง โ P)
โง (๐ฆ โ
P โง ๐ค
โ P)) โ ((๐ฅ ยทP ๐ง) +P
(๐ฆ
ยทP ๐ค)) โ P) |
15 | 14 | an4s 659 |
. . . 4
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P)) โ ((๐ฅ ยทP ๐ง) +P
(๐ฆ
ยทP ๐ค)) โ P) |
16 | | mulclpr 11015 |
. . . . . 6
โข ((๐ฅ โ P โง
๐ค โ P)
โ (๐ฅ
ยทP ๐ค) โ P) |
17 | | mulclpr 11015 |
. . . . . 6
โข ((๐ฆ โ P โง
๐ง โ P)
โ (๐ฆ
ยทP ๐ง) โ P) |
18 | | addclpr 11013 |
. . . . . 6
โข (((๐ฅ
ยทP ๐ค) โ P โง (๐ฆ
ยทP ๐ง) โ P) โ ((๐ฅ
ยทP ๐ค) +P (๐ฆ
ยทP ๐ง)) โ P) |
19 | 16, 17, 18 | syl2an 597 |
. . . . 5
โข (((๐ฅ โ P โง
๐ค โ P)
โง (๐ฆ โ
P โง ๐ง
โ P)) โ ((๐ฅ ยทP ๐ค) +P
(๐ฆ
ยทP ๐ง)) โ P) |
20 | 19 | an42s 660 |
. . . 4
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P)) โ ((๐ฅ ยทP ๐ค) +P
(๐ฆ
ยทP ๐ง)) โ P) |
21 | 15, 20 | jca 513 |
. . 3
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P)) โ (((๐ฅ ยทP ๐ง) +P
(๐ฆ
ยทP ๐ค)) โ P โง ((๐ฅ
ยทP ๐ค) +P (๐ฆ
ยทP ๐ง)) โ P)) |
22 | | mulclpr 11015 |
. . . . . 6
โข ((๐ฅ โ P โง
๐ฃ โ P)
โ (๐ฅ
ยทP ๐ฃ) โ P) |
23 | | mulclpr 11015 |
. . . . . 6
โข ((๐ฆ โ P โง
๐ข โ P)
โ (๐ฆ
ยทP ๐ข) โ P) |
24 | | addclpr 11013 |
. . . . . 6
โข (((๐ฅ
ยทP ๐ฃ) โ P โง (๐ฆ
ยทP ๐ข) โ P) โ ((๐ฅ
ยทP ๐ฃ) +P (๐ฆ
ยทP ๐ข)) โ P) |
25 | 22, 23, 24 | syl2an 597 |
. . . . 5
โข (((๐ฅ โ P โง
๐ฃ โ P)
โง (๐ฆ โ
P โง ๐ข
โ P)) โ ((๐ฅ ยทP ๐ฃ) +P
(๐ฆ
ยทP ๐ข)) โ P) |
26 | 25 | an4s 659 |
. . . 4
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ฃ โ
P โง ๐ข
โ P)) โ ((๐ฅ ยทP ๐ฃ) +P
(๐ฆ
ยทP ๐ข)) โ P) |
27 | | mulclpr 11015 |
. . . . . 6
โข ((๐ฅ โ P โง
๐ข โ P)
โ (๐ฅ
ยทP ๐ข) โ P) |
28 | | mulclpr 11015 |
. . . . . 6
โข ((๐ฆ โ P โง
๐ฃ โ P)
โ (๐ฆ
ยทP ๐ฃ) โ P) |
29 | | addclpr 11013 |
. . . . . 6
โข (((๐ฅ
ยทP ๐ข) โ P โง (๐ฆ
ยทP ๐ฃ) โ P) โ ((๐ฅ
ยทP ๐ข) +P (๐ฆ
ยทP ๐ฃ)) โ P) |
30 | 27, 28, 29 | syl2an 597 |
. . . . 5
โข (((๐ฅ โ P โง
๐ข โ P)
โง (๐ฆ โ
P โง ๐ฃ
โ P)) โ ((๐ฅ ยทP ๐ข) +P
(๐ฆ
ยทP ๐ฃ)) โ P) |
31 | 30 | an42s 660 |
. . . 4
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ฃ โ
P โง ๐ข
โ P)) โ ((๐ฅ ยทP ๐ข) +P
(๐ฆ
ยทP ๐ฃ)) โ P) |
32 | 26, 31 | jca 513 |
. . 3
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ฃ โ
P โง ๐ข
โ P)) โ (((๐ฅ ยทP ๐ฃ) +P
(๐ฆ
ยทP ๐ข)) โ P โง ((๐ฅ
ยทP ๐ข) +P (๐ฆ
ยทP ๐ฃ)) โ P)) |
33 | | distrpr 11023 |
. . . . 5
โข (๐ฅ
ยทP (๐ง +P ๐ฃ)) = ((๐ฅ ยทP ๐ง) +P
(๐ฅ
ยทP ๐ฃ)) |
34 | | distrpr 11023 |
. . . . 5
โข (๐ฆ
ยทP (๐ค +P ๐ข)) = ((๐ฆ ยทP ๐ค) +P
(๐ฆ
ยทP ๐ข)) |
35 | 33, 34 | oveq12i 7421 |
. . . 4
โข ((๐ฅ
ยทP (๐ง +P ๐ฃ)) +P
(๐ฆ
ยทP (๐ค +P ๐ข))) = (((๐ฅ ยทP ๐ง) +P
(๐ฅ
ยทP ๐ฃ)) +P ((๐ฆ
ยทP ๐ค) +P (๐ฆ
ยทP ๐ข))) |
36 | | ovex 7442 |
. . . . 5
โข (๐ฅ
ยทP ๐ง) โ V |
37 | | ovex 7442 |
. . . . 5
โข (๐ฅ
ยทP ๐ฃ) โ V |
38 | | ovex 7442 |
. . . . 5
โข (๐ฆ
ยทP ๐ค) โ V |
39 | | addcompr 11016 |
. . . . 5
โข (๐ +P
๐) = (๐ +P ๐) |
40 | | addasspr 11017 |
. . . . 5
โข ((๐ +P
๐)
+P โ) = (๐ +P (๐ +P
โ)) |
41 | | ovex 7442 |
. . . . 5
โข (๐ฆ
ยทP ๐ข) โ V |
42 | 36, 37, 38, 39, 40, 41 | caov4 7638 |
. . . 4
โข (((๐ฅ
ยทP ๐ง) +P (๐ฅ
ยทP ๐ฃ)) +P ((๐ฆ
ยทP ๐ค) +P (๐ฆ
ยทP ๐ข))) = (((๐ฅ ยทP ๐ง) +P
(๐ฆ
ยทP ๐ค)) +P ((๐ฅ
ยทP ๐ฃ) +P (๐ฆ
ยทP ๐ข))) |
43 | 35, 42 | eqtri 2761 |
. . 3
โข ((๐ฅ
ยทP (๐ง +P ๐ฃ)) +P
(๐ฆ
ยทP (๐ค +P ๐ข))) = (((๐ฅ ยทP ๐ง) +P
(๐ฆ
ยทP ๐ค)) +P ((๐ฅ
ยทP ๐ฃ) +P (๐ฆ
ยทP ๐ข))) |
44 | | distrpr 11023 |
. . . . 5
โข (๐ฅ
ยทP (๐ค +P ๐ข)) = ((๐ฅ ยทP ๐ค) +P
(๐ฅ
ยทP ๐ข)) |
45 | | distrpr 11023 |
. . . . 5
โข (๐ฆ
ยทP (๐ง +P ๐ฃ)) = ((๐ฆ ยทP ๐ง) +P
(๐ฆ
ยทP ๐ฃ)) |
46 | 44, 45 | oveq12i 7421 |
. . . 4
โข ((๐ฅ
ยทP (๐ค +P ๐ข)) +P
(๐ฆ
ยทP (๐ง +P ๐ฃ))) = (((๐ฅ ยทP ๐ค) +P
(๐ฅ
ยทP ๐ข)) +P ((๐ฆ
ยทP ๐ง) +P (๐ฆ
ยทP ๐ฃ))) |
47 | | ovex 7442 |
. . . . 5
โข (๐ฅ
ยทP ๐ค) โ V |
48 | | ovex 7442 |
. . . . 5
โข (๐ฅ
ยทP ๐ข) โ V |
49 | | ovex 7442 |
. . . . 5
โข (๐ฆ
ยทP ๐ง) โ V |
50 | | ovex 7442 |
. . . . 5
โข (๐ฆ
ยทP ๐ฃ) โ V |
51 | 47, 48, 49, 39, 40, 50 | caov4 7638 |
. . . 4
โข (((๐ฅ
ยทP ๐ค) +P (๐ฅ
ยทP ๐ข)) +P ((๐ฆ
ยทP ๐ง) +P (๐ฆ
ยทP ๐ฃ))) = (((๐ฅ ยทP ๐ค) +P
(๐ฆ
ยทP ๐ง)) +P ((๐ฅ
ยทP ๐ข) +P (๐ฆ
ยทP ๐ฃ))) |
52 | 46, 51 | eqtri 2761 |
. . 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 8819 |
. 2
โข ((๐ด โ R โง
๐ต โ R
โง ๐ถ โ
R) โ (๐ด
ยทR (๐ต +R ๐ถ)) = ((๐ด ยทR ๐ต) +R
(๐ด
ยทR ๐ถ))) |
54 | | dmaddsr 11080 |
. . 3
โข dom
+R = (R ร
R) |
55 | | 0nsr 11074 |
. . 3
โข ยฌ
โ
โ R |
56 | | dmmulsr 11081 |
. . 3
โข dom
ยทR = (R ร
R) |
57 | 54, 55, 56 | ndmovdistr 7596 |
. 2
โข (ยฌ
(๐ด โ R
โง ๐ต โ
R โง ๐ถ
โ R) โ (๐ด ยทR (๐ต +R
๐ถ)) = ((๐ด ยทR ๐ต) +R
(๐ด
ยทR ๐ถ))) |
58 | 53, 57 | pm2.61i 182 |
1
โข (๐ด
ยทR (๐ต +R ๐ถ)) = ((๐ด ยทR ๐ต) +R
(๐ด
ยทR ๐ถ)) |