Step | Hyp | Ref
| Expression |
1 | | dfcnqs 11085 |
. 2
โข โ =
((R ร R) / โก E ) |
2 | | addcnsrec 11086 |
. 2
โข (((๐ง โ R โง
๐ค โ R)
โง (๐ฃ โ
R โง ๐ข
โ R)) โ ([โจ๐ง, ๐คโฉ]โก E + [โจ๐ฃ, ๐ขโฉ]โก E ) = [โจ(๐ง +R ๐ฃ), (๐ค +R ๐ข)โฉ]โก E ) |
3 | | mulcnsrec 11087 |
. 2
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง ((๐ง
+R ๐ฃ) โ R โง (๐ค +R
๐ข) โ R))
โ ([โจ๐ฅ, ๐ฆโฉ]โก E ยท [โจ(๐ง +R ๐ฃ), (๐ค +R ๐ข)โฉ]โก E ) = [โจ((๐ฅ ยทR (๐ง +R
๐ฃ))
+R (-1R
ยทR (๐ฆ ยทR (๐ค +R
๐ข)))), ((๐ฆ ยทR (๐ง +R
๐ฃ))
+R (๐ฅ ยทR (๐ค +R
๐ข)))โฉ]โก E ) |
4 | | mulcnsrec 11087 |
. 2
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R)) โ ([โจ๐ฅ, ๐ฆโฉ]โก E ยท [โจ๐ง, ๐คโฉ]โก E ) = [โจ((๐ฅ ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))), ((๐ฆ ยทR ๐ง) +R
(๐ฅ
ยทR ๐ค))โฉ]โก E ) |
5 | | mulcnsrec 11087 |
. 2
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ฃ โ
R โง ๐ข
โ R)) โ ([โจ๐ฅ, ๐ฆโฉ]โก E ยท [โจ๐ฃ, ๐ขโฉ]โก E ) = [โจ((๐ฅ ยทR ๐ฃ) +R
(-1R ยทR (๐ฆ
ยทR ๐ข))), ((๐ฆ ยทR ๐ฃ) +R
(๐ฅ
ยทR ๐ข))โฉ]โก E ) |
6 | | addcnsrec 11086 |
. 2
โข
(((((๐ฅ
ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))) โ R โง ((๐ฆ
ยทR ๐ง) +R (๐ฅ
ยทR ๐ค)) โ R) โง (((๐ฅ
ยทR ๐ฃ) +R
(-1R ยทR (๐ฆ
ยทR ๐ข))) โ R โง ((๐ฆ
ยทR ๐ฃ) +R (๐ฅ
ยทR ๐ข)) โ R)) โ
([โจ((๐ฅ
ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))), ((๐ฆ ยทR ๐ง) +R
(๐ฅ
ยทR ๐ค))โฉ]โก E + [โจ((๐ฅ ยทR ๐ฃ) +R
(-1R ยทR (๐ฆ
ยทR ๐ข))), ((๐ฆ ยทR ๐ฃ) +R
(๐ฅ
ยทR ๐ข))โฉ]โก E ) = [โจ(((๐ฅ ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))) +R ((๐ฅ
ยทR ๐ฃ) +R
(-1R ยทR (๐ฆ
ยทR ๐ข)))), (((๐ฆ ยทR ๐ง) +R
(๐ฅ
ยทR ๐ค)) +R ((๐ฆ
ยทR ๐ฃ) +R (๐ฅ
ยทR ๐ข)))โฉ]โก E ) |
7 | | addclsr 11026 |
. . . 4
โข ((๐ง โ R โง
๐ฃ โ R)
โ (๐ง
+R ๐ฃ) โ R) |
8 | | addclsr 11026 |
. . . 4
โข ((๐ค โ R โง
๐ข โ R)
โ (๐ค
+R ๐ข) โ R) |
9 | 7, 8 | anim12i 614 |
. . 3
โข (((๐ง โ R โง
๐ฃ โ R)
โง (๐ค โ
R โง ๐ข
โ R)) โ ((๐ง +R ๐ฃ) โ R โง
(๐ค
+R ๐ข) โ R)) |
10 | 9 | an4s 659 |
. 2
โข (((๐ง โ R โง
๐ค โ R)
โง (๐ฃ โ
R โง ๐ข
โ R)) โ ((๐ง +R ๐ฃ) โ R โง
(๐ค
+R ๐ข) โ R)) |
11 | | mulclsr 11027 |
. . . . 5
โข ((๐ฅ โ R โง
๐ง โ R)
โ (๐ฅ
ยทR ๐ง) โ R) |
12 | | m1r 11025 |
. . . . . 6
โข
-1R โ R |
13 | | mulclsr 11027 |
. . . . . 6
โข ((๐ฆ โ R โง
๐ค โ R)
โ (๐ฆ
ยทR ๐ค) โ R) |
14 | | mulclsr 11027 |
. . . . . 6
โข
((-1R โ R โง (๐ฆ
ยทR ๐ค) โ R) โ
(-1R ยทR (๐ฆ
ยทR ๐ค)) โ R) |
15 | 12, 13, 14 | sylancr 588 |
. . . . 5
โข ((๐ฆ โ R โง
๐ค โ R)
โ (-1R ยทR (๐ฆ
ยทR ๐ค)) โ R) |
16 | | addclsr 11026 |
. . . . 5
โข (((๐ฅ
ยทR ๐ง) โ R โง
(-1R ยทR (๐ฆ
ยทR ๐ค)) โ R) โ ((๐ฅ
ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))) โ R) |
17 | 11, 15, 16 | syl2an 597 |
. . . 4
โข (((๐ฅ โ R โง
๐ง โ R)
โง (๐ฆ โ
R โง ๐ค
โ R)) โ ((๐ฅ ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))) โ R) |
18 | 17 | an4s 659 |
. . 3
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R)) โ ((๐ฅ ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))) โ R) |
19 | | mulclsr 11027 |
. . . . 5
โข ((๐ฆ โ R โง
๐ง โ R)
โ (๐ฆ
ยทR ๐ง) โ R) |
20 | | mulclsr 11027 |
. . . . 5
โข ((๐ฅ โ R โง
๐ค โ R)
โ (๐ฅ
ยทR ๐ค) โ R) |
21 | | addclsr 11026 |
. . . . 5
โข (((๐ฆ
ยทR ๐ง) โ R โง (๐ฅ
ยทR ๐ค) โ R) โ ((๐ฆ
ยทR ๐ง) +R (๐ฅ
ยทR ๐ค)) โ R) |
22 | 19, 20, 21 | syl2anr 598 |
. . . 4
โข (((๐ฅ โ R โง
๐ค โ R)
โง (๐ฆ โ
R โง ๐ง
โ R)) โ ((๐ฆ ยทR ๐ง) +R
(๐ฅ
ยทR ๐ค)) โ R) |
23 | 22 | an42s 660 |
. . 3
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R)) โ ((๐ฆ ยทR ๐ง) +R
(๐ฅ
ยทR ๐ค)) โ R) |
24 | 18, 23 | jca 513 |
. 2
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R)) โ (((๐ฅ ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))) โ R โง ((๐ฆ
ยทR ๐ง) +R (๐ฅ
ยทR ๐ค)) โ R)) |
25 | | mulclsr 11027 |
. . . . 5
โข ((๐ฅ โ R โง
๐ฃ โ R)
โ (๐ฅ
ยทR ๐ฃ) โ R) |
26 | | mulclsr 11027 |
. . . . . 6
โข ((๐ฆ โ R โง
๐ข โ R)
โ (๐ฆ
ยทR ๐ข) โ R) |
27 | | mulclsr 11027 |
. . . . . 6
โข
((-1R โ R โง (๐ฆ
ยทR ๐ข) โ R) โ
(-1R ยทR (๐ฆ
ยทR ๐ข)) โ R) |
28 | 12, 26, 27 | sylancr 588 |
. . . . 5
โข ((๐ฆ โ R โง
๐ข โ R)
โ (-1R ยทR (๐ฆ
ยทR ๐ข)) โ R) |
29 | | addclsr 11026 |
. . . . 5
โข (((๐ฅ
ยทR ๐ฃ) โ R โง
(-1R ยทR (๐ฆ
ยทR ๐ข)) โ R) โ ((๐ฅ
ยทR ๐ฃ) +R
(-1R ยทR (๐ฆ
ยทR ๐ข))) โ R) |
30 | 25, 28, 29 | syl2an 597 |
. . . 4
โข (((๐ฅ โ R โง
๐ฃ โ R)
โง (๐ฆ โ
R โง ๐ข
โ R)) โ ((๐ฅ ยทR ๐ฃ) +R
(-1R ยทR (๐ฆ
ยทR ๐ข))) โ R) |
31 | 30 | an4s 659 |
. . 3
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ฃ โ
R โง ๐ข
โ R)) โ ((๐ฅ ยทR ๐ฃ) +R
(-1R ยทR (๐ฆ
ยทR ๐ข))) โ R) |
32 | | mulclsr 11027 |
. . . . 5
โข ((๐ฆ โ R โง
๐ฃ โ R)
โ (๐ฆ
ยทR ๐ฃ) โ R) |
33 | | mulclsr 11027 |
. . . . 5
โข ((๐ฅ โ R โง
๐ข โ R)
โ (๐ฅ
ยทR ๐ข) โ R) |
34 | | addclsr 11026 |
. . . . 5
โข (((๐ฆ
ยทR ๐ฃ) โ R โง (๐ฅ
ยทR ๐ข) โ R) โ ((๐ฆ
ยทR ๐ฃ) +R (๐ฅ
ยทR ๐ข)) โ R) |
35 | 32, 33, 34 | syl2anr 598 |
. . . 4
โข (((๐ฅ โ R โง
๐ข โ R)
โง (๐ฆ โ
R โง ๐ฃ
โ R)) โ ((๐ฆ ยทR ๐ฃ) +R
(๐ฅ
ยทR ๐ข)) โ R) |
36 | 35 | an42s 660 |
. . 3
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ฃ โ
R โง ๐ข
โ R)) โ ((๐ฆ ยทR ๐ฃ) +R
(๐ฅ
ยทR ๐ข)) โ R) |
37 | 31, 36 | jca 513 |
. 2
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ฃ โ
R โง ๐ข
โ R)) โ (((๐ฅ ยทR ๐ฃ) +R
(-1R ยทR (๐ฆ
ยทR ๐ข))) โ R โง ((๐ฆ
ยทR ๐ฃ) +R (๐ฅ
ยทR ๐ข)) โ R)) |
38 | | distrsr 11034 |
. . . 4
โข (๐ฅ
ยทR (๐ง +R ๐ฃ)) = ((๐ฅ ยทR ๐ง) +R
(๐ฅ
ยทR ๐ฃ)) |
39 | | distrsr 11034 |
. . . . . 6
โข (๐ฆ
ยทR (๐ค +R ๐ข)) = ((๐ฆ ยทR ๐ค) +R
(๐ฆ
ยทR ๐ข)) |
40 | 39 | oveq2i 7373 |
. . . . 5
โข
(-1R ยทR (๐ฆ
ยทR (๐ค +R ๐ข))) =
(-1R ยทR ((๐ฆ
ยทR ๐ค) +R (๐ฆ
ยทR ๐ข))) |
41 | | distrsr 11034 |
. . . . 5
โข
(-1R ยทR ((๐ฆ
ยทR ๐ค) +R (๐ฆ
ยทR ๐ข))) = ((-1R
ยทR (๐ฆ ยทR ๐ค)) +R
(-1R ยทR (๐ฆ
ยทR ๐ข))) |
42 | 40, 41 | eqtri 2765 |
. . . 4
โข
(-1R ยทR (๐ฆ
ยทR (๐ค +R ๐ข))) =
((-1R ยทR (๐ฆ
ยทR ๐ค)) +R
(-1R ยทR (๐ฆ
ยทR ๐ข))) |
43 | 38, 42 | oveq12i 7374 |
. . 3
โข ((๐ฅ
ยทR (๐ง +R ๐ฃ)) +R
(-1R ยทR (๐ฆ
ยทR (๐ค +R ๐ข)))) = (((๐ฅ ยทR ๐ง) +R
(๐ฅ
ยทR ๐ฃ)) +R
((-1R ยทR (๐ฆ
ยทR ๐ค)) +R
(-1R ยทR (๐ฆ
ยทR ๐ข)))) |
44 | | ovex 7395 |
. . . 4
โข (๐ฅ
ยทR ๐ง) โ V |
45 | | ovex 7395 |
. . . 4
โข (๐ฅ
ยทR ๐ฃ) โ V |
46 | | ovex 7395 |
. . . 4
โข
(-1R ยทR (๐ฆ
ยทR ๐ค)) โ V |
47 | | addcomsr 11030 |
. . . 4
โข (๐ +R
๐) = (๐ +R ๐) |
48 | | addasssr 11031 |
. . . 4
โข ((๐ +R
๐)
+R โ) = (๐ +R (๐ +R
โ)) |
49 | | ovex 7395 |
. . . 4
โข
(-1R ยทR (๐ฆ
ยทR ๐ข)) โ V |
50 | 44, 45, 46, 47, 48, 49 | caov4 7590 |
. . 3
โข (((๐ฅ
ยทR ๐ง) +R (๐ฅ
ยทR ๐ฃ)) +R
((-1R ยทR (๐ฆ
ยทR ๐ค)) +R
(-1R ยทR (๐ฆ
ยทR ๐ข)))) = (((๐ฅ ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))) +R ((๐ฅ
ยทR ๐ฃ) +R
(-1R ยทR (๐ฆ
ยทR ๐ข)))) |
51 | 43, 50 | eqtri 2765 |
. 2
โข ((๐ฅ
ยทR (๐ง +R ๐ฃ)) +R
(-1R ยทR (๐ฆ
ยทR (๐ค +R ๐ข)))) = (((๐ฅ ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))) +R ((๐ฅ
ยทR ๐ฃ) +R
(-1R ยทR (๐ฆ
ยทR ๐ข)))) |
52 | | distrsr 11034 |
. . . 4
โข (๐ฆ
ยทR (๐ง +R ๐ฃ)) = ((๐ฆ ยทR ๐ง) +R
(๐ฆ
ยทR ๐ฃ)) |
53 | | distrsr 11034 |
. . . 4
โข (๐ฅ
ยทR (๐ค +R ๐ข)) = ((๐ฅ ยทR ๐ค) +R
(๐ฅ
ยทR ๐ข)) |
54 | 52, 53 | oveq12i 7374 |
. . 3
โข ((๐ฆ
ยทR (๐ง +R ๐ฃ)) +R
(๐ฅ
ยทR (๐ค +R ๐ข))) = (((๐ฆ ยทR ๐ง) +R
(๐ฆ
ยทR ๐ฃ)) +R ((๐ฅ
ยทR ๐ค) +R (๐ฅ
ยทR ๐ข))) |
55 | | ovex 7395 |
. . . 4
โข (๐ฆ
ยทR ๐ง) โ V |
56 | | ovex 7395 |
. . . 4
โข (๐ฆ
ยทR ๐ฃ) โ V |
57 | | ovex 7395 |
. . . 4
โข (๐ฅ
ยทR ๐ค) โ V |
58 | | ovex 7395 |
. . . 4
โข (๐ฅ
ยทR ๐ข) โ V |
59 | 55, 56, 57, 47, 48, 58 | caov4 7590 |
. . 3
โข (((๐ฆ
ยทR ๐ง) +R (๐ฆ
ยทR ๐ฃ)) +R ((๐ฅ
ยทR ๐ค) +R (๐ฅ
ยทR ๐ข))) = (((๐ฆ ยทR ๐ง) +R
(๐ฅ
ยทR ๐ค)) +R ((๐ฆ
ยทR ๐ฃ) +R (๐ฅ
ยทR ๐ข))) |
60 | 54, 59 | eqtri 2765 |
. 2
โข ((๐ฆ
ยทR (๐ง +R ๐ฃ)) +R
(๐ฅ
ยทR (๐ค +R ๐ข))) = (((๐ฆ ยทR ๐ง) +R
(๐ฅ
ยทR ๐ค)) +R ((๐ฆ
ยทR ๐ฃ) +R (๐ฅ
ยทR ๐ข))) |
61 | 1, 2, 3, 4, 5, 6, 10, 24, 37, 51, 60 | ecovdi 8771 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด ยท (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ))) |