Step | Hyp | Ref
| Expression |
1 | | addasspi 10838 |
. . . . . . . 8
โข
((((1st โ๐ด) ยทN
((2nd โ๐ต)
ยทN (2nd โ๐ถ))) +N
(((1st โ๐ต)
ยทN (2nd โ๐ด)) ยทN
(2nd โ๐ถ)))
+N ((1st โ๐ถ) ยทN
((2nd โ๐ด)
ยทN (2nd โ๐ต)))) = (((1st โ๐ด)
ยทN ((2nd โ๐ต) ยทN
(2nd โ๐ถ)))
+N ((((1st โ๐ต) ยทN
(2nd โ๐ด))
ยทN (2nd โ๐ถ)) +N
((1st โ๐ถ)
ยทN ((2nd โ๐ด) ยทN
(2nd โ๐ต))))) |
2 | | ovex 7395 |
. . . . . . . . . . 11
โข
((1st โ๐ด) ยทN
(2nd โ๐ต))
โ V |
3 | | ovex 7395 |
. . . . . . . . . . 11
โข
((1st โ๐ต) ยทN
(2nd โ๐ด))
โ V |
4 | | fvex 6860 |
. . . . . . . . . . 11
โข
(2nd โ๐ถ) โ V |
5 | | mulcompi 10839 |
. . . . . . . . . . 11
โข (๐ฅ
ยทN ๐ฆ) = (๐ฆ ยทN ๐ฅ) |
6 | | distrpi 10841 |
. . . . . . . . . . 11
โข (๐ฅ
ยทN (๐ฆ +N ๐ง)) = ((๐ฅ ยทN ๐ฆ) +N
(๐ฅ
ยทN ๐ง)) |
7 | 2, 3, 4, 5, 6 | caovdir 7593 |
. . . . . . . . . 10
โข
((((1st โ๐ด) ยทN
(2nd โ๐ต))
+N ((1st โ๐ต) ยทN
(2nd โ๐ด)))
ยทN (2nd โ๐ถ)) = ((((1st โ๐ด)
ยทN (2nd โ๐ต)) ยทN
(2nd โ๐ถ))
+N (((1st โ๐ต) ยทN
(2nd โ๐ด))
ยทN (2nd โ๐ถ))) |
8 | | mulasspi 10840 |
. . . . . . . . . . 11
โข
(((1st โ๐ด) ยทN
(2nd โ๐ต))
ยทN (2nd โ๐ถ)) = ((1st โ๐ด)
ยทN ((2nd โ๐ต) ยทN
(2nd โ๐ถ))) |
9 | 8 | oveq1i 7372 |
. . . . . . . . . 10
โข
((((1st โ๐ด) ยทN
(2nd โ๐ต))
ยทN (2nd โ๐ถ)) +N
(((1st โ๐ต)
ยทN (2nd โ๐ด)) ยทN
(2nd โ๐ถ)))
= (((1st โ๐ด) ยทN
((2nd โ๐ต)
ยทN (2nd โ๐ถ))) +N
(((1st โ๐ต)
ยทN (2nd โ๐ด)) ยทN
(2nd โ๐ถ))) |
10 | 7, 9 | eqtri 2765 |
. . . . . . . . 9
โข
((((1st โ๐ด) ยทN
(2nd โ๐ต))
+N ((1st โ๐ต) ยทN
(2nd โ๐ด)))
ยทN (2nd โ๐ถ)) = (((1st โ๐ด)
ยทN ((2nd โ๐ต) ยทN
(2nd โ๐ถ)))
+N (((1st โ๐ต) ยทN
(2nd โ๐ด))
ยทN (2nd โ๐ถ))) |
11 | 10 | oveq1i 7372 |
. . . . . . . 8
โข
(((((1st โ๐ด) ยทN
(2nd โ๐ต))
+N ((1st โ๐ต) ยทN
(2nd โ๐ด)))
ยทN (2nd โ๐ถ)) +N
((1st โ๐ถ)
ยทN ((2nd โ๐ด) ยทN
(2nd โ๐ต)))) = ((((1st โ๐ด)
ยทN ((2nd โ๐ต) ยทN
(2nd โ๐ถ)))
+N (((1st โ๐ต) ยทN
(2nd โ๐ด))
ยทN (2nd โ๐ถ))) +N
((1st โ๐ถ)
ยทN ((2nd โ๐ด) ยทN
(2nd โ๐ต)))) |
12 | | ovex 7395 |
. . . . . . . . . . 11
โข
((1st โ๐ต) ยทN
(2nd โ๐ถ))
โ V |
13 | | ovex 7395 |
. . . . . . . . . . 11
โข
((1st โ๐ถ) ยทN
(2nd โ๐ต))
โ V |
14 | | fvex 6860 |
. . . . . . . . . . 11
โข
(2nd โ๐ด) โ V |
15 | 12, 13, 14, 5, 6 | caovdir 7593 |
. . . . . . . . . 10
โข
((((1st โ๐ต) ยทN
(2nd โ๐ถ))
+N ((1st โ๐ถ) ยทN
(2nd โ๐ต)))
ยทN (2nd โ๐ด)) = ((((1st โ๐ต)
ยทN (2nd โ๐ถ)) ยทN
(2nd โ๐ด))
+N (((1st โ๐ถ) ยทN
(2nd โ๐ต))
ยทN (2nd โ๐ด))) |
16 | | fvex 6860 |
. . . . . . . . . . . 12
โข
(1st โ๐ต) โ V |
17 | | mulasspi 10840 |
. . . . . . . . . . . 12
โข ((๐ฅ
ยทN ๐ฆ) ยทN ๐ง) = (๐ฅ ยทN (๐ฆ
ยทN ๐ง)) |
18 | 16, 4, 14, 5, 17 | caov32 7586 |
. . . . . . . . . . 11
โข
(((1st โ๐ต) ยทN
(2nd โ๐ถ))
ยทN (2nd โ๐ด)) = (((1st โ๐ต)
ยทN (2nd โ๐ด)) ยทN
(2nd โ๐ถ)) |
19 | | mulasspi 10840 |
. . . . . . . . . . . 12
โข
(((1st โ๐ถ) ยทN
(2nd โ๐ต))
ยทN (2nd โ๐ด)) = ((1st โ๐ถ)
ยทN ((2nd โ๐ต) ยทN
(2nd โ๐ด))) |
20 | | mulcompi 10839 |
. . . . . . . . . . . . 13
โข
((2nd โ๐ต) ยทN
(2nd โ๐ด))
= ((2nd โ๐ด) ยทN
(2nd โ๐ต)) |
21 | 20 | oveq2i 7373 |
. . . . . . . . . . . 12
โข
((1st โ๐ถ) ยทN
((2nd โ๐ต)
ยทN (2nd โ๐ด))) = ((1st โ๐ถ)
ยทN ((2nd โ๐ด) ยทN
(2nd โ๐ต))) |
22 | 19, 21 | eqtri 2765 |
. . . . . . . . . . 11
โข
(((1st โ๐ถ) ยทN
(2nd โ๐ต))
ยทN (2nd โ๐ด)) = ((1st โ๐ถ)
ยทN ((2nd โ๐ด) ยทN
(2nd โ๐ต))) |
23 | 18, 22 | oveq12i 7374 |
. . . . . . . . . 10
โข
((((1st โ๐ต) ยทN
(2nd โ๐ถ))
ยทN (2nd โ๐ด)) +N
(((1st โ๐ถ)
ยทN (2nd โ๐ต)) ยทN
(2nd โ๐ด)))
= ((((1st โ๐ต) ยทN
(2nd โ๐ด))
ยทN (2nd โ๐ถ)) +N
((1st โ๐ถ)
ยทN ((2nd โ๐ด) ยทN
(2nd โ๐ต)))) |
24 | 15, 23 | eqtri 2765 |
. . . . . . . . 9
โข
((((1st โ๐ต) ยทN
(2nd โ๐ถ))
+N ((1st โ๐ถ) ยทN
(2nd โ๐ต)))
ยทN (2nd โ๐ด)) = ((((1st โ๐ต)
ยทN (2nd โ๐ด)) ยทN
(2nd โ๐ถ))
+N ((1st โ๐ถ) ยทN
((2nd โ๐ด)
ยทN (2nd โ๐ต)))) |
25 | 24 | oveq2i 7373 |
. . . . . . . 8
โข
(((1st โ๐ด) ยทN
((2nd โ๐ต)
ยทN (2nd โ๐ถ))) +N
((((1st โ๐ต) ยทN
(2nd โ๐ถ))
+N ((1st โ๐ถ) ยทN
(2nd โ๐ต)))
ยทN (2nd โ๐ด))) = (((1st โ๐ด)
ยทN ((2nd โ๐ต) ยทN
(2nd โ๐ถ)))
+N ((((1st โ๐ต) ยทN
(2nd โ๐ด))
ยทN (2nd โ๐ถ)) +N
((1st โ๐ถ)
ยทN ((2nd โ๐ด) ยทN
(2nd โ๐ต))))) |
26 | 1, 11, 25 | 3eqtr4i 2775 |
. . . . . . 7
โข
(((((1st โ๐ด) ยทN
(2nd โ๐ต))
+N ((1st โ๐ต) ยทN
(2nd โ๐ด)))
ยทN (2nd โ๐ถ)) +N
((1st โ๐ถ)
ยทN ((2nd โ๐ด) ยทN
(2nd โ๐ต)))) = (((1st โ๐ด)
ยทN ((2nd โ๐ต) ยทN
(2nd โ๐ถ)))
+N ((((1st โ๐ต) ยทN
(2nd โ๐ถ))
+N ((1st โ๐ถ) ยทN
(2nd โ๐ต)))
ยทN (2nd โ๐ด))) |
27 | | mulasspi 10840 |
. . . . . . 7
โข
(((2nd โ๐ด) ยทN
(2nd โ๐ต))
ยทN (2nd โ๐ถ)) = ((2nd โ๐ด)
ยทN ((2nd โ๐ต) ยทN
(2nd โ๐ถ))) |
28 | 26, 27 | opeq12i 4840 |
. . . . . 6
โข
โจ(((((1st โ๐ด) ยทN
(2nd โ๐ต))
+N ((1st โ๐ต) ยทN
(2nd โ๐ด)))
ยทN (2nd โ๐ถ)) +N
((1st โ๐ถ)
ยทN ((2nd โ๐ด) ยทN
(2nd โ๐ต)))), (((2nd โ๐ด)
ยทN (2nd โ๐ต)) ยทN
(2nd โ๐ถ))โฉ = โจ(((1st
โ๐ด)
ยทN ((2nd โ๐ต) ยทN
(2nd โ๐ถ)))
+N ((((1st โ๐ต) ยทN
(2nd โ๐ถ))
+N ((1st โ๐ถ) ยทN
(2nd โ๐ต)))
ยทN (2nd โ๐ด))), ((2nd โ๐ด)
ยทN ((2nd โ๐ต) ยทN
(2nd โ๐ถ)))โฉ |
29 | | elpqn 10868 |
. . . . . . . . . 10
โข (๐ด โ Q โ
๐ด โ (N
ร N)) |
30 | 29 | 3ad2ant1 1134 |
. . . . . . . . 9
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ๐ด
โ (N ร N)) |
31 | | elpqn 10868 |
. . . . . . . . . 10
โข (๐ต โ Q โ
๐ต โ (N
ร N)) |
32 | 31 | 3ad2ant2 1135 |
. . . . . . . . 9
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ๐ต
โ (N ร N)) |
33 | | addpipq2 10879 |
. . . . . . . . 9
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ (๐ด +pQ ๐ต) = โจ(((1st
โ๐ด)
ยทN (2nd โ๐ต)) +N
((1st โ๐ต)
ยทN (2nd โ๐ด))), ((2nd โ๐ด)
ยทN (2nd โ๐ต))โฉ) |
34 | 30, 32, 33 | syl2anc 585 |
. . . . . . . 8
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (๐ด
+pQ ๐ต) = โจ(((1st โ๐ด)
ยทN (2nd โ๐ต)) +N
((1st โ๐ต)
ยทN (2nd โ๐ด))), ((2nd โ๐ด)
ยทN (2nd โ๐ต))โฉ) |
35 | | relxp 5656 |
. . . . . . . . 9
โข Rel
(N ร N) |
36 | | elpqn 10868 |
. . . . . . . . . 10
โข (๐ถ โ Q โ
๐ถ โ (N
ร N)) |
37 | 36 | 3ad2ant3 1136 |
. . . . . . . . 9
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ๐ถ
โ (N ร N)) |
38 | | 1st2nd 7976 |
. . . . . . . . 9
โข ((Rel
(N ร N) โง ๐ถ โ (N ร
N)) โ ๐ถ
= โจ(1st โ๐ถ), (2nd โ๐ถ)โฉ) |
39 | 35, 37, 38 | sylancr 588 |
. . . . . . . 8
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ๐ถ =
โจ(1st โ๐ถ), (2nd โ๐ถ)โฉ) |
40 | 34, 39 | oveq12d 7380 |
. . . . . . 7
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ((๐ด
+pQ ๐ต) +pQ ๐ถ) = (โจ(((1st
โ๐ด)
ยทN (2nd โ๐ต)) +N
((1st โ๐ต)
ยทN (2nd โ๐ด))), ((2nd โ๐ด)
ยทN (2nd โ๐ต))โฉ +pQ
โจ(1st โ๐ถ), (2nd โ๐ถ)โฉ)) |
41 | | xp1st 7958 |
. . . . . . . . . . 11
โข (๐ด โ (N ร
N) โ (1st โ๐ด) โ N) |
42 | 30, 41 | syl 17 |
. . . . . . . . . 10
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (1st โ๐ด) โ N) |
43 | | xp2nd 7959 |
. . . . . . . . . . 11
โข (๐ต โ (N ร
N) โ (2nd โ๐ต) โ N) |
44 | 32, 43 | syl 17 |
. . . . . . . . . 10
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (2nd โ๐ต) โ N) |
45 | | mulclpi 10836 |
. . . . . . . . . 10
โข
(((1st โ๐ด) โ N โง
(2nd โ๐ต)
โ N) โ ((1st โ๐ด) ยทN
(2nd โ๐ต))
โ N) |
46 | 42, 44, 45 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ((1st โ๐ด) ยทN
(2nd โ๐ต))
โ N) |
47 | | xp1st 7958 |
. . . . . . . . . . 11
โข (๐ต โ (N ร
N) โ (1st โ๐ต) โ N) |
48 | 32, 47 | syl 17 |
. . . . . . . . . 10
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (1st โ๐ต) โ N) |
49 | | xp2nd 7959 |
. . . . . . . . . . 11
โข (๐ด โ (N ร
N) โ (2nd โ๐ด) โ N) |
50 | 30, 49 | syl 17 |
. . . . . . . . . 10
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (2nd โ๐ด) โ N) |
51 | | mulclpi 10836 |
. . . . . . . . . 10
โข
(((1st โ๐ต) โ N โง
(2nd โ๐ด)
โ N) โ ((1st โ๐ต) ยทN
(2nd โ๐ด))
โ N) |
52 | 48, 50, 51 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ((1st โ๐ต) ยทN
(2nd โ๐ด))
โ N) |
53 | | addclpi 10835 |
. . . . . . . . 9
โข
((((1st โ๐ด) ยทN
(2nd โ๐ต))
โ N โง ((1st โ๐ต) ยทN
(2nd โ๐ด))
โ N) โ (((1st โ๐ด) ยทN
(2nd โ๐ต))
+N ((1st โ๐ต) ยทN
(2nd โ๐ด)))
โ N) |
54 | 46, 52, 53 | syl2anc 585 |
. . . . . . . 8
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (((1st โ๐ด) ยทN
(2nd โ๐ต))
+N ((1st โ๐ต) ยทN
(2nd โ๐ด)))
โ N) |
55 | | mulclpi 10836 |
. . . . . . . . 9
โข
(((2nd โ๐ด) โ N โง
(2nd โ๐ต)
โ N) โ ((2nd โ๐ด) ยทN
(2nd โ๐ต))
โ N) |
56 | 50, 44, 55 | syl2anc 585 |
. . . . . . . 8
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ((2nd โ๐ด) ยทN
(2nd โ๐ต))
โ N) |
57 | | xp1st 7958 |
. . . . . . . . 9
โข (๐ถ โ (N ร
N) โ (1st โ๐ถ) โ N) |
58 | 37, 57 | syl 17 |
. . . . . . . 8
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (1st โ๐ถ) โ N) |
59 | | xp2nd 7959 |
. . . . . . . . 9
โข (๐ถ โ (N ร
N) โ (2nd โ๐ถ) โ N) |
60 | 37, 59 | syl 17 |
. . . . . . . 8
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (2nd โ๐ถ) โ N) |
61 | | addpipq 10880 |
. . . . . . . 8
โข
((((((1st โ๐ด) ยทN
(2nd โ๐ต))
+N ((1st โ๐ต) ยทN
(2nd โ๐ด)))
โ N โง ((2nd โ๐ด) ยทN
(2nd โ๐ต))
โ N) โง ((1st โ๐ถ) โ N โง
(2nd โ๐ถ)
โ N)) โ (โจ(((1st โ๐ด)
ยทN (2nd โ๐ต)) +N
((1st โ๐ต)
ยทN (2nd โ๐ด))), ((2nd โ๐ด)
ยทN (2nd โ๐ต))โฉ +pQ
โจ(1st โ๐ถ), (2nd โ๐ถ)โฉ) = โจ(((((1st
โ๐ด)
ยทN (2nd โ๐ต)) +N
((1st โ๐ต)
ยทN (2nd โ๐ด))) ยทN
(2nd โ๐ถ))
+N ((1st โ๐ถ) ยทN
((2nd โ๐ด)
ยทN (2nd โ๐ต)))), (((2nd โ๐ด)
ยทN (2nd โ๐ต)) ยทN
(2nd โ๐ถ))โฉ) |
62 | 54, 56, 58, 60, 61 | syl22anc 838 |
. . . . . . 7
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (โจ(((1st โ๐ด) ยทN
(2nd โ๐ต))
+N ((1st โ๐ต) ยทN
(2nd โ๐ด))), ((2nd โ๐ด)
ยทN (2nd โ๐ต))โฉ +pQ
โจ(1st โ๐ถ), (2nd โ๐ถ)โฉ) = โจ(((((1st
โ๐ด)
ยทN (2nd โ๐ต)) +N
((1st โ๐ต)
ยทN (2nd โ๐ด))) ยทN
(2nd โ๐ถ))
+N ((1st โ๐ถ) ยทN
((2nd โ๐ด)
ยทN (2nd โ๐ต)))), (((2nd โ๐ด)
ยทN (2nd โ๐ต)) ยทN
(2nd โ๐ถ))โฉ) |
63 | 40, 62 | eqtrd 2777 |
. . . . . 6
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ((๐ด
+pQ ๐ต) +pQ ๐ถ) = โจ(((((1st
โ๐ด)
ยทN (2nd โ๐ต)) +N
((1st โ๐ต)
ยทN (2nd โ๐ด))) ยทN
(2nd โ๐ถ))
+N ((1st โ๐ถ) ยทN
((2nd โ๐ด)
ยทN (2nd โ๐ต)))), (((2nd โ๐ด)
ยทN (2nd โ๐ต)) ยทN
(2nd โ๐ถ))โฉ) |
64 | | 1st2nd 7976 |
. . . . . . . . 9
โข ((Rel
(N ร N) โง ๐ด โ (N ร
N)) โ ๐ด
= โจ(1st โ๐ด), (2nd โ๐ด)โฉ) |
65 | 35, 30, 64 | sylancr 588 |
. . . . . . . 8
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ๐ด =
โจ(1st โ๐ด), (2nd โ๐ด)โฉ) |
66 | | addpipq2 10879 |
. . . . . . . . 9
โข ((๐ต โ (N ร
N) โง ๐ถ
โ (N ร N)) โ (๐ต +pQ ๐ถ) = โจ(((1st
โ๐ต)
ยทN (2nd โ๐ถ)) +N
((1st โ๐ถ)
ยทN (2nd โ๐ต))), ((2nd โ๐ต)
ยทN (2nd โ๐ถ))โฉ) |
67 | 32, 37, 66 | syl2anc 585 |
. . . . . . . 8
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (๐ต
+pQ ๐ถ) = โจ(((1st โ๐ต)
ยทN (2nd โ๐ถ)) +N
((1st โ๐ถ)
ยทN (2nd โ๐ต))), ((2nd โ๐ต)
ยทN (2nd โ๐ถ))โฉ) |
68 | 65, 67 | oveq12d 7380 |
. . . . . . 7
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (๐ด
+pQ (๐ต +pQ ๐ถ)) = (โจ(1st
โ๐ด), (2nd
โ๐ด)โฉ
+pQ โจ(((1st โ๐ต) ยทN
(2nd โ๐ถ))
+N ((1st โ๐ถ) ยทN
(2nd โ๐ต))), ((2nd โ๐ต)
ยทN (2nd โ๐ถ))โฉ)) |
69 | | mulclpi 10836 |
. . . . . . . . . 10
โข
(((1st โ๐ต) โ N โง
(2nd โ๐ถ)
โ N) โ ((1st โ๐ต) ยทN
(2nd โ๐ถ))
โ N) |
70 | 48, 60, 69 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ((1st โ๐ต) ยทN
(2nd โ๐ถ))
โ N) |
71 | | mulclpi 10836 |
. . . . . . . . . 10
โข
(((1st โ๐ถ) โ N โง
(2nd โ๐ต)
โ N) โ ((1st โ๐ถ) ยทN
(2nd โ๐ต))
โ N) |
72 | 58, 44, 71 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ((1st โ๐ถ) ยทN
(2nd โ๐ต))
โ N) |
73 | | addclpi 10835 |
. . . . . . . . 9
โข
((((1st โ๐ต) ยทN
(2nd โ๐ถ))
โ N โง ((1st โ๐ถ) ยทN
(2nd โ๐ต))
โ N) โ (((1st โ๐ต) ยทN
(2nd โ๐ถ))
+N ((1st โ๐ถ) ยทN
(2nd โ๐ต)))
โ N) |
74 | 70, 72, 73 | syl2anc 585 |
. . . . . . . 8
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (((1st โ๐ต) ยทN
(2nd โ๐ถ))
+N ((1st โ๐ถ) ยทN
(2nd โ๐ต)))
โ N) |
75 | | mulclpi 10836 |
. . . . . . . . 9
โข
(((2nd โ๐ต) โ N โง
(2nd โ๐ถ)
โ N) โ ((2nd โ๐ต) ยทN
(2nd โ๐ถ))
โ N) |
76 | 44, 60, 75 | syl2anc 585 |
. . . . . . . 8
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ((2nd โ๐ต) ยทN
(2nd โ๐ถ))
โ N) |
77 | | addpipq 10880 |
. . . . . . . 8
โข
((((1st โ๐ด) โ N โง
(2nd โ๐ด)
โ N) โง ((((1st โ๐ต) ยทN
(2nd โ๐ถ))
+N ((1st โ๐ถ) ยทN
(2nd โ๐ต)))
โ N โง ((2nd โ๐ต) ยทN
(2nd โ๐ถ))
โ N)) โ (โจ(1st โ๐ด), (2nd โ๐ด)โฉ +pQ
โจ(((1st โ๐ต) ยทN
(2nd โ๐ถ))
+N ((1st โ๐ถ) ยทN
(2nd โ๐ต))), ((2nd โ๐ต)
ยทN (2nd โ๐ถ))โฉ) = โจ(((1st
โ๐ด)
ยทN ((2nd โ๐ต) ยทN
(2nd โ๐ถ)))
+N ((((1st โ๐ต) ยทN
(2nd โ๐ถ))
+N ((1st โ๐ถ) ยทN
(2nd โ๐ต)))
ยทN (2nd โ๐ด))), ((2nd โ๐ด)
ยทN ((2nd โ๐ต) ยทN
(2nd โ๐ถ)))โฉ) |
78 | 42, 50, 74, 76, 77 | syl22anc 838 |
. . . . . . 7
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (โจ(1st โ๐ด), (2nd โ๐ด)โฉ +pQ
โจ(((1st โ๐ต) ยทN
(2nd โ๐ถ))
+N ((1st โ๐ถ) ยทN
(2nd โ๐ต))), ((2nd โ๐ต)
ยทN (2nd โ๐ถ))โฉ) = โจ(((1st
โ๐ด)
ยทN ((2nd โ๐ต) ยทN
(2nd โ๐ถ)))
+N ((((1st โ๐ต) ยทN
(2nd โ๐ถ))
+N ((1st โ๐ถ) ยทN
(2nd โ๐ต)))
ยทN (2nd โ๐ด))), ((2nd โ๐ด)
ยทN ((2nd โ๐ต) ยทN
(2nd โ๐ถ)))โฉ) |
79 | 68, 78 | eqtrd 2777 |
. . . . . 6
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (๐ด
+pQ (๐ต +pQ ๐ถ)) = โจ(((1st
โ๐ด)
ยทN ((2nd โ๐ต) ยทN
(2nd โ๐ถ)))
+N ((((1st โ๐ต) ยทN
(2nd โ๐ถ))
+N ((1st โ๐ถ) ยทN
(2nd โ๐ต)))
ยทN (2nd โ๐ด))), ((2nd โ๐ด)
ยทN ((2nd โ๐ต) ยทN
(2nd โ๐ถ)))โฉ) |
80 | 28, 63, 79 | 3eqtr4a 2803 |
. . . . 5
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ((๐ด
+pQ ๐ต) +pQ ๐ถ) = (๐ด +pQ (๐ต +pQ
๐ถ))) |
81 | 80 | fveq2d 6851 |
. . . 4
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ([Q]โ((๐ด +pQ ๐ต) +pQ
๐ถ)) =
([Q]โ(๐ด
+pQ (๐ต +pQ ๐ถ)))) |
82 | | adderpq 10899 |
. . . 4
โข
(([Q]โ(๐ด +pQ ๐ต)) +Q
([Q]โ๐ถ)) = ([Q]โ((๐ด +pQ
๐ต)
+pQ ๐ถ)) |
83 | | adderpq 10899 |
. . . 4
โข
(([Q]โ๐ด) +Q
([Q]โ(๐ต
+pQ ๐ถ))) = ([Q]โ(๐ด +pQ
(๐ต
+pQ ๐ถ))) |
84 | 81, 82, 83 | 3eqtr4g 2802 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (([Q]โ(๐ด +pQ ๐ต)) +Q
([Q]โ๐ถ)) = (([Q]โ๐ด) +Q
([Q]โ(๐ต
+pQ ๐ถ)))) |
85 | | addpqnq 10881 |
. . . . 5
โข ((๐ด โ Q โง
๐ต โ Q)
โ (๐ด
+Q ๐ต) = ([Q]โ(๐ด +pQ
๐ต))) |
86 | 85 | 3adant3 1133 |
. . . 4
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (๐ด
+Q ๐ต) = ([Q]โ(๐ด +pQ
๐ต))) |
87 | | nqerid 10876 |
. . . . . 6
โข (๐ถ โ Q โ
([Q]โ๐ถ)
= ๐ถ) |
88 | 87 | eqcomd 2743 |
. . . . 5
โข (๐ถ โ Q โ
๐ถ =
([Q]โ๐ถ)) |
89 | 88 | 3ad2ant3 1136 |
. . . 4
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ๐ถ =
([Q]โ๐ถ)) |
90 | 86, 89 | oveq12d 7380 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ((๐ด
+Q ๐ต) +Q ๐ถ) =
(([Q]โ(๐ด +pQ ๐ต)) +Q
([Q]โ๐ถ))) |
91 | | nqerid 10876 |
. . . . . 6
โข (๐ด โ Q โ
([Q]โ๐ด)
= ๐ด) |
92 | 91 | eqcomd 2743 |
. . . . 5
โข (๐ด โ Q โ
๐ด =
([Q]โ๐ด)) |
93 | 92 | 3ad2ant1 1134 |
. . . 4
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ๐ด =
([Q]โ๐ด)) |
94 | | addpqnq 10881 |
. . . . 5
โข ((๐ต โ Q โง
๐ถ โ Q)
โ (๐ต
+Q ๐ถ) = ([Q]โ(๐ต +pQ
๐ถ))) |
95 | 94 | 3adant1 1131 |
. . . 4
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (๐ต
+Q ๐ถ) = ([Q]โ(๐ต +pQ
๐ถ))) |
96 | 93, 95 | oveq12d 7380 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (๐ด
+Q (๐ต +Q ๐ถ)) =
(([Q]โ๐ด) +Q
([Q]โ(๐ต
+pQ ๐ถ)))) |
97 | 84, 90, 96 | 3eqtr4d 2787 |
. 2
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ((๐ด
+Q ๐ต) +Q ๐ถ) = (๐ด +Q (๐ต +Q
๐ถ))) |
98 | | addnqf 10891 |
. . . 4
โข
+Q :(Q ร
Q)โถQ |
99 | 98 | fdmi 6685 |
. . 3
โข dom
+Q = (Q ร
Q) |
100 | | 0nnq 10867 |
. . 3
โข ยฌ
โ
โ Q |
101 | 99, 100 | ndmovass 7547 |
. 2
โข (ยฌ
(๐ด โ Q
โง ๐ต โ
Q โง ๐ถ
โ Q) โ ((๐ด +Q ๐ต) +Q
๐ถ) = (๐ด +Q (๐ต +Q
๐ถ))) |
102 | 97, 101 | pm2.61i 182 |
1
โข ((๐ด +Q
๐ต)
+Q ๐ถ) = (๐ด +Q (๐ต +Q
๐ถ)) |