Step | Hyp | Ref
| Expression |
1 | | mulcompi 10698 |
. . . . . . . . . . . . 13
β’
((1st βπ΄) Β·N
(1st βπ΅))
= ((1st βπ΅) Β·N
(1st βπ΄)) |
2 | 1 | oveq1i 7317 |
. . . . . . . . . . . 12
β’
(((1st βπ΄) Β·N
(1st βπ΅))
Β·N ((2nd βπ΄) Β·N
(2nd βπΆ)))
= (((1st βπ΅) Β·N
(1st βπ΄))
Β·N ((2nd βπ΄) Β·N
(2nd βπΆ))) |
3 | | fvex 6817 |
. . . . . . . . . . . . 13
β’
(1st βπ΅) β V |
4 | | fvex 6817 |
. . . . . . . . . . . . 13
β’
(1st βπ΄) β V |
5 | | fvex 6817 |
. . . . . . . . . . . . 13
β’
(2nd βπ΄) β V |
6 | | mulcompi 10698 |
. . . . . . . . . . . . 13
β’ (π₯
Β·N π¦) = (π¦ Β·N π₯) |
7 | | mulasspi 10699 |
. . . . . . . . . . . . 13
β’ ((π₯
Β·N π¦) Β·N π§) = (π₯ Β·N (π¦
Β·N π§)) |
8 | | fvex 6817 |
. . . . . . . . . . . . 13
β’
(2nd βπΆ) β V |
9 | 3, 4, 5, 6, 7, 8 | caov411 7536 |
. . . . . . . . . . . 12
β’
(((1st βπ΅) Β·N
(1st βπ΄))
Β·N ((2nd βπ΄) Β·N
(2nd βπΆ)))
= (((2nd βπ΄) Β·N
(1st βπ΄))
Β·N ((1st βπ΅) Β·N
(2nd βπΆ))) |
10 | 2, 9 | eqtri 2764 |
. . . . . . . . . . 11
β’
(((1st βπ΄) Β·N
(1st βπ΅))
Β·N ((2nd βπ΄) Β·N
(2nd βπΆ)))
= (((2nd βπ΄) Β·N
(1st βπ΄))
Β·N ((1st βπ΅) Β·N
(2nd βπΆ))) |
11 | | mulcompi 10698 |
. . . . . . . . . . . . 13
β’
((1st βπ΄) Β·N
(1st βπΆ))
= ((1st βπΆ) Β·N
(1st βπ΄)) |
12 | 11 | oveq1i 7317 |
. . . . . . . . . . . 12
β’
(((1st βπ΄) Β·N
(1st βπΆ))
Β·N ((2nd βπ΄) Β·N
(2nd βπ΅)))
= (((1st βπΆ) Β·N
(1st βπ΄))
Β·N ((2nd βπ΄) Β·N
(2nd βπ΅))) |
13 | | fvex 6817 |
. . . . . . . . . . . . 13
β’
(1st βπΆ) β V |
14 | | fvex 6817 |
. . . . . . . . . . . . 13
β’
(2nd βπ΅) β V |
15 | 13, 4, 5, 6, 7, 14 | caov411 7536 |
. . . . . . . . . . . 12
β’
(((1st βπΆ) Β·N
(1st βπ΄))
Β·N ((2nd βπ΄) Β·N
(2nd βπ΅)))
= (((2nd βπ΄) Β·N
(1st βπ΄))
Β·N ((1st βπΆ) Β·N
(2nd βπ΅))) |
16 | 12, 15 | eqtri 2764 |
. . . . . . . . . . 11
β’
(((1st βπ΄) Β·N
(1st βπΆ))
Β·N ((2nd βπ΄) Β·N
(2nd βπ΅)))
= (((2nd βπ΄) Β·N
(1st βπ΄))
Β·N ((1st βπΆ) Β·N
(2nd βπ΅))) |
17 | 10, 16 | oveq12i 7319 |
. . . . . . . . . 10
β’
((((1st βπ΄) Β·N
(1st βπ΅))
Β·N ((2nd βπ΄) Β·N
(2nd βπΆ)))
+N (((1st βπ΄) Β·N
(1st βπΆ))
Β·N ((2nd βπ΄) Β·N
(2nd βπ΅)))) = ((((2nd βπ΄)
Β·N (1st βπ΄)) Β·N
((1st βπ΅)
Β·N (2nd βπΆ))) +N
(((2nd βπ΄)
Β·N (1st βπ΄)) Β·N
((1st βπΆ)
Β·N (2nd βπ΅)))) |
18 | | distrpi 10700 |
. . . . . . . . . 10
β’
(((2nd βπ΄) Β·N
(1st βπ΄))
Β·N (((1st βπ΅) Β·N
(2nd βπΆ))
+N ((1st βπΆ) Β·N
(2nd βπ΅)))) = ((((2nd βπ΄)
Β·N (1st βπ΄)) Β·N
((1st βπ΅)
Β·N (2nd βπΆ))) +N
(((2nd βπ΄)
Β·N (1st βπ΄)) Β·N
((1st βπΆ)
Β·N (2nd βπ΅)))) |
19 | | mulasspi 10699 |
. . . . . . . . . 10
β’
(((2nd βπ΄) Β·N
(1st βπ΄))
Β·N (((1st βπ΅) Β·N
(2nd βπΆ))
+N ((1st βπΆ) Β·N
(2nd βπ΅)))) = ((2nd βπ΄)
Β·N ((1st βπ΄) Β·N
(((1st βπ΅)
Β·N (2nd βπΆ)) +N
((1st βπΆ)
Β·N (2nd βπ΅))))) |
20 | 17, 18, 19 | 3eqtr2i 2770 |
. . . . . . . . 9
β’
((((1st βπ΄) Β·N
(1st βπ΅))
Β·N ((2nd βπ΄) Β·N
(2nd βπΆ)))
+N (((1st βπ΄) Β·N
(1st βπΆ))
Β·N ((2nd βπ΄) Β·N
(2nd βπ΅)))) = ((2nd βπ΄)
Β·N ((1st βπ΄) Β·N
(((1st βπ΅)
Β·N (2nd βπΆ)) +N
((1st βπΆ)
Β·N (2nd βπ΅))))) |
21 | | mulasspi 10699 |
. . . . . . . . . 10
β’
(((2nd βπ΄) Β·N
(2nd βπ΅))
Β·N ((2nd βπ΄) Β·N
(2nd βπΆ)))
= ((2nd βπ΄) Β·N
((2nd βπ΅)
Β·N ((2nd βπ΄) Β·N
(2nd βπΆ)))) |
22 | 14, 5, 8, 6, 7 | caov12 7532 |
. . . . . . . . . . 11
β’
((2nd βπ΅) Β·N
((2nd βπ΄)
Β·N (2nd βπΆ))) = ((2nd βπ΄)
Β·N ((2nd βπ΅) Β·N
(2nd βπΆ))) |
23 | 22 | oveq2i 7318 |
. . . . . . . . . 10
β’
((2nd βπ΄) Β·N
((2nd βπ΅)
Β·N ((2nd βπ΄) Β·N
(2nd βπΆ)))) = ((2nd βπ΄)
Β·N ((2nd βπ΄) Β·N
((2nd βπ΅)
Β·N (2nd βπΆ)))) |
24 | 21, 23 | eqtri 2764 |
. . . . . . . . 9
β’
(((2nd βπ΄) Β·N
(2nd βπ΅))
Β·N ((2nd βπ΄) Β·N
(2nd βπΆ)))
= ((2nd βπ΄) Β·N
((2nd βπ΄)
Β·N ((2nd βπ΅) Β·N
(2nd βπΆ)))) |
25 | 20, 24 | opeq12i 4814 |
. . . . . . . 8
β’
β¨((((1st βπ΄) Β·N
(1st βπ΅))
Β·N ((2nd βπ΄) Β·N
(2nd βπΆ)))
+N (((1st βπ΄) Β·N
(1st βπΆ))
Β·N ((2nd βπ΄) Β·N
(2nd βπ΅)))), (((2nd βπ΄)
Β·N (2nd βπ΅)) Β·N
((2nd βπ΄)
Β·N (2nd βπΆ)))β© = β¨((2nd
βπ΄)
Β·N ((1st βπ΄) Β·N
(((1st βπ΅)
Β·N (2nd βπΆ)) +N
((1st βπΆ)
Β·N (2nd βπ΅))))), ((2nd βπ΄)
Β·N ((2nd βπ΄) Β·N
((2nd βπ΅)
Β·N (2nd βπΆ))))β© |
26 | | elpqn 10727 |
. . . . . . . . . . 11
β’ (π΄ β Q β
π΄ β (N
Γ N)) |
27 | 26 | 3ad2ant1 1133 |
. . . . . . . . . 10
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β π΄
β (N Γ N)) |
28 | | xp2nd 7896 |
. . . . . . . . . 10
β’ (π΄ β (N Γ
N) β (2nd βπ΄) β N) |
29 | 27, 28 | syl 17 |
. . . . . . . . 9
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (2nd βπ΄) β N) |
30 | | xp1st 7895 |
. . . . . . . . . . 11
β’ (π΄ β (N Γ
N) β (1st βπ΄) β N) |
31 | 27, 30 | syl 17 |
. . . . . . . . . 10
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (1st βπ΄) β N) |
32 | | elpqn 10727 |
. . . . . . . . . . . . . 14
β’ (π΅ β Q β
π΅ β (N
Γ N)) |
33 | 32 | 3ad2ant2 1134 |
. . . . . . . . . . . . 13
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β π΅
β (N Γ N)) |
34 | | xp1st 7895 |
. . . . . . . . . . . . 13
β’ (π΅ β (N Γ
N) β (1st βπ΅) β N) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . 12
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (1st βπ΅) β N) |
36 | | elpqn 10727 |
. . . . . . . . . . . . . 14
β’ (πΆ β Q β
πΆ β (N
Γ N)) |
37 | 36 | 3ad2ant3 1135 |
. . . . . . . . . . . . 13
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β πΆ
β (N Γ N)) |
38 | | xp2nd 7896 |
. . . . . . . . . . . . 13
β’ (πΆ β (N Γ
N) β (2nd βπΆ) β N) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . 12
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (2nd βπΆ) β N) |
40 | | mulclpi 10695 |
. . . . . . . . . . . 12
β’
(((1st βπ΅) β N β§
(2nd βπΆ)
β N) β ((1st βπ΅) Β·N
(2nd βπΆ))
β N) |
41 | 35, 39, 40 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β ((1st βπ΅) Β·N
(2nd βπΆ))
β N) |
42 | | xp1st 7895 |
. . . . . . . . . . . . 13
β’ (πΆ β (N Γ
N) β (1st βπΆ) β N) |
43 | 37, 42 | syl 17 |
. . . . . . . . . . . 12
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (1st βπΆ) β N) |
44 | | xp2nd 7896 |
. . . . . . . . . . . . 13
β’ (π΅ β (N Γ
N) β (2nd βπ΅) β N) |
45 | 33, 44 | syl 17 |
. . . . . . . . . . . 12
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (2nd βπ΅) β N) |
46 | | mulclpi 10695 |
. . . . . . . . . . . 12
β’
(((1st βπΆ) β N β§
(2nd βπ΅)
β N) β ((1st βπΆ) Β·N
(2nd βπ΅))
β N) |
47 | 43, 45, 46 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β ((1st βπΆ) Β·N
(2nd βπ΅))
β N) |
48 | | addclpi 10694 |
. . . . . . . . . . 11
β’
((((1st βπ΅) Β·N
(2nd βπΆ))
β N β§ ((1st βπΆ) Β·N
(2nd βπ΅))
β N) β (((1st βπ΅) Β·N
(2nd βπΆ))
+N ((1st βπΆ) Β·N
(2nd βπ΅)))
β N) |
49 | 41, 47, 48 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (((1st βπ΅) Β·N
(2nd βπΆ))
+N ((1st βπΆ) Β·N
(2nd βπ΅)))
β N) |
50 | | mulclpi 10695 |
. . . . . . . . . 10
β’
(((1st βπ΄) β N β§
(((1st βπ΅)
Β·N (2nd βπΆ)) +N
((1st βπΆ)
Β·N (2nd βπ΅))) β N) β
((1st βπ΄)
Β·N (((1st βπ΅) Β·N
(2nd βπΆ))
+N ((1st βπΆ) Β·N
(2nd βπ΅)))) β
N) |
51 | 31, 49, 50 | syl2anc 585 |
. . . . . . . . 9
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β ((1st βπ΄) Β·N
(((1st βπ΅)
Β·N (2nd βπΆ)) +N
((1st βπΆ)
Β·N (2nd βπ΅)))) β
N) |
52 | | mulclpi 10695 |
. . . . . . . . . . 11
β’
(((2nd βπ΅) β N β§
(2nd βπΆ)
β N) β ((2nd βπ΅) Β·N
(2nd βπΆ))
β N) |
53 | 45, 39, 52 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β ((2nd βπ΅) Β·N
(2nd βπΆ))
β N) |
54 | | mulclpi 10695 |
. . . . . . . . . 10
β’
(((2nd βπ΄) β N β§
((2nd βπ΅)
Β·N (2nd βπΆ)) β N) β
((2nd βπ΄)
Β·N ((2nd βπ΅) Β·N
(2nd βπΆ)))
β N) |
55 | 29, 53, 54 | syl2anc 585 |
. . . . . . . . 9
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β ((2nd βπ΄) Β·N
((2nd βπ΅)
Β·N (2nd βπΆ))) β N) |
56 | | mulcanenq 10762 |
. . . . . . . . 9
β’
(((2nd βπ΄) β N β§
((1st βπ΄)
Β·N (((1st βπ΅) Β·N
(2nd βπΆ))
+N ((1st βπΆ) Β·N
(2nd βπ΅)))) β N β§
((2nd βπ΄)
Β·N ((2nd βπ΅) Β·N
(2nd βπΆ)))
β N) β β¨((2nd βπ΄) Β·N
((1st βπ΄)
Β·N (((1st βπ΅) Β·N
(2nd βπΆ))
+N ((1st βπΆ) Β·N
(2nd βπ΅))))), ((2nd βπ΄)
Β·N ((2nd βπ΄) Β·N
((2nd βπ΅)
Β·N (2nd βπΆ))))β© ~Q
β¨((1st βπ΄) Β·N
(((1st βπ΅)
Β·N (2nd βπΆ)) +N
((1st βπΆ)
Β·N (2nd βπ΅)))), ((2nd βπ΄)
Β·N ((2nd βπ΅) Β·N
(2nd βπΆ)))β©) |
57 | 29, 51, 55, 56 | syl3anc 1371 |
. . . . . . . 8
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β β¨((2nd βπ΄) Β·N
((1st βπ΄)
Β·N (((1st βπ΅) Β·N
(2nd βπΆ))
+N ((1st βπΆ) Β·N
(2nd βπ΅))))), ((2nd βπ΄)
Β·N ((2nd βπ΄) Β·N
((2nd βπ΅)
Β·N (2nd βπΆ))))β© ~Q
β¨((1st βπ΄) Β·N
(((1st βπ΅)
Β·N (2nd βπΆ)) +N
((1st βπΆ)
Β·N (2nd βπ΅)))), ((2nd βπ΄)
Β·N ((2nd βπ΅) Β·N
(2nd βπΆ)))β©) |
58 | 25, 57 | eqbrtrid 5116 |
. . . . . . 7
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β β¨((((1st βπ΄) Β·N
(1st βπ΅))
Β·N ((2nd βπ΄) Β·N
(2nd βπΆ)))
+N (((1st βπ΄) Β·N
(1st βπΆ))
Β·N ((2nd βπ΄) Β·N
(2nd βπ΅)))), (((2nd βπ΄)
Β·N (2nd βπ΅)) Β·N
((2nd βπ΄)
Β·N (2nd βπΆ)))β© ~Q
β¨((1st βπ΄) Β·N
(((1st βπ΅)
Β·N (2nd βπΆ)) +N
((1st βπΆ)
Β·N (2nd βπ΅)))), ((2nd βπ΄)
Β·N ((2nd βπ΅) Β·N
(2nd βπΆ)))β©) |
59 | | mulpipq2 10741 |
. . . . . . . . . 10
β’ ((π΄ β (N Γ
N) β§ π΅
β (N Γ N)) β (π΄ Β·pQ π΅) = β¨((1st
βπ΄)
Β·N (1st βπ΅)), ((2nd βπ΄)
Β·N (2nd βπ΅))β©) |
60 | 27, 33, 59 | syl2anc 585 |
. . . . . . . . 9
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (π΄
Β·pQ π΅) = β¨((1st βπ΄)
Β·N (1st βπ΅)), ((2nd βπ΄)
Β·N (2nd βπ΅))β©) |
61 | | mulpipq2 10741 |
. . . . . . . . . 10
β’ ((π΄ β (N Γ
N) β§ πΆ
β (N Γ N)) β (π΄ Β·pQ πΆ) = β¨((1st
βπ΄)
Β·N (1st βπΆ)), ((2nd βπ΄)
Β·N (2nd βπΆ))β©) |
62 | 27, 37, 61 | syl2anc 585 |
. . . . . . . . 9
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (π΄
Β·pQ πΆ) = β¨((1st βπ΄)
Β·N (1st βπΆ)), ((2nd βπ΄)
Β·N (2nd βπΆ))β©) |
63 | 60, 62 | oveq12d 7325 |
. . . . . . . 8
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β ((π΄
Β·pQ π΅) +pQ (π΄
Β·pQ πΆ)) = (β¨((1st βπ΄)
Β·N (1st βπ΅)), ((2nd βπ΄)
Β·N (2nd βπ΅))β© +pQ
β¨((1st βπ΄) Β·N
(1st βπΆ)),
((2nd βπ΄)
Β·N (2nd βπΆ))β©)) |
64 | | mulclpi 10695 |
. . . . . . . . . 10
β’
(((1st βπ΄) β N β§
(1st βπ΅)
β N) β ((1st βπ΄) Β·N
(1st βπ΅))
β N) |
65 | 31, 35, 64 | syl2anc 585 |
. . . . . . . . 9
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β ((1st βπ΄) Β·N
(1st βπ΅))
β N) |
66 | | mulclpi 10695 |
. . . . . . . . . 10
β’
(((2nd βπ΄) β N β§
(2nd βπ΅)
β N) β ((2nd βπ΄) Β·N
(2nd βπ΅))
β N) |
67 | 29, 45, 66 | syl2anc 585 |
. . . . . . . . 9
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β ((2nd βπ΄) Β·N
(2nd βπ΅))
β N) |
68 | | mulclpi 10695 |
. . . . . . . . . 10
β’
(((1st βπ΄) β N β§
(1st βπΆ)
β N) β ((1st βπ΄) Β·N
(1st βπΆ))
β N) |
69 | 31, 43, 68 | syl2anc 585 |
. . . . . . . . 9
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β ((1st βπ΄) Β·N
(1st βπΆ))
β N) |
70 | | mulclpi 10695 |
. . . . . . . . . 10
β’
(((2nd βπ΄) β N β§
(2nd βπΆ)
β N) β ((2nd βπ΄) Β·N
(2nd βπΆ))
β N) |
71 | 29, 39, 70 | syl2anc 585 |
. . . . . . . . 9
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β ((2nd βπ΄) Β·N
(2nd βπΆ))
β N) |
72 | | addpipq 10739 |
. . . . . . . . 9
β’
(((((1st βπ΄) Β·N
(1st βπ΅))
β N β§ ((2nd βπ΄) Β·N
(2nd βπ΅))
β N) β§ (((1st βπ΄) Β·N
(1st βπΆ))
β N β§ ((2nd βπ΄) Β·N
(2nd βπΆ))
β N)) β (β¨((1st βπ΄)
Β·N (1st βπ΅)), ((2nd βπ΄)
Β·N (2nd βπ΅))β© +pQ
β¨((1st βπ΄) Β·N
(1st βπΆ)),
((2nd βπ΄)
Β·N (2nd βπΆ))β©) = β¨((((1st
βπ΄)
Β·N (1st βπ΅)) Β·N
((2nd βπ΄)
Β·N (2nd βπΆ))) +N
(((1st βπ΄)
Β·N (1st βπΆ)) Β·N
((2nd βπ΄)
Β·N (2nd βπ΅)))), (((2nd βπ΄)
Β·N (2nd βπ΅)) Β·N
((2nd βπ΄)
Β·N (2nd βπΆ)))β©) |
73 | 65, 67, 69, 71, 72 | syl22anc 837 |
. . . . . . . 8
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (β¨((1st βπ΄) Β·N
(1st βπ΅)),
((2nd βπ΄)
Β·N (2nd βπ΅))β© +pQ
β¨((1st βπ΄) Β·N
(1st βπΆ)),
((2nd βπ΄)
Β·N (2nd βπΆ))β©) = β¨((((1st
βπ΄)
Β·N (1st βπ΅)) Β·N
((2nd βπ΄)
Β·N (2nd βπΆ))) +N
(((1st βπ΄)
Β·N (1st βπΆ)) Β·N
((2nd βπ΄)
Β·N (2nd βπ΅)))), (((2nd βπ΄)
Β·N (2nd βπ΅)) Β·N
((2nd βπ΄)
Β·N (2nd βπΆ)))β©) |
74 | 63, 73 | eqtrd 2776 |
. . . . . . 7
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β ((π΄
Β·pQ π΅) +pQ (π΄
Β·pQ πΆ)) = β¨((((1st βπ΄)
Β·N (1st βπ΅)) Β·N
((2nd βπ΄)
Β·N (2nd βπΆ))) +N
(((1st βπ΄)
Β·N (1st βπΆ)) Β·N
((2nd βπ΄)
Β·N (2nd βπ΅)))), (((2nd βπ΄)
Β·N (2nd βπ΅)) Β·N
((2nd βπ΄)
Β·N (2nd βπΆ)))β©) |
75 | | relxp 5618 |
. . . . . . . . . 10
β’ Rel
(N Γ N) |
76 | | 1st2nd 7912 |
. . . . . . . . . 10
β’ ((Rel
(N Γ N) β§ π΄ β (N Γ
N)) β π΄
= β¨(1st βπ΄), (2nd βπ΄)β©) |
77 | 75, 27, 76 | sylancr 588 |
. . . . . . . . 9
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β π΄ =
β¨(1st βπ΄), (2nd βπ΄)β©) |
78 | | addpipq2 10738 |
. . . . . . . . . 10
β’ ((π΅ β (N Γ
N) β§ πΆ
β (N Γ N)) β (π΅ +pQ πΆ) = β¨(((1st
βπ΅)
Β·N (2nd βπΆ)) +N
((1st βπΆ)
Β·N (2nd βπ΅))), ((2nd βπ΅)
Β·N (2nd βπΆ))β©) |
79 | 33, 37, 78 | syl2anc 585 |
. . . . . . . . 9
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (π΅
+pQ πΆ) = β¨(((1st βπ΅)
Β·N (2nd βπΆ)) +N
((1st βπΆ)
Β·N (2nd βπ΅))), ((2nd βπ΅)
Β·N (2nd βπΆ))β©) |
80 | 77, 79 | oveq12d 7325 |
. . . . . . . 8
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (π΄
Β·pQ (π΅ +pQ πΆ)) = (β¨(1st
βπ΄), (2nd
βπ΄)β©
Β·pQ β¨(((1st βπ΅)
Β·N (2nd βπΆ)) +N
((1st βπΆ)
Β·N (2nd βπ΅))), ((2nd βπ΅)
Β·N (2nd βπΆ))β©)) |
81 | | mulpipq 10742 |
. . . . . . . . 9
β’
((((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 (((1st βπ΅) Β·N
(2nd βπΆ))
+N ((1st βπΆ) Β·N
(2nd βπ΅)))), ((2nd βπ΄)
Β·N ((2nd βπ΅) Β·N
(2nd βπΆ)))β©) |
82 | 31, 29, 49, 53, 81 | syl22anc 837 |
. . . . . . . 8
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (β¨(1st βπ΄), (2nd βπ΄)β© Β·pQ
β¨(((1st βπ΅) Β·N
(2nd βπΆ))
+N ((1st βπΆ) Β·N
(2nd βπ΅))), ((2nd βπ΅)
Β·N (2nd βπΆ))β©) = β¨((1st
βπ΄)
Β·N (((1st βπ΅) Β·N
(2nd βπΆ))
+N ((1st βπΆ) Β·N
(2nd βπ΅)))), ((2nd βπ΄)
Β·N ((2nd βπ΅) Β·N
(2nd βπΆ)))β©) |
83 | 80, 82 | eqtrd 2776 |
. . . . . . 7
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (π΄
Β·pQ (π΅ +pQ πΆ)) = β¨((1st
βπ΄)
Β·N (((1st βπ΅) Β·N
(2nd βπΆ))
+N ((1st βπΆ) Β·N
(2nd βπ΅)))), ((2nd βπ΄)
Β·N ((2nd βπ΅) Β·N
(2nd βπΆ)))β©) |
84 | 58, 74, 83 | 3brtr4d 5113 |
. . . . . 6
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β ((π΄
Β·pQ π΅) +pQ (π΄
Β·pQ πΆ)) ~Q (π΄
Β·pQ (π΅ +pQ πΆ))) |
85 | | mulpqf 10748 |
. . . . . . . . . 10
β’
Β·pQ :((N Γ N)
Γ (N Γ N))βΆ(N
Γ N) |
86 | 85 | fovcl 7434 |
. . . . . . . . 9
β’ ((π΄ β (N Γ
N) β§ π΅
β (N Γ N)) β (π΄ Β·pQ π΅) β (N
Γ N)) |
87 | 27, 33, 86 | syl2anc 585 |
. . . . . . . 8
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (π΄
Β·pQ π΅) β (N Γ
N)) |
88 | 85 | fovcl 7434 |
. . . . . . . . 9
β’ ((π΄ β (N Γ
N) β§ πΆ
β (N Γ N)) β (π΄ Β·pQ πΆ) β (N
Γ N)) |
89 | 27, 37, 88 | syl2anc 585 |
. . . . . . . 8
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (π΄
Β·pQ πΆ) β (N Γ
N)) |
90 | | addpqf 10746 |
. . . . . . . . 9
β’
+pQ :((N Γ N)
Γ (N Γ N))βΆ(N
Γ N) |
91 | 90 | fovcl 7434 |
. . . . . . . 8
β’ (((π΄
Β·pQ π΅) β (N Γ
N) β§ (π΄
Β·pQ πΆ) β (N Γ
N)) β ((π΄ Β·pQ π΅) +pQ
(π΄
Β·pQ πΆ)) β (N Γ
N)) |
92 | 87, 89, 91 | syl2anc 585 |
. . . . . . 7
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β ((π΄
Β·pQ π΅) +pQ (π΄
Β·pQ πΆ)) β (N Γ
N)) |
93 | 90 | fovcl 7434 |
. . . . . . . . 9
β’ ((π΅ β (N Γ
N) β§ πΆ
β (N Γ N)) β (π΅ +pQ πΆ) β (N
Γ N)) |
94 | 33, 37, 93 | syl2anc 585 |
. . . . . . . 8
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (π΅
+pQ πΆ) β (N Γ
N)) |
95 | 85 | fovcl 7434 |
. . . . . . . 8
β’ ((π΄ β (N Γ
N) β§ (π΅
+pQ πΆ) β (N Γ
N)) β (π΄
Β·pQ (π΅ +pQ πΆ)) β (N
Γ N)) |
96 | 27, 94, 95 | syl2anc 585 |
. . . . . . 7
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (π΄
Β·pQ (π΅ +pQ πΆ)) β (N
Γ N)) |
97 | | nqereq 10737 |
. . . . . . 7
β’ ((((π΄
Β·pQ π΅) +pQ (π΄
Β·pQ πΆ)) β (N Γ
N) β§ (π΄
Β·pQ (π΅ +pQ πΆ)) β (N
Γ N)) β (((π΄ Β·pQ π΅) +pQ
(π΄
Β·pQ πΆ)) ~Q (π΄
Β·pQ (π΅ +pQ πΆ)) β
([Q]β((π΄ Β·pQ π΅) +pQ
(π΄
Β·pQ πΆ))) = ([Q]β(π΄
Β·pQ (π΅ +pQ πΆ))))) |
98 | 92, 96, 97 | syl2anc 585 |
. . . . . 6
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (((π΄ Β·pQ π΅) +pQ
(π΄
Β·pQ πΆ)) ~Q (π΄
Β·pQ (π΅ +pQ πΆ)) β
([Q]β((π΄ Β·pQ π΅) +pQ
(π΄
Β·pQ πΆ))) = ([Q]β(π΄
Β·pQ (π΅ +pQ πΆ))))) |
99 | 84, 98 | mpbid 231 |
. . . . 5
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β ([Q]β((π΄ Β·pQ π΅) +pQ
(π΄
Β·pQ πΆ))) = ([Q]β(π΄
Β·pQ (π΅ +pQ πΆ)))) |
100 | 99 | eqcomd 2742 |
. . . 4
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β ([Q]β(π΄ Β·pQ (π΅ +pQ
πΆ))) =
([Q]β((π΄ Β·pQ π΅) +pQ
(π΄
Β·pQ πΆ)))) |
101 | | mulerpq 10759 |
. . . 4
β’
(([Q]βπ΄) Β·Q
([Q]β(π΅
+pQ πΆ))) = ([Q]β(π΄
Β·pQ (π΅ +pQ πΆ))) |
102 | | adderpq 10758 |
. . . 4
β’
(([Q]β(π΄ Β·pQ π΅)) +Q
([Q]β(π΄
Β·pQ πΆ))) = ([Q]β((π΄
Β·pQ π΅) +pQ (π΄
Β·pQ πΆ))) |
103 | 100, 101,
102 | 3eqtr4g 2801 |
. . 3
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (([Q]βπ΄) Β·Q
([Q]β(π΅
+pQ πΆ))) = (([Q]β(π΄
Β·pQ π΅)) +Q
([Q]β(π΄
Β·pQ πΆ)))) |
104 | | nqerid 10735 |
. . . . . 6
β’ (π΄ β Q β
([Q]βπ΄)
= π΄) |
105 | 104 | eqcomd 2742 |
. . . . 5
β’ (π΄ β Q β
π΄ =
([Q]βπ΄)) |
106 | 105 | 3ad2ant1 1133 |
. . . 4
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β π΄ =
([Q]βπ΄)) |
107 | | addpqnq 10740 |
. . . . 5
β’ ((π΅ β Q β§
πΆ β Q)
β (π΅
+Q πΆ) = ([Q]β(π΅ +pQ
πΆ))) |
108 | 107 | 3adant1 1130 |
. . . 4
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (π΅
+Q πΆ) = ([Q]β(π΅ +pQ
πΆ))) |
109 | 106, 108 | oveq12d 7325 |
. . 3
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (π΄
Β·Q (π΅ +Q πΆ)) =
(([Q]βπ΄) Β·Q
([Q]β(π΅
+pQ πΆ)))) |
110 | | mulpqnq 10743 |
. . . . 5
β’ ((π΄ β Q β§
π΅ β Q)
β (π΄
Β·Q π΅) = ([Q]β(π΄
Β·pQ π΅))) |
111 | 110 | 3adant3 1132 |
. . . 4
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (π΄
Β·Q π΅) = ([Q]β(π΄
Β·pQ π΅))) |
112 | | mulpqnq 10743 |
. . . . 5
β’ ((π΄ β Q β§
πΆ β Q)
β (π΄
Β·Q πΆ) = ([Q]β(π΄
Β·pQ πΆ))) |
113 | 112 | 3adant2 1131 |
. . . 4
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (π΄
Β·Q πΆ) = ([Q]β(π΄
Β·pQ πΆ))) |
114 | 111, 113 | oveq12d 7325 |
. . 3
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β ((π΄
Β·Q π΅) +Q (π΄
Β·Q πΆ)) = (([Q]β(π΄
Β·pQ π΅)) +Q
([Q]β(π΄
Β·pQ πΆ)))) |
115 | 103, 109,
114 | 3eqtr4d 2786 |
. 2
β’ ((π΄ β Q β§
π΅ β Q
β§ πΆ β
Q) β (π΄
Β·Q (π΅ +Q πΆ)) = ((π΄ Β·Q π΅) +Q
(π΄
Β·Q πΆ))) |
116 | | addnqf 10750 |
. . . 4
β’
+Q :(Q Γ
Q)βΆQ |
117 | 116 | fdmi 6642 |
. . 3
β’ dom
+Q = (Q Γ
Q) |
118 | | 0nnq 10726 |
. . 3
β’ Β¬
β
β Q |
119 | | mulnqf 10751 |
. . . 4
β’
Β·Q :(Q Γ
Q)βΆQ |
120 | 119 | fdmi 6642 |
. . 3
β’ dom
Β·Q = (Q Γ
Q) |
121 | 117, 118,
120 | ndmovdistr 7493 |
. 2
β’ (Β¬
(π΄ β Q
β§ π΅ β
Q β§ πΆ
β Q) β (π΄ Β·Q (π΅ +Q
πΆ)) = ((π΄ Β·Q π΅) +Q
(π΄
Β·Q πΆ))) |
122 | 115, 121 | pm2.61i 182 |
1
β’ (π΄
Β·Q (π΅ +Q πΆ)) = ((π΄ Β·Q π΅) +Q
(π΄
Β·Q πΆ)) |