Step | Hyp | Ref
| Expression |
1 | | dfcnqs 7839 |
. 2
โข โ =
((R ร R) / โก E ) |
2 | | mulcnsrec 7841 |
. 2
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R)) โ ([โจ๐ฅ, ๐ฆโฉ]โก E ยท [โจ๐ง, ๐คโฉ]โก E ) = [โจ((๐ฅ ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))), ((๐ฆ ยทR ๐ง) +R
(๐ฅ
ยทR ๐ค))โฉ]โก E ) |
3 | | mulcnsrec 7841 |
. 2
โข (((๐ง โ R โง
๐ค โ R)
โง (๐ฃ โ
R โง ๐ข
โ R)) โ ([โจ๐ง, ๐คโฉ]โก E ยท [โจ๐ฃ, ๐ขโฉ]โก E ) = [โจ((๐ง ยทR ๐ฃ) +R
(-1R ยทR (๐ค
ยทR ๐ข))), ((๐ค ยทR ๐ฃ) +R
(๐ง
ยทR ๐ข))โฉ]โก E ) |
4 | | mulcnsrec 7841 |
. 2
โข
(((((๐ฅ
ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))) โ R โง ((๐ฆ
ยทR ๐ง) +R (๐ฅ
ยทR ๐ค)) โ R) โง (๐ฃ โ R โง
๐ข โ R))
โ ([โจ((๐ฅ
ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))), ((๐ฆ ยทR ๐ง) +R
(๐ฅ
ยทR ๐ค))โฉ]โก E ยท [โจ๐ฃ, ๐ขโฉ]โก E ) = [โจ((((๐ฅ ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))) ยทR ๐ฃ) +R
(-1R ยทR (((๐ฆ
ยทR ๐ง) +R (๐ฅ
ยทR ๐ค)) ยทR ๐ข))), ((((๐ฆ ยทR ๐ง) +R
(๐ฅ
ยทR ๐ค)) ยทR ๐ฃ) +R
(((๐ฅ
ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))) ยทR ๐ข))โฉ]โก E ) |
5 | | mulcnsrec 7841 |
. 2
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (((๐ง
ยทR ๐ฃ) +R
(-1R ยทR (๐ค
ยทR ๐ข))) โ R โง ((๐ค
ยทR ๐ฃ) +R (๐ง
ยทR ๐ข)) โ R)) โ
([โจ๐ฅ, ๐ฆโฉ]โก E ยท [โจ((๐ง ยทR ๐ฃ) +R
(-1R ยทR (๐ค
ยทR ๐ข))), ((๐ค ยทR ๐ฃ) +R
(๐ง
ยทR ๐ข))โฉ]โก E ) = [โจ((๐ฅ ยทR ((๐ง
ยทR ๐ฃ) +R
(-1R ยทR (๐ค
ยทR ๐ข)))) +R
(-1R ยทR (๐ฆ
ยทR ((๐ค ยทR ๐ฃ) +R
(๐ง
ยทR ๐ข))))), ((๐ฆ ยทR ((๐ง
ยทR ๐ฃ) +R
(-1R ยทR (๐ค
ยทR ๐ข)))) +R (๐ฅ
ยทR ((๐ค ยทR ๐ฃ) +R
(๐ง
ยทR ๐ข))))โฉ]โก E ) |
6 | | mulclsr 7752 |
. . . . 5
โข ((๐ฅ โ R โง
๐ง โ R)
โ (๐ฅ
ยทR ๐ง) โ R) |
7 | | m1r 7750 |
. . . . . 6
โข
-1R โ R |
8 | | mulclsr 7752 |
. . . . . 6
โข ((๐ฆ โ R โง
๐ค โ R)
โ (๐ฆ
ยทR ๐ค) โ R) |
9 | | mulclsr 7752 |
. . . . . 6
โข
((-1R โ R โง (๐ฆ
ยทR ๐ค) โ R) โ
(-1R ยทR (๐ฆ
ยทR ๐ค)) โ R) |
10 | 7, 8, 9 | sylancr 414 |
. . . . 5
โข ((๐ฆ โ R โง
๐ค โ R)
โ (-1R ยทR (๐ฆ
ยทR ๐ค)) โ R) |
11 | | addclsr 7751 |
. . . . 5
โข (((๐ฅ
ยทR ๐ง) โ R โง
(-1R ยทR (๐ฆ
ยทR ๐ค)) โ R) โ ((๐ฅ
ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))) โ R) |
12 | 6, 10, 11 | syl2an 289 |
. . . 4
โข (((๐ฅ โ R โง
๐ง โ R)
โง (๐ฆ โ
R โง ๐ค
โ R)) โ ((๐ฅ ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))) โ R) |
13 | 12 | an4s 588 |
. . 3
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R)) โ ((๐ฅ ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))) โ R) |
14 | | mulclsr 7752 |
. . . . 5
โข ((๐ฆ โ R โง
๐ง โ R)
โ (๐ฆ
ยทR ๐ง) โ R) |
15 | | mulclsr 7752 |
. . . . 5
โข ((๐ฅ โ R โง
๐ค โ R)
โ (๐ฅ
ยทR ๐ค) โ R) |
16 | | addclsr 7751 |
. . . . 5
โข (((๐ฆ
ยทR ๐ง) โ R โง (๐ฅ
ยทR ๐ค) โ R) โ ((๐ฆ
ยทR ๐ง) +R (๐ฅ
ยทR ๐ค)) โ R) |
17 | 14, 15, 16 | syl2anr 290 |
. . . 4
โข (((๐ฅ โ R โง
๐ค โ R)
โง (๐ฆ โ
R โง ๐ง
โ R)) โ ((๐ฆ ยทR ๐ง) +R
(๐ฅ
ยทR ๐ค)) โ R) |
18 | 17 | an42s 589 |
. . 3
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R)) โ ((๐ฆ ยทR ๐ง) +R
(๐ฅ
ยทR ๐ค)) โ R) |
19 | 13, 18 | jca 306 |
. 2
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R)) โ (((๐ฅ ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))) โ R โง ((๐ฆ
ยทR ๐ง) +R (๐ฅ
ยทR ๐ค)) โ R)) |
20 | | mulclsr 7752 |
. . . . 5
โข ((๐ง โ R โง
๐ฃ โ R)
โ (๐ง
ยทR ๐ฃ) โ R) |
21 | | mulclsr 7752 |
. . . . . 6
โข ((๐ค โ R โง
๐ข โ R)
โ (๐ค
ยทR ๐ข) โ R) |
22 | | mulclsr 7752 |
. . . . . 6
โข
((-1R โ R โง (๐ค
ยทR ๐ข) โ R) โ
(-1R ยทR (๐ค
ยทR ๐ข)) โ R) |
23 | 7, 21, 22 | sylancr 414 |
. . . . 5
โข ((๐ค โ R โง
๐ข โ R)
โ (-1R ยทR (๐ค
ยทR ๐ข)) โ R) |
24 | | addclsr 7751 |
. . . . 5
โข (((๐ง
ยทR ๐ฃ) โ R โง
(-1R ยทR (๐ค
ยทR ๐ข)) โ R) โ ((๐ง
ยทR ๐ฃ) +R
(-1R ยทR (๐ค
ยทR ๐ข))) โ R) |
25 | 20, 23, 24 | syl2an 289 |
. . . 4
โข (((๐ง โ R โง
๐ฃ โ R)
โง (๐ค โ
R โง ๐ข
โ R)) โ ((๐ง ยทR ๐ฃ) +R
(-1R ยทR (๐ค
ยทR ๐ข))) โ R) |
26 | 25 | an4s 588 |
. . 3
โข (((๐ง โ R โง
๐ค โ R)
โง (๐ฃ โ
R โง ๐ข
โ R)) โ ((๐ง ยทR ๐ฃ) +R
(-1R ยทR (๐ค
ยทR ๐ข))) โ R) |
27 | | mulclsr 7752 |
. . . . 5
โข ((๐ค โ R โง
๐ฃ โ R)
โ (๐ค
ยทR ๐ฃ) โ R) |
28 | | mulclsr 7752 |
. . . . 5
โข ((๐ง โ R โง
๐ข โ R)
โ (๐ง
ยทR ๐ข) โ R) |
29 | | addclsr 7751 |
. . . . 5
โข (((๐ค
ยทR ๐ฃ) โ R โง (๐ง
ยทR ๐ข) โ R) โ ((๐ค
ยทR ๐ฃ) +R (๐ง
ยทR ๐ข)) โ R) |
30 | 27, 28, 29 | syl2anr 290 |
. . . 4
โข (((๐ง โ R โง
๐ข โ R)
โง (๐ค โ
R โง ๐ฃ
โ R)) โ ((๐ค ยทR ๐ฃ) +R
(๐ง
ยทR ๐ข)) โ R) |
31 | 30 | an42s 589 |
. . 3
โข (((๐ง โ R โง
๐ค โ R)
โง (๐ฃ โ
R โง ๐ข
โ R)) โ ((๐ค ยทR ๐ฃ) +R
(๐ง
ยทR ๐ข)) โ R) |
32 | 26, 31 | jca 306 |
. 2
โข (((๐ง โ R โง
๐ค โ R)
โง (๐ฃ โ
R โง ๐ข
โ R)) โ (((๐ง ยทR ๐ฃ) +R
(-1R ยทR (๐ค
ยทR ๐ข))) โ R โง ((๐ค
ยทR ๐ฃ) +R (๐ง
ยทR ๐ข)) โ R)) |
33 | | simp1l 1021 |
. . . . 5
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
๐ฅ โ
R) |
34 | | simp2l 1023 |
. . . . . 6
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
๐ง โ
R) |
35 | | simp3l 1025 |
. . . . . 6
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
๐ฃ โ
R) |
36 | 34, 35, 20 | syl2anc 411 |
. . . . 5
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(๐ง
ยทR ๐ฃ) โ R) |
37 | | mulclsr 7752 |
. . . . 5
โข ((๐ฅ โ R โง
(๐ง
ยทR ๐ฃ) โ R) โ (๐ฅ
ยทR (๐ง ยทR ๐ฃ)) โ
R) |
38 | 33, 36, 37 | syl2anc 411 |
. . . 4
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(๐ฅ
ยทR (๐ง ยทR ๐ฃ)) โ
R) |
39 | | simp2r 1024 |
. . . . . . 7
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
๐ค โ
R) |
40 | | simp3r 1026 |
. . . . . . 7
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
๐ข โ
R) |
41 | 39, 40, 21 | syl2anc 411 |
. . . . . 6
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(๐ค
ยทR ๐ข) โ R) |
42 | 7, 41, 22 | sylancr 414 |
. . . . 5
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(-1R ยทR (๐ค
ยทR ๐ข)) โ R) |
43 | | mulclsr 7752 |
. . . . 5
โข ((๐ฅ โ R โง
(-1R ยทR (๐ค
ยทR ๐ข)) โ R) โ (๐ฅ
ยทR (-1R
ยทR (๐ค ยทR ๐ข))) โ
R) |
44 | 33, 42, 43 | syl2anc 411 |
. . . 4
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(๐ฅ
ยทR (-1R
ยทR (๐ค ยทR ๐ข))) โ
R) |
45 | | simp1r 1022 |
. . . . . 6
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
๐ฆ โ
R) |
46 | 39, 35, 27 | syl2anc 411 |
. . . . . 6
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(๐ค
ยทR ๐ฃ) โ R) |
47 | | mulclsr 7752 |
. . . . . 6
โข ((๐ฆ โ R โง
(๐ค
ยทR ๐ฃ) โ R) โ (๐ฆ
ยทR (๐ค ยทR ๐ฃ)) โ
R) |
48 | 45, 46, 47 | syl2anc 411 |
. . . . 5
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(๐ฆ
ยทR (๐ค ยทR ๐ฃ)) โ
R) |
49 | | mulclsr 7752 |
. . . . 5
โข
((-1R โ R โง (๐ฆ
ยทR (๐ค ยทR ๐ฃ)) โ R)
โ (-1R ยทR (๐ฆ
ยทR (๐ค ยทR ๐ฃ))) โ
R) |
50 | 7, 48, 49 | sylancr 414 |
. . . 4
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(-1R ยทR (๐ฆ
ยทR (๐ค ยทR ๐ฃ))) โ
R) |
51 | | addcomsrg 7753 |
. . . . 5
โข ((๐ โ R โง
๐ โ R)
โ (๐
+R ๐) = (๐ +R ๐)) |
52 | 51 | adantl 277 |
. . . 4
โข ((((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โง
(๐ โ R
โง ๐ โ
R)) โ (๐
+R ๐) = (๐ +R ๐)) |
53 | | addasssrg 7754 |
. . . . 5
โข ((๐ โ R โง
๐ โ R
โง โ โ
R) โ ((๐
+R ๐) +R โ) = (๐ +R (๐ +R
โ))) |
54 | 53 | adantl 277 |
. . . 4
โข ((((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โง
(๐ โ R
โง ๐ โ
R โง โ
โ R)) โ ((๐ +R ๐) +R
โ) = (๐ +R (๐ +R
โ))) |
55 | 34, 40, 28 | syl2anc 411 |
. . . . . 6
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(๐ง
ยทR ๐ข) โ R) |
56 | | mulclsr 7752 |
. . . . . 6
โข ((๐ฆ โ R โง
(๐ง
ยทR ๐ข) โ R) โ (๐ฆ
ยทR (๐ง ยทR ๐ข)) โ
R) |
57 | 45, 55, 56 | syl2anc 411 |
. . . . 5
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(๐ฆ
ยทR (๐ง ยทR ๐ข)) โ
R) |
58 | | mulclsr 7752 |
. . . . 5
โข
((-1R โ R โง (๐ฆ
ยทR (๐ง ยทR ๐ข)) โ R)
โ (-1R ยทR (๐ฆ
ยทR (๐ง ยทR ๐ข))) โ
R) |
59 | 7, 57, 58 | sylancr 414 |
. . . 4
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(-1R ยทR (๐ฆ
ยทR (๐ง ยทR ๐ข))) โ
R) |
60 | | addclsr 7751 |
. . . . 5
โข ((๐ โ R โง
๐ โ R)
โ (๐
+R ๐) โ R) |
61 | 60 | adantl 277 |
. . . 4
โข ((((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โง
(๐ โ R
โง ๐ โ
R)) โ (๐
+R ๐) โ R) |
62 | 38, 44, 50, 52, 54, 59, 61 | caov42d 6060 |
. . 3
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(((๐ฅ
ยทR (๐ง ยทR ๐ฃ)) +R
(๐ฅ
ยทR (-1R
ยทR (๐ค ยทR ๐ข)))) +R
((-1R ยทR (๐ฆ
ยทR (๐ค ยทR ๐ฃ))) +R
(-1R ยทR (๐ฆ
ยทR (๐ง ยทR ๐ข))))) = (((๐ฅ ยทR (๐ง
ยทR ๐ฃ)) +R
(-1R ยทR (๐ฆ
ยทR (๐ค ยทR ๐ฃ)))) +R
((-1R ยทR (๐ฆ
ยทR (๐ง ยทR ๐ข))) +R
(๐ฅ
ยทR (-1R
ยทR (๐ค ยทR ๐ข)))))) |
63 | | distrsrg 7757 |
. . . . 5
โข ((๐ฅ โ R โง
(๐ง
ยทR ๐ฃ) โ R โง
(-1R ยทR (๐ค
ยทR ๐ข)) โ R) โ (๐ฅ
ยทR ((๐ง ยทR ๐ฃ) +R
(-1R ยทR (๐ค
ยทR ๐ข)))) = ((๐ฅ ยทR (๐ง
ยทR ๐ฃ)) +R (๐ฅ
ยทR (-1R
ยทR (๐ค ยทR ๐ข))))) |
64 | 33, 36, 42, 63 | syl3anc 1238 |
. . . 4
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(๐ฅ
ยทR ((๐ง ยทR ๐ฃ) +R
(-1R ยทR (๐ค
ยทR ๐ข)))) = ((๐ฅ ยทR (๐ง
ยทR ๐ฃ)) +R (๐ฅ
ยทR (-1R
ยทR (๐ค ยทR ๐ข))))) |
65 | | distrsrg 7757 |
. . . . . . 7
โข ((๐ฆ โ R โง
(๐ค
ยทR ๐ฃ) โ R โง (๐ง
ยทR ๐ข) โ R) โ (๐ฆ
ยทR ((๐ค ยทR ๐ฃ) +R
(๐ง
ยทR ๐ข))) = ((๐ฆ ยทR (๐ค
ยทR ๐ฃ)) +R (๐ฆ
ยทR (๐ง ยทR ๐ข)))) |
66 | 45, 46, 55, 65 | syl3anc 1238 |
. . . . . 6
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(๐ฆ
ยทR ((๐ค ยทR ๐ฃ) +R
(๐ง
ยทR ๐ข))) = ((๐ฆ ยทR (๐ค
ยทR ๐ฃ)) +R (๐ฆ
ยทR (๐ง ยทR ๐ข)))) |
67 | 66 | oveq2d 5890 |
. . . . 5
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(-1R ยทR (๐ฆ
ยทR ((๐ค ยทR ๐ฃ) +R
(๐ง
ยทR ๐ข)))) = (-1R
ยทR ((๐ฆ ยทR (๐ค
ยทR ๐ฃ)) +R (๐ฆ
ยทR (๐ง ยทR ๐ข))))) |
68 | 7 | a1i 9 |
. . . . . 6
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
-1R โ R) |
69 | | distrsrg 7757 |
. . . . . 6
โข
((-1R โ R โง (๐ฆ
ยทR (๐ค ยทR ๐ฃ)) โ R โง
(๐ฆ
ยทR (๐ง ยทR ๐ข)) โ R)
โ (-1R ยทR ((๐ฆ
ยทR (๐ค ยทR ๐ฃ)) +R
(๐ฆ
ยทR (๐ง ยทR ๐ข)))) =
((-1R ยทR (๐ฆ
ยทR (๐ค ยทR ๐ฃ))) +R
(-1R ยทR (๐ฆ
ยทR (๐ง ยทR ๐ข))))) |
70 | 68, 48, 57, 69 | syl3anc 1238 |
. . . . 5
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(-1R ยทR ((๐ฆ
ยทR (๐ค ยทR ๐ฃ)) +R
(๐ฆ
ยทR (๐ง ยทR ๐ข)))) =
((-1R ยทR (๐ฆ
ยทR (๐ค ยทR ๐ฃ))) +R
(-1R ยทR (๐ฆ
ยทR (๐ง ยทR ๐ข))))) |
71 | 67, 70 | eqtrd 2210 |
. . . 4
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(-1R ยทR (๐ฆ
ยทR ((๐ค ยทR ๐ฃ) +R
(๐ง
ยทR ๐ข)))) = ((-1R
ยทR (๐ฆ ยทR (๐ค
ยทR ๐ฃ))) +R
(-1R ยทR (๐ฆ
ยทR (๐ง ยทR ๐ข))))) |
72 | 64, 71 | oveq12d 5892 |
. . 3
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
((๐ฅ
ยทR ((๐ง ยทR ๐ฃ) +R
(-1R ยทR (๐ค
ยทR ๐ข)))) +R
(-1R ยทR (๐ฆ
ยทR ((๐ค ยทR ๐ฃ) +R
(๐ง
ยทR ๐ข))))) = (((๐ฅ ยทR (๐ง
ยทR ๐ฃ)) +R (๐ฅ
ยทR (-1R
ยทR (๐ค ยทR ๐ข)))) +R
((-1R ยทR (๐ฆ
ยทR (๐ค ยทR ๐ฃ))) +R
(-1R ยทR (๐ฆ
ยทR (๐ง ยทR ๐ข)))))) |
73 | | mulcomsrg 7755 |
. . . . . . 7
โข ((๐ โ R โง
๐ โ R)
โ (๐
ยทR ๐) = (๐ ยทR ๐)) |
74 | 73 | adantl 277 |
. . . . . 6
โข ((((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โง
(๐ โ R
โง ๐ โ
R)) โ (๐
ยทR ๐) = (๐ ยทR ๐)) |
75 | | distrsrg 7757 |
. . . . . . . . 9
โข ((โ โ R โง
๐ โ R
โง ๐ โ
R) โ (โ
ยทR (๐ +R ๐)) = ((โ ยทR ๐) +R
(โ
ยทR ๐))) |
76 | 75 | 3coml 1210 |
. . . . . . . 8
โข ((๐ โ R โง
๐ โ R
โง โ โ
R) โ (โ
ยทR (๐ +R ๐)) = ((โ ยทR ๐) +R
(โ
ยทR ๐))) |
77 | | simp3 999 |
. . . . . . . . 9
โข ((๐ โ R โง
๐ โ R
โง โ โ
R) โ โ
โ R) |
78 | 60 | 3adant3 1017 |
. . . . . . . . 9
โข ((๐ โ R โง
๐ โ R
โง โ โ
R) โ (๐
+R ๐) โ R) |
79 | | mulcomsrg 7755 |
. . . . . . . . 9
โข ((โ โ R โง
(๐
+R ๐) โ R) โ (โ
ยทR (๐ +R ๐)) = ((๐ +R ๐)
ยทR โ)) |
80 | 77, 78, 79 | syl2anc 411 |
. . . . . . . 8
โข ((๐ โ R โง
๐ โ R
โง โ โ
R) โ (โ
ยทR (๐ +R ๐)) = ((๐ +R ๐)
ยทR โ)) |
81 | | simp1 997 |
. . . . . . . . . 10
โข ((๐ โ R โง
๐ โ R
โง โ โ
R) โ ๐
โ R) |
82 | | mulcomsrg 7755 |
. . . . . . . . . 10
โข ((โ โ R โง
๐ โ R)
โ (โ
ยทR ๐) = (๐ ยทR โ)) |
83 | 77, 81, 82 | syl2anc 411 |
. . . . . . . . 9
โข ((๐ โ R โง
๐ โ R
โง โ โ
R) โ (โ
ยทR ๐) = (๐ ยทR โ)) |
84 | | simp2 998 |
. . . . . . . . . 10
โข ((๐ โ R โง
๐ โ R
โง โ โ
R) โ ๐
โ R) |
85 | | mulcomsrg 7755 |
. . . . . . . . . 10
โข ((โ โ R โง
๐ โ R)
โ (โ
ยทR ๐) = (๐ ยทR โ)) |
86 | 77, 84, 85 | syl2anc 411 |
. . . . . . . . 9
โข ((๐ โ R โง
๐ โ R
โง โ โ
R) โ (โ
ยทR ๐) = (๐ ยทR โ)) |
87 | 83, 86 | oveq12d 5892 |
. . . . . . . 8
โข ((๐ โ R โง
๐ โ R
โง โ โ
R) โ ((โ
ยทR ๐) +R (โ
ยทR ๐)) = ((๐ ยทR โ) +R
(๐
ยทR โ))) |
88 | 76, 80, 87 | 3eqtr3d 2218 |
. . . . . . 7
โข ((๐ โ R โง
๐ โ R
โง โ โ
R) โ ((๐
+R ๐) ยทR โ) = ((๐ ยทR โ) +R
(๐
ยทR โ))) |
89 | 88 | adantl 277 |
. . . . . 6
โข ((((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โง
(๐ โ R
โง ๐ โ
R โง โ
โ R)) โ ((๐ +R ๐)
ยทR โ) = ((๐ ยทR โ) +R
(๐
ยทR โ))) |
90 | | mulasssrg 7756 |
. . . . . . 7
โข ((๐ โ R โง
๐ โ R
โง โ โ
R) โ ((๐
ยทR ๐) ยทR โ) = (๐ ยทR (๐
ยทR โ))) |
91 | 90 | adantl 277 |
. . . . . 6
โข ((((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โง
(๐ โ R
โง ๐ โ
R โง โ
โ R)) โ ((๐ ยทR ๐)
ยทR โ) = (๐ ยทR (๐
ยทR โ))) |
92 | | mulclsr 7752 |
. . . . . . 7
โข ((๐ โ R โง
๐ โ R)
โ (๐
ยทR ๐) โ R) |
93 | 92 | adantl 277 |
. . . . . 6
โข ((((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โง
(๐ โ R
โง ๐ โ
R)) โ (๐
ยทR ๐) โ R) |
94 | 45, 39, 8 | syl2anc 411 |
. . . . . 6
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(๐ฆ
ยทR ๐ค) โ R) |
95 | 74, 89, 91, 93, 33, 68, 34, 94, 35 | caovdilemd 6065 |
. . . . 5
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(((๐ฅ
ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))) ยทR ๐ฃ) = ((๐ฅ ยทR (๐ง
ยทR ๐ฃ)) +R
(-1R ยทR ((๐ฆ
ยทR ๐ค) ยทR ๐ฃ)))) |
96 | | mulasssrg 7756 |
. . . . . . . 8
โข ((๐ฆ โ R โง
๐ค โ R
โง ๐ฃ โ
R) โ ((๐ฆ
ยทR ๐ค) ยทR ๐ฃ) = (๐ฆ ยทR (๐ค
ยทR ๐ฃ))) |
97 | 45, 39, 35, 96 | syl3anc 1238 |
. . . . . . 7
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
((๐ฆ
ยทR ๐ค) ยทR ๐ฃ) = (๐ฆ ยทR (๐ค
ยทR ๐ฃ))) |
98 | 97 | oveq2d 5890 |
. . . . . 6
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(-1R ยทR ((๐ฆ
ยทR ๐ค) ยทR ๐ฃ)) =
(-1R ยทR (๐ฆ
ยทR (๐ค ยทR ๐ฃ)))) |
99 | 98 | oveq2d 5890 |
. . . . 5
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
((๐ฅ
ยทR (๐ง ยทR ๐ฃ)) +R
(-1R ยทR ((๐ฆ
ยทR ๐ค) ยทR ๐ฃ))) = ((๐ฅ ยทR (๐ง
ยทR ๐ฃ)) +R
(-1R ยทR (๐ฆ
ยทR (๐ค ยทR ๐ฃ))))) |
100 | 95, 99 | eqtrd 2210 |
. . . 4
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(((๐ฅ
ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))) ยทR ๐ฃ) = ((๐ฅ ยทR (๐ง
ยทR ๐ฃ)) +R
(-1R ยทR (๐ฆ
ยทR (๐ค ยทR ๐ฃ))))) |
101 | 74, 89, 91, 93, 45, 33, 34, 39, 40 | caovdilemd 6065 |
. . . . . 6
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(((๐ฆ
ยทR ๐ง) +R (๐ฅ
ยทR ๐ค)) ยทR ๐ข) = ((๐ฆ ยทR (๐ง
ยทR ๐ข)) +R (๐ฅ
ยทR (๐ค ยทR ๐ข)))) |
102 | 101 | oveq2d 5890 |
. . . . 5
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(-1R ยทR (((๐ฆ
ยทR ๐ง) +R (๐ฅ
ยทR ๐ค)) ยทR ๐ข)) =
(-1R ยทR ((๐ฆ
ยทR (๐ง ยทR ๐ข)) +R
(๐ฅ
ยทR (๐ค ยทR ๐ข))))) |
103 | 93, 33, 41 | caovcld 6027 |
. . . . . 6
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(๐ฅ
ยทR (๐ค ยทR ๐ข)) โ
R) |
104 | | distrsrg 7757 |
. . . . . 6
โข
((-1R โ R โง (๐ฆ
ยทR (๐ง ยทR ๐ข)) โ R โง
(๐ฅ
ยทR (๐ค ยทR ๐ข)) โ R)
โ (-1R ยทR ((๐ฆ
ยทR (๐ง ยทR ๐ข)) +R
(๐ฅ
ยทR (๐ค ยทR ๐ข)))) =
((-1R ยทR (๐ฆ
ยทR (๐ง ยทR ๐ข))) +R
(-1R ยทR (๐ฅ
ยทR (๐ค ยทR ๐ข))))) |
105 | 68, 57, 103, 104 | syl3anc 1238 |
. . . . 5
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(-1R ยทR ((๐ฆ
ยทR (๐ง ยทR ๐ข)) +R
(๐ฅ
ยทR (๐ค ยทR ๐ข)))) =
((-1R ยทR (๐ฆ
ยทR (๐ง ยทR ๐ข))) +R
(-1R ยทR (๐ฅ
ยทR (๐ค ยทR ๐ข))))) |
106 | 68, 33, 41, 74, 91 | caov12d 6055 |
. . . . . 6
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(-1R ยทR (๐ฅ
ยทR (๐ค ยทR ๐ข))) = (๐ฅ ยทR
(-1R ยทR (๐ค
ยทR ๐ข)))) |
107 | 106 | oveq2d 5890 |
. . . . 5
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
((-1R ยทR (๐ฆ
ยทR (๐ง ยทR ๐ข))) +R
(-1R ยทR (๐ฅ
ยทR (๐ค ยทR ๐ข)))) =
((-1R ยทR (๐ฆ
ยทR (๐ง ยทR ๐ข))) +R
(๐ฅ
ยทR (-1R
ยทR (๐ค ยทR ๐ข))))) |
108 | 102, 105,
107 | 3eqtrd 2214 |
. . . 4
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(-1R ยทR (((๐ฆ
ยทR ๐ง) +R (๐ฅ
ยทR ๐ค)) ยทR ๐ข)) =
((-1R ยทR (๐ฆ
ยทR (๐ง ยทR ๐ข))) +R
(๐ฅ
ยทR (-1R
ยทR (๐ค ยทR ๐ข))))) |
109 | 100, 108 | oveq12d 5892 |
. . 3
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
((((๐ฅ
ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))) ยทR ๐ฃ) +R
(-1R ยทR (((๐ฆ
ยทR ๐ง) +R (๐ฅ
ยทR ๐ค)) ยทR ๐ข))) = (((๐ฅ ยทR (๐ง
ยทR ๐ฃ)) +R
(-1R ยทR (๐ฆ
ยทR (๐ค ยทR ๐ฃ)))) +R
((-1R ยทR (๐ฆ
ยทR (๐ง ยทR ๐ข))) +R
(๐ฅ
ยทR (-1R
ยทR (๐ค ยทR ๐ข)))))) |
110 | 62, 72, 109 | 3eqtr4rd 2221 |
. 2
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
((((๐ฅ
ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))) ยทR ๐ฃ) +R
(-1R ยทR (((๐ฆ
ยทR ๐ง) +R (๐ฅ
ยทR ๐ค)) ยทR ๐ข))) = ((๐ฅ ยทR ((๐ง
ยทR ๐ฃ) +R
(-1R ยทR (๐ค
ยทR ๐ข)))) +R
(-1R ยทR (๐ฆ
ยทR ((๐ค ยทR ๐ฃ) +R
(๐ง
ยทR ๐ข)))))) |
111 | 93, 45, 36 | caovcld 6027 |
. . . 4
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(๐ฆ
ยทR (๐ง ยทR ๐ฃ)) โ
R) |
112 | 93, 45, 42 | caovcld 6027 |
. . . 4
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(๐ฆ
ยทR (-1R
ยทR (๐ค ยทR ๐ข))) โ
R) |
113 | 93, 33, 46 | caovcld 6027 |
. . . 4
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(๐ฅ
ยทR (๐ค ยทR ๐ฃ)) โ
R) |
114 | 93, 33, 55 | caovcld 6027 |
. . . 4
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(๐ฅ
ยทR (๐ง ยทR ๐ข)) โ
R) |
115 | 111, 112,
113, 52, 54, 114, 61 | caov42d 6060 |
. . 3
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(((๐ฆ
ยทR (๐ง ยทR ๐ฃ)) +R
(๐ฆ
ยทR (-1R
ยทR (๐ค ยทR ๐ข)))) +R
((๐ฅ
ยทR (๐ค ยทR ๐ฃ)) +R
(๐ฅ
ยทR (๐ง ยทR ๐ข)))) = (((๐ฆ ยทR (๐ง
ยทR ๐ฃ)) +R (๐ฅ
ยทR (๐ค ยทR ๐ฃ))) +R
((๐ฅ
ยทR (๐ง ยทR ๐ข)) +R
(๐ฆ
ยทR (-1R
ยทR (๐ค ยทR ๐ข)))))) |
116 | | distrsrg 7757 |
. . . . 5
โข ((๐ฆ โ R โง
(๐ง
ยทR ๐ฃ) โ R โง
(-1R ยทR (๐ค
ยทR ๐ข)) โ R) โ (๐ฆ
ยทR ((๐ง ยทR ๐ฃ) +R
(-1R ยทR (๐ค
ยทR ๐ข)))) = ((๐ฆ ยทR (๐ง
ยทR ๐ฃ)) +R (๐ฆ
ยทR (-1R
ยทR (๐ค ยทR ๐ข))))) |
117 | 45, 36, 42, 116 | syl3anc 1238 |
. . . 4
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(๐ฆ
ยทR ((๐ง ยทR ๐ฃ) +R
(-1R ยทR (๐ค
ยทR ๐ข)))) = ((๐ฆ ยทR (๐ง
ยทR ๐ฃ)) +R (๐ฆ
ยทR (-1R
ยทR (๐ค ยทR ๐ข))))) |
118 | | distrsrg 7757 |
. . . . 5
โข ((๐ฅ โ R โง
(๐ค
ยทR ๐ฃ) โ R โง (๐ง
ยทR ๐ข) โ R) โ (๐ฅ
ยทR ((๐ค ยทR ๐ฃ) +R
(๐ง
ยทR ๐ข))) = ((๐ฅ ยทR (๐ค
ยทR ๐ฃ)) +R (๐ฅ
ยทR (๐ง ยทR ๐ข)))) |
119 | 33, 46, 55, 118 | syl3anc 1238 |
. . . 4
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(๐ฅ
ยทR ((๐ค ยทR ๐ฃ) +R
(๐ง
ยทR ๐ข))) = ((๐ฅ ยทR (๐ค
ยทR ๐ฃ)) +R (๐ฅ
ยทR (๐ง ยทR ๐ข)))) |
120 | 117, 119 | oveq12d 5892 |
. . 3
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
((๐ฆ
ยทR ((๐ง ยทR ๐ฃ) +R
(-1R ยทR (๐ค
ยทR ๐ข)))) +R (๐ฅ
ยทR ((๐ค ยทR ๐ฃ) +R
(๐ง
ยทR ๐ข)))) = (((๐ฆ ยทR (๐ง
ยทR ๐ฃ)) +R (๐ฆ
ยทR (-1R
ยทR (๐ค ยทR ๐ข)))) +R
((๐ฅ
ยทR (๐ค ยทR ๐ฃ)) +R
(๐ฅ
ยทR (๐ง ยทR ๐ข))))) |
121 | 74, 89, 91, 93, 45, 33, 34, 39, 35 | caovdilemd 6065 |
. . . 4
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(((๐ฆ
ยทR ๐ง) +R (๐ฅ
ยทR ๐ค)) ยทR ๐ฃ) = ((๐ฆ ยทR (๐ง
ยทR ๐ฃ)) +R (๐ฅ
ยทR (๐ค ยทR ๐ฃ)))) |
122 | 74, 89, 91, 93, 33, 68, 34, 94, 40 | caovdilemd 6065 |
. . . . 5
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(((๐ฅ
ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))) ยทR ๐ข) = ((๐ฅ ยทR (๐ง
ยทR ๐ข)) +R
(-1R ยทR ((๐ฆ
ยทR ๐ค) ยทR ๐ข)))) |
123 | | mulasssrg 7756 |
. . . . . . . . 9
โข ((๐ฆ โ R โง
๐ค โ R
โง ๐ข โ
R) โ ((๐ฆ
ยทR ๐ค) ยทR ๐ข) = (๐ฆ ยทR (๐ค
ยทR ๐ข))) |
124 | 45, 39, 40, 123 | syl3anc 1238 |
. . . . . . . 8
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
((๐ฆ
ยทR ๐ค) ยทR ๐ข) = (๐ฆ ยทR (๐ค
ยทR ๐ข))) |
125 | 124 | oveq2d 5890 |
. . . . . . 7
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(-1R ยทR ((๐ฆ
ยทR ๐ค) ยทR ๐ข)) =
(-1R ยทR (๐ฆ
ยทR (๐ค ยทR ๐ข)))) |
126 | 68, 45, 41, 74, 91 | caov12d 6055 |
. . . . . . 7
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(-1R ยทR (๐ฆ
ยทR (๐ค ยทR ๐ข))) = (๐ฆ ยทR
(-1R ยทR (๐ค
ยทR ๐ข)))) |
127 | 125, 126 | eqtrd 2210 |
. . . . . 6
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(-1R ยทR ((๐ฆ
ยทR ๐ค) ยทR ๐ข)) = (๐ฆ ยทR
(-1R ยทR (๐ค
ยทR ๐ข)))) |
128 | 127 | oveq2d 5890 |
. . . . 5
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
((๐ฅ
ยทR (๐ง ยทR ๐ข)) +R
(-1R ยทR ((๐ฆ
ยทR ๐ค) ยทR ๐ข))) = ((๐ฅ ยทR (๐ง
ยทR ๐ข)) +R (๐ฆ
ยทR (-1R
ยทR (๐ค ยทR ๐ข))))) |
129 | 122, 128 | eqtrd 2210 |
. . . 4
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
(((๐ฅ
ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))) ยทR ๐ข) = ((๐ฅ ยทR (๐ง
ยทR ๐ข)) +R (๐ฆ
ยทR (-1R
ยทR (๐ค ยทR ๐ข))))) |
130 | 121, 129 | oveq12d 5892 |
. . 3
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
((((๐ฆ
ยทR ๐ง) +R (๐ฅ
ยทR ๐ค)) ยทR ๐ฃ) +R
(((๐ฅ
ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))) ยทR ๐ข)) = (((๐ฆ ยทR (๐ง
ยทR ๐ฃ)) +R (๐ฅ
ยทR (๐ค ยทR ๐ฃ))) +R
((๐ฅ
ยทR (๐ง ยทR ๐ข)) +R
(๐ฆ
ยทR (-1R
ยทR (๐ค ยทR ๐ข)))))) |
131 | 115, 120,
130 | 3eqtr4rd 2221 |
. 2
โข (((๐ฅ โ R โง
๐ฆ โ R)
โง (๐ง โ
R โง ๐ค
โ R) โง (๐ฃ โ R โง ๐ข โ R)) โ
((((๐ฆ
ยทR ๐ง) +R (๐ฅ
ยทR ๐ค)) ยทR ๐ฃ) +R
(((๐ฅ
ยทR ๐ง) +R
(-1R ยทR (๐ฆ
ยทR ๐ค))) ยทR ๐ข)) = ((๐ฆ ยทR ((๐ง
ยทR ๐ฃ) +R
(-1R ยทR (๐ค
ยทR ๐ข)))) +R (๐ฅ
ยทR ((๐ค ยทR ๐ฃ) +R
(๐ง
ยทR ๐ข))))) |
132 | 1, 2, 3, 4, 5, 19,
32, 110, 131 | ecoviass 6644 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด ยท ๐ต) ยท ๐ถ) = (๐ด ยท (๐ต ยท ๐ถ))) |