Step | Hyp | Ref
| Expression |
1 | | gsumle.a |
. . 3
β’ (π β π΄ β Fin) |
2 | | ssid 3967 |
. . . 4
β’ π΄ β π΄ |
3 | | sseq1 3970 |
. . . . . . . 8
β’ (π = β
β (π β π΄ β β
β π΄)) |
4 | 3 | anbi2d 630 |
. . . . . . 7
β’ (π = β
β ((π β§ π β π΄) β (π β§ β
β π΄))) |
5 | | reseq2 5933 |
. . . . . . . . 9
β’ (π = β
β (πΉ βΎ π) = (πΉ βΎ β
)) |
6 | 5 | oveq2d 7374 |
. . . . . . . 8
β’ (π = β
β (π Ξ£g
(πΉ βΎ π)) = (π Ξ£g (πΉ βΎ
β
))) |
7 | | reseq2 5933 |
. . . . . . . . 9
β’ (π = β
β (πΊ βΎ π) = (πΊ βΎ β
)) |
8 | 7 | oveq2d 7374 |
. . . . . . . 8
β’ (π = β
β (π Ξ£g
(πΊ βΎ π)) = (π Ξ£g (πΊ βΎ
β
))) |
9 | 6, 8 | breq12d 5119 |
. . . . . . 7
β’ (π = β
β ((π Ξ£g
(πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π)) β (π Ξ£g (πΉ βΎ β
)) β€ (π Ξ£g
(πΊ βΎ
β
)))) |
10 | 4, 9 | imbi12d 345 |
. . . . . 6
β’ (π = β
β (((π β§ π β π΄) β (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β ((π β§ β
β π΄) β (π Ξ£g (πΉ βΎ β
)) β€ (π Ξ£g
(πΊ βΎ
β
))))) |
11 | | sseq1 3970 |
. . . . . . . 8
β’ (π = π β (π β π΄ β π β π΄)) |
12 | 11 | anbi2d 630 |
. . . . . . 7
β’ (π = π β ((π β§ π β π΄) β (π β§ π β π΄))) |
13 | | reseq2 5933 |
. . . . . . . . 9
β’ (π = π β (πΉ βΎ π) = (πΉ βΎ π)) |
14 | 13 | oveq2d 7374 |
. . . . . . . 8
β’ (π = π β (π Ξ£g (πΉ βΎ π)) = (π Ξ£g (πΉ βΎ π))) |
15 | | reseq2 5933 |
. . . . . . . . 9
β’ (π = π β (πΊ βΎ π) = (πΊ βΎ π)) |
16 | 15 | oveq2d 7374 |
. . . . . . . 8
β’ (π = π β (π Ξ£g (πΊ βΎ π)) = (π Ξ£g (πΊ βΎ π))) |
17 | 14, 16 | breq12d 5119 |
. . . . . . 7
β’ (π = π β ((π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π)) β (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π)))) |
18 | 12, 17 | imbi12d 345 |
. . . . . 6
β’ (π = π β (((π β§ π β π΄) β (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β ((π β§ π β π΄) β (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))))) |
19 | | sseq1 3970 |
. . . . . . . 8
β’ (π = (π βͺ {π¦}) β (π β π΄ β (π βͺ {π¦}) β π΄)) |
20 | 19 | anbi2d 630 |
. . . . . . 7
β’ (π = (π βͺ {π¦}) β ((π β§ π β π΄) β (π β§ (π βͺ {π¦}) β π΄))) |
21 | | reseq2 5933 |
. . . . . . . . 9
β’ (π = (π βͺ {π¦}) β (πΉ βΎ π) = (πΉ βΎ (π βͺ {π¦}))) |
22 | 21 | oveq2d 7374 |
. . . . . . . 8
β’ (π = (π βͺ {π¦}) β (π Ξ£g (πΉ βΎ π)) = (π Ξ£g (πΉ βΎ (π βͺ {π¦})))) |
23 | | reseq2 5933 |
. . . . . . . . 9
β’ (π = (π βͺ {π¦}) β (πΊ βΎ π) = (πΊ βΎ (π βͺ {π¦}))) |
24 | 23 | oveq2d 7374 |
. . . . . . . 8
β’ (π = (π βͺ {π¦}) β (π Ξ£g (πΊ βΎ π)) = (π Ξ£g (πΊ βΎ (π βͺ {π¦})))) |
25 | 22, 24 | breq12d 5119 |
. . . . . . 7
β’ (π = (π βͺ {π¦}) β ((π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π)) β (π Ξ£g (πΉ βΎ (π βͺ {π¦}))) β€ (π Ξ£g (πΊ βΎ (π βͺ {π¦}))))) |
26 | 20, 25 | imbi12d 345 |
. . . . . 6
β’ (π = (π βͺ {π¦}) β (((π β§ π β π΄) β (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β ((π β§ (π βͺ {π¦}) β π΄) β (π Ξ£g (πΉ βΎ (π βͺ {π¦}))) β€ (π Ξ£g (πΊ βΎ (π βͺ {π¦})))))) |
27 | | sseq1 3970 |
. . . . . . . 8
β’ (π = π΄ β (π β π΄ β π΄ β π΄)) |
28 | 27 | anbi2d 630 |
. . . . . . 7
β’ (π = π΄ β ((π β§ π β π΄) β (π β§ π΄ β π΄))) |
29 | | reseq2 5933 |
. . . . . . . . 9
β’ (π = π΄ β (πΉ βΎ π) = (πΉ βΎ π΄)) |
30 | 29 | oveq2d 7374 |
. . . . . . . 8
β’ (π = π΄ β (π Ξ£g (πΉ βΎ π)) = (π Ξ£g (πΉ βΎ π΄))) |
31 | | reseq2 5933 |
. . . . . . . . 9
β’ (π = π΄ β (πΊ βΎ π) = (πΊ βΎ π΄)) |
32 | 31 | oveq2d 7374 |
. . . . . . . 8
β’ (π = π΄ β (π Ξ£g (πΊ βΎ π)) = (π Ξ£g (πΊ βΎ π΄))) |
33 | 30, 32 | breq12d 5119 |
. . . . . . 7
β’ (π = π΄ β ((π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π)) β (π Ξ£g (πΉ βΎ π΄)) β€ (π Ξ£g (πΊ βΎ π΄)))) |
34 | 28, 33 | imbi12d 345 |
. . . . . 6
β’ (π = π΄ β (((π β§ π β π΄) β (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β ((π β§ π΄ β π΄) β (π Ξ£g (πΉ βΎ π΄)) β€ (π Ξ£g (πΊ βΎ π΄))))) |
35 | | gsumle.m |
. . . . . . . . . 10
β’ (π β π β oMnd) |
36 | | omndtos 31962 |
. . . . . . . . . 10
β’ (π β oMnd β π β Toset) |
37 | | tospos 18314 |
. . . . . . . . . 10
β’ (π β Toset β π β Poset) |
38 | 35, 36, 37 | 3syl 18 |
. . . . . . . . 9
β’ (π β π β Poset) |
39 | | res0 5942 |
. . . . . . . . . . . 12
β’ (πΉ βΎ β
) =
β
|
40 | 39 | oveq2i 7369 |
. . . . . . . . . . 11
β’ (π Ξ£g
(πΉ βΎ β
)) =
(π
Ξ£g β
) |
41 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(0gβπ) = (0gβπ) |
42 | 41 | gsum0 18544 |
. . . . . . . . . . 11
β’ (π Ξ£g
β
) = (0gβπ) |
43 | 40, 42 | eqtri 2761 |
. . . . . . . . . 10
β’ (π Ξ£g
(πΉ βΎ β
)) =
(0gβπ) |
44 | | omndmnd 31961 |
. . . . . . . . . . 11
β’ (π β oMnd β π β Mnd) |
45 | | gsumle.b |
. . . . . . . . . . . 12
β’ π΅ = (Baseβπ) |
46 | 45, 41 | mndidcl 18576 |
. . . . . . . . . . 11
β’ (π β Mnd β
(0gβπ)
β π΅) |
47 | 35, 44, 46 | 3syl 18 |
. . . . . . . . . 10
β’ (π β (0gβπ) β π΅) |
48 | 43, 47 | eqeltrid 2838 |
. . . . . . . . 9
β’ (π β (π Ξ£g (πΉ βΎ β
)) β π΅) |
49 | | gsumle.l |
. . . . . . . . . 10
β’ β€ =
(leβπ) |
50 | 45, 49 | posref 18212 |
. . . . . . . . 9
β’ ((π β Poset β§ (π Ξ£g
(πΉ βΎ β
)) β
π΅) β (π Ξ£g
(πΉ βΎ β
)) β€ (π Ξ£g
(πΉ βΎ
β
))) |
51 | 38, 48, 50 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π Ξ£g (πΉ βΎ β
)) β€ (π Ξ£g
(πΉ βΎ
β
))) |
52 | | res0 5942 |
. . . . . . . . . 10
β’ (πΊ βΎ β
) =
β
|
53 | 39, 52 | eqtr4i 2764 |
. . . . . . . . 9
β’ (πΉ βΎ β
) = (πΊ βΎ
β
) |
54 | 53 | oveq2i 7369 |
. . . . . . . 8
β’ (π Ξ£g
(πΉ βΎ β
)) =
(π
Ξ£g (πΊ βΎ β
)) |
55 | 51, 54 | breqtrdi 5147 |
. . . . . . 7
β’ (π β (π Ξ£g (πΉ βΎ β
)) β€ (π Ξ£g
(πΊ βΎ
β
))) |
56 | 55 | adantr 482 |
. . . . . 6
β’ ((π β§ β
β π΄) β (π Ξ£g (πΉ βΎ β
)) β€ (π Ξ£g
(πΊ βΎ
β
))) |
57 | | ssun1 4133 |
. . . . . . . . . 10
β’ π β (π βͺ {π¦}) |
58 | | sstr2 3952 |
. . . . . . . . . 10
β’ (π β (π βͺ {π¦}) β ((π βͺ {π¦}) β π΄ β π β π΄)) |
59 | 57, 58 | ax-mp 5 |
. . . . . . . . 9
β’ ((π βͺ {π¦}) β π΄ β π β π΄) |
60 | 59 | anim2i 618 |
. . . . . . . 8
β’ ((π β§ (π βͺ {π¦}) β π΄) β (π β§ π β π΄)) |
61 | 60 | imim1i 63 |
. . . . . . 7
β’ (((π β§ π β π΄) β (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β ((π β§ (π βͺ {π¦}) β π΄) β (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π)))) |
62 | | simplr 768 |
. . . . . . . . . 10
β’ ((((π β Fin β§ Β¬ π¦ β π) β§ (π β§ (π βͺ {π¦}) β π΄)) β§ (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β (π β§ (π βͺ {π¦}) β π΄)) |
63 | | simpllr 775 |
. . . . . . . . . 10
β’ ((((π β Fin β§ Β¬ π¦ β π) β§ (π β§ (π βͺ {π¦}) β π΄)) β§ (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β Β¬ π¦ β π) |
64 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β Fin β§ Β¬ π¦ β π) β§ (π β§ (π βͺ {π¦}) β π΄)) β§ (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) |
65 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(+gβπ) = (+gβπ) |
66 | 35 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’ ((((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β§ (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β π β oMnd) |
67 | | gsumle.g |
. . . . . . . . . . . . . . 15
β’ (π β πΊ:π΄βΆπ΅) |
68 | 67 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β πΊ:π΄βΆπ΅) |
69 | | simplr 768 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β (π βͺ {π¦}) β π΄) |
70 | | ssun2 4134 |
. . . . . . . . . . . . . . . . 17
β’ {π¦} β (π βͺ {π¦}) |
71 | | vex 3448 |
. . . . . . . . . . . . . . . . . 18
β’ π¦ β V |
72 | 71 | snss 4747 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β (π βͺ {π¦}) β {π¦} β (π βͺ {π¦})) |
73 | 70, 72 | mpbir 230 |
. . . . . . . . . . . . . . . 16
β’ π¦ β (π βͺ {π¦}) |
74 | 73 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β π¦ β (π βͺ {π¦})) |
75 | 69, 74 | sseldd 3946 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β π¦ β π΄) |
76 | 68, 75 | ffvelcdmd 7037 |
. . . . . . . . . . . . 13
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β (πΊβπ¦) β π΅) |
77 | 76 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β§ (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β (πΊβπ¦) β π΅) |
78 | | gsumle.n |
. . . . . . . . . . . . . . 15
β’ (π β π β CMnd) |
79 | 78 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β π β CMnd) |
80 | | vex 3448 |
. . . . . . . . . . . . . . 15
β’ π β V |
81 | 80 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β π β V) |
82 | | gsumle.f |
. . . . . . . . . . . . . . . 16
β’ (π β πΉ:π΄βΆπ΅) |
83 | 82 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β πΉ:π΄βΆπ΅) |
84 | 57, 69 | sstrid 3956 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β π β π΄) |
85 | 83, 84 | fssresd 6710 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β (πΉ βΎ π):πβΆπ΅) |
86 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β π΄ β Fin) |
87 | | fvexd 6858 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β (0gβπ) β V) |
88 | 83, 86, 87 | fdmfifsupp 9320 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β πΉ finSupp (0gβπ)) |
89 | 88, 87 | fsuppres 9335 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β (πΉ βΎ π) finSupp (0gβπ)) |
90 | 45, 41, 79, 81, 85, 89 | gsumcl 19697 |
. . . . . . . . . . . . 13
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β (π Ξ£g (πΉ βΎ π)) β π΅) |
91 | 90 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β§ (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β (π Ξ£g (πΉ βΎ π)) β π΅) |
92 | 83, 75 | ffvelcdmd 7037 |
. . . . . . . . . . . . 13
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β (πΉβπ¦) β π΅) |
93 | 92 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β§ (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β (πΉβπ¦) β π΅) |
94 | 68, 84 | fssresd 6710 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β (πΊ βΎ π):πβΆπ΅) |
95 | | ssfi 9120 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β Fin β§ π β π΄) β π β Fin) |
96 | 86, 84, 95 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β π β Fin) |
97 | 94, 96, 87 | fdmfifsupp 9320 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β (πΊ βΎ π) finSupp (0gβπ)) |
98 | 45, 41, 79, 81, 94, 97 | gsumcl 19697 |
. . . . . . . . . . . . 13
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β (π Ξ£g (πΊ βΎ π)) β π΅) |
99 | 98 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β§ (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β (π Ξ£g (πΊ βΎ π)) β π΅) |
100 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β§ (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) |
101 | | simpll 766 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β π) |
102 | | gsumle.c |
. . . . . . . . . . . . . . 15
β’ (π β πΉ βr β€ πΊ) |
103 | 102 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β πΉ βr β€ πΊ) |
104 | 82 | ffnd 6670 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ Fn π΄) |
105 | 67 | ffnd 6670 |
. . . . . . . . . . . . . . 15
β’ (π β πΊ Fn π΄) |
106 | | inidm 4179 |
. . . . . . . . . . . . . . 15
β’ (π΄ β© π΄) = π΄ |
107 | | eqidd 2734 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β π΄) β (πΉβπ¦) = (πΉβπ¦)) |
108 | | eqidd 2734 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β π΄) β (πΊβπ¦) = (πΊβπ¦)) |
109 | 104, 105,
1, 1, 106, 107, 108 | ofrval 7630 |
. . . . . . . . . . . . . 14
β’ ((π β§ πΉ βr β€ πΊ β§ π¦ β π΄) β (πΉβπ¦) β€ (πΊβπ¦)) |
110 | 101, 103,
75, 109 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β (πΉβπ¦) β€ (πΊβπ¦)) |
111 | 110 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β§ (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β (πΉβπ¦) β€ (πΊβπ¦)) |
112 | 79 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β§ (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β π β CMnd) |
113 | 45, 49, 65, 66, 77, 91, 93, 99, 100, 111, 112 | omndadd2d 31965 |
. . . . . . . . . . 11
β’ ((((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β§ (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β ((π Ξ£g (πΉ βΎ π))(+gβπ)(πΉβπ¦)) β€ ((π Ξ£g (πΊ βΎ π))(+gβπ)(πΊβπ¦))) |
114 | 96 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β§ (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β π β Fin) |
115 | 82 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ π§ β π) β πΉ:π΄βΆπ΅) |
116 | | simplr 768 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ π§ β π) β (π βͺ {π¦}) β π΄) |
117 | | elun1 4137 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ β π β π§ β (π βͺ {π¦})) |
118 | 117 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ π§ β π) β π§ β (π βͺ {π¦})) |
119 | 116, 118 | sseldd 3946 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ π§ β π) β π§ β π΄) |
120 | 115, 119 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ π§ β π) β (πΉβπ§) β π΅) |
121 | 120 | ex 414 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π βͺ {π¦}) β π΄) β (π§ β π β (πΉβπ§) β π΅)) |
122 | 121 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β§ (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β (π§ β π β (πΉβπ§) β π΅)) |
123 | 122 | imp 408 |
. . . . . . . . . . . . 13
β’
(((((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β§ (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β§ π§ β π) β (πΉβπ§) β π΅) |
124 | 71 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β§ (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β π¦ β V) |
125 | | simplr 768 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β§ (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β Β¬ π¦ β π) |
126 | | fveq2 6843 |
. . . . . . . . . . . . 13
β’ (π§ = π¦ β (πΉβπ§) = (πΉβπ¦)) |
127 | 45, 65, 112, 114, 123, 124, 125, 93, 126 | gsumunsn 19742 |
. . . . . . . . . . . 12
β’ ((((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β§ (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β (π Ξ£g (π§ β (π βͺ {π¦}) β¦ (πΉβπ§))) = ((π Ξ£g (π§ β π β¦ (πΉβπ§)))(+gβπ)(πΉβπ¦))) |
128 | 83, 69 | feqresmpt 6912 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β (πΉ βΎ (π βͺ {π¦})) = (π§ β (π βͺ {π¦}) β¦ (πΉβπ§))) |
129 | 128 | oveq2d 7374 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β (π Ξ£g (πΉ βΎ (π βͺ {π¦}))) = (π Ξ£g (π§ β (π βͺ {π¦}) β¦ (πΉβπ§)))) |
130 | 83, 84 | feqresmpt 6912 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β (πΉ βΎ π) = (π§ β π β¦ (πΉβπ§))) |
131 | 130 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β (π Ξ£g (πΉ βΎ π)) = (π Ξ£g (π§ β π β¦ (πΉβπ§)))) |
132 | 131 | oveq1d 7373 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β ((π Ξ£g (πΉ βΎ π))(+gβπ)(πΉβπ¦)) = ((π Ξ£g (π§ β π β¦ (πΉβπ§)))(+gβπ)(πΉβπ¦))) |
133 | 129, 132 | eqeq12d 2749 |
. . . . . . . . . . . . 13
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β ((π Ξ£g (πΉ βΎ (π βͺ {π¦}))) = ((π Ξ£g (πΉ βΎ π))(+gβπ)(πΉβπ¦)) β (π Ξ£g (π§ β (π βͺ {π¦}) β¦ (πΉβπ§))) = ((π Ξ£g (π§ β π β¦ (πΉβπ§)))(+gβπ)(πΉβπ¦)))) |
134 | 133 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β§ (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β ((π Ξ£g (πΉ βΎ (π βͺ {π¦}))) = ((π Ξ£g (πΉ βΎ π))(+gβπ)(πΉβπ¦)) β (π Ξ£g (π§ β (π βͺ {π¦}) β¦ (πΉβπ§))) = ((π Ξ£g (π§ β π β¦ (πΉβπ§)))(+gβπ)(πΉβπ¦)))) |
135 | 127, 134 | mpbird 257 |
. . . . . . . . . . 11
β’ ((((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β§ (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β (π Ξ£g (πΉ βΎ (π βͺ {π¦}))) = ((π Ξ£g (πΉ βΎ π))(+gβπ)(πΉβπ¦))) |
136 | 67 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π βͺ {π¦}) β π΄) β πΊ:π΄βΆπ΅) |
137 | 136 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β§ π§ β π) β πΊ:π΄βΆπ΅) |
138 | 119 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β§ π§ β π) β π§ β π΄) |
139 | 137, 138 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β§ π§ β π) β (πΊβπ§) β π΅) |
140 | 71 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β π¦ β V) |
141 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β Β¬ π¦ β π) |
142 | | fveq2 6843 |
. . . . . . . . . . . . . . . 16
β’ (π§ = π¦ β (πΊβπ§) = (πΊβπ¦)) |
143 | 45, 65, 79, 96, 139, 140, 141, 76, 142 | gsumunsn 19742 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β (π Ξ£g (π§ β (π βͺ {π¦}) β¦ (πΊβπ§))) = ((π Ξ£g (π§ β π β¦ (πΊβπ§)))(+gβπ)(πΊβπ¦))) |
144 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π βͺ {π¦}) β π΄) β (π βͺ {π¦}) β π΄) |
145 | 136, 144 | feqresmpt 6912 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π βͺ {π¦}) β π΄) β (πΊ βΎ (π βͺ {π¦})) = (π§ β (π βͺ {π¦}) β¦ (πΊβπ§))) |
146 | 145 | oveq2d 7374 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π βͺ {π¦}) β π΄) β (π Ξ£g (πΊ βΎ (π βͺ {π¦}))) = (π Ξ£g (π§ β (π βͺ {π¦}) β¦ (πΊβπ§)))) |
147 | | resabs1 5968 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π βͺ {π¦}) β ((πΊ βΎ (π βͺ {π¦})) βΎ π) = (πΊ βΎ π)) |
148 | 57, 147 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π βͺ {π¦}) β π΄) β ((πΊ βΎ (π βͺ {π¦})) βΎ π) = (πΊ βΎ π)) |
149 | 59 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π βͺ {π¦}) β π΄) β π β π΄) |
150 | 136, 149 | feqresmpt 6912 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π βͺ {π¦}) β π΄) β (πΊ βΎ π) = (π§ β π β¦ (πΊβπ§))) |
151 | 148, 150 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π βͺ {π¦}) β π΄) β ((πΊ βΎ (π βͺ {π¦})) βΎ π) = (π§ β π β¦ (πΊβπ§))) |
152 | 151 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π βͺ {π¦}) β π΄) β (π Ξ£g ((πΊ βΎ (π βͺ {π¦})) βΎ π)) = (π Ξ£g (π§ β π β¦ (πΊβπ§)))) |
153 | | resabs1 5968 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ({π¦} β (π βͺ {π¦}) β ((πΊ βΎ (π βͺ {π¦})) βΎ {π¦}) = (πΊ βΎ {π¦})) |
154 | 70, 153 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π βͺ {π¦}) β π΄) β ((πΊ βΎ (π βͺ {π¦})) βΎ {π¦}) = (πΊ βΎ {π¦})) |
155 | 70, 144 | sstrid 3956 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π βͺ {π¦}) β π΄) β {π¦} β π΄) |
156 | 136, 155 | feqresmpt 6912 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π βͺ {π¦}) β π΄) β (πΊ βΎ {π¦}) = (π§ β {π¦} β¦ (πΊβπ§))) |
157 | 154, 156 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π βͺ {π¦}) β π΄) β ((πΊ βΎ (π βͺ {π¦})) βΎ {π¦}) = (π§ β {π¦} β¦ (πΊβπ§))) |
158 | 157 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π βͺ {π¦}) β π΄) β (π Ξ£g ((πΊ βΎ (π βͺ {π¦})) βΎ {π¦})) = (π Ξ£g (π§ β {π¦} β¦ (πΊβπ§)))) |
159 | 35, 44 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β Mnd) |
160 | 159 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π βͺ {π¦}) β π΄) β π β Mnd) |
161 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π βͺ {π¦}) β π΄) β π¦ β V) |
162 | 73 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π βͺ {π¦}) β π΄) β π¦ β (π βͺ {π¦})) |
163 | 144, 162 | sseldd 3946 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π βͺ {π¦}) β π΄) β π¦ β π΄) |
164 | 136, 163 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π βͺ {π¦}) β π΄) β (πΊβπ¦) β π΅) |
165 | 142 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ π§ = π¦) β (πΊβπ§) = (πΊβπ¦)) |
166 | 45, 160, 161, 164, 165 | gsumsnd 19734 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π βͺ {π¦}) β π΄) β (π Ξ£g (π§ β {π¦} β¦ (πΊβπ§))) = (πΊβπ¦)) |
167 | 158, 166 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π βͺ {π¦}) β π΄) β (π Ξ£g ((πΊ βΎ (π βͺ {π¦})) βΎ {π¦})) = (πΊβπ¦)) |
168 | 152, 167 | oveq12d 7376 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π βͺ {π¦}) β π΄) β ((π Ξ£g ((πΊ βΎ (π βͺ {π¦})) βΎ π))(+gβπ)(π Ξ£g ((πΊ βΎ (π βͺ {π¦})) βΎ {π¦}))) = ((π Ξ£g (π§ β π β¦ (πΊβπ§)))(+gβπ)(πΊβπ¦))) |
169 | 146, 168 | eqeq12d 2749 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π βͺ {π¦}) β π΄) β ((π Ξ£g (πΊ βΎ (π βͺ {π¦}))) = ((π Ξ£g ((πΊ βΎ (π βͺ {π¦})) βΎ π))(+gβπ)(π Ξ£g ((πΊ βΎ (π βͺ {π¦})) βΎ {π¦}))) β (π Ξ£g (π§ β (π βͺ {π¦}) β¦ (πΊβπ§))) = ((π Ξ£g (π§ β π β¦ (πΊβπ§)))(+gβπ)(πΊβπ¦)))) |
170 | 169 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β ((π Ξ£g (πΊ βΎ (π βͺ {π¦}))) = ((π Ξ£g ((πΊ βΎ (π βͺ {π¦})) βΎ π))(+gβπ)(π Ξ£g ((πΊ βΎ (π βͺ {π¦})) βΎ {π¦}))) β (π Ξ£g (π§ β (π βͺ {π¦}) β¦ (πΊβπ§))) = ((π Ξ£g (π§ β π β¦ (πΊβπ§)))(+gβπ)(πΊβπ¦)))) |
171 | 143, 170 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β (π Ξ£g (πΊ βΎ (π βͺ {π¦}))) = ((π Ξ£g ((πΊ βΎ (π βͺ {π¦})) βΎ π))(+gβπ)(π Ξ£g ((πΊ βΎ (π βͺ {π¦})) βΎ {π¦})))) |
172 | 57, 147 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ ((πΊ βΎ (π βͺ {π¦})) βΎ π) = (πΊ βΎ π) |
173 | 172 | oveq2i 7369 |
. . . . . . . . . . . . . . 15
β’ (π Ξ£g
((πΊ βΎ (π βͺ {π¦})) βΎ π)) = (π Ξ£g (πΊ βΎ π)) |
174 | 70, 153 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ ((πΊ βΎ (π βͺ {π¦})) βΎ {π¦}) = (πΊ βΎ {π¦}) |
175 | 174 | oveq2i 7369 |
. . . . . . . . . . . . . . 15
β’ (π Ξ£g
((πΊ βΎ (π βͺ {π¦})) βΎ {π¦})) = (π Ξ£g (πΊ βΎ {π¦})) |
176 | 173, 175 | oveq12i 7370 |
. . . . . . . . . . . . . 14
β’ ((π Ξ£g
((πΊ βΎ (π βͺ {π¦})) βΎ π))(+gβπ)(π Ξ£g ((πΊ βΎ (π βͺ {π¦})) βΎ {π¦}))) = ((π Ξ£g (πΊ βΎ π))(+gβπ)(π Ξ£g (πΊ βΎ {π¦}))) |
177 | 171, 176 | eqtrdi 2789 |
. . . . . . . . . . . . 13
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β (π Ξ£g (πΊ βΎ (π βͺ {π¦}))) = ((π Ξ£g (πΊ βΎ π))(+gβπ)(π Ξ£g (πΊ βΎ {π¦})))) |
178 | 70, 69 | sstrid 3956 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β {π¦} β π΄) |
179 | 68, 178 | feqresmpt 6912 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β (πΊ βΎ {π¦}) = (π₯ β {π¦} β¦ (πΊβπ₯))) |
180 | 179 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β (π Ξ£g (πΊ βΎ {π¦})) = (π Ξ£g (π₯ β {π¦} β¦ (πΊβπ₯)))) |
181 | | cmnmnd 19584 |
. . . . . . . . . . . . . . . . 17
β’ (π β CMnd β π β Mnd) |
182 | 79, 181 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β π β Mnd) |
183 | | fveq2 6843 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π¦ β (πΊβπ₯) = (πΊβπ¦)) |
184 | 45, 183 | gsumsn 19736 |
. . . . . . . . . . . . . . . 16
β’ ((π β Mnd β§ π¦ β V β§ (πΊβπ¦) β π΅) β (π Ξ£g (π₯ β {π¦} β¦ (πΊβπ₯))) = (πΊβπ¦)) |
185 | 182, 140,
76, 184 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β (π Ξ£g (π₯ β {π¦} β¦ (πΊβπ₯))) = (πΊβπ¦)) |
186 | 180, 185 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β (π Ξ£g (πΊ βΎ {π¦})) = (πΊβπ¦)) |
187 | 186 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β ((π Ξ£g (πΊ βΎ π))(+gβπ)(π Ξ£g (πΊ βΎ {π¦}))) = ((π Ξ£g (πΊ βΎ π))(+gβπ)(πΊβπ¦))) |
188 | 177, 187 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β (π Ξ£g (πΊ βΎ (π βͺ {π¦}))) = ((π Ξ£g (πΊ βΎ π))(+gβπ)(πΊβπ¦))) |
189 | 188 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β§ (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β (π Ξ£g (πΊ βΎ (π βͺ {π¦}))) = ((π Ξ£g (πΊ βΎ π))(+gβπ)(πΊβπ¦))) |
190 | 113, 135,
189 | 3brtr4d 5138 |
. . . . . . . . . 10
β’ ((((π β§ (π βͺ {π¦}) β π΄) β§ Β¬ π¦ β π) β§ (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β (π Ξ£g (πΉ βΎ (π βͺ {π¦}))) β€ (π Ξ£g (πΊ βΎ (π βͺ {π¦})))) |
191 | 62, 63, 64, 190 | syl21anc 837 |
. . . . . . . . 9
β’ ((((π β Fin β§ Β¬ π¦ β π) β§ (π β§ (π βͺ {π¦}) β π΄)) β§ (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β (π Ξ£g (πΉ βΎ (π βͺ {π¦}))) β€ (π Ξ£g (πΊ βΎ (π βͺ {π¦})))) |
192 | 191 | exp31 421 |
. . . . . . . 8
β’ ((π β Fin β§ Β¬ π¦ β π) β ((π β§ (π βͺ {π¦}) β π΄) β ((π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π)) β (π Ξ£g (πΉ βΎ (π βͺ {π¦}))) β€ (π Ξ£g (πΊ βΎ (π βͺ {π¦})))))) |
193 | 192 | a2d 29 |
. . . . . . 7
β’ ((π β Fin β§ Β¬ π¦ β π) β (((π β§ (π βͺ {π¦}) β π΄) β (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β ((π β§ (π βͺ {π¦}) β π΄) β (π Ξ£g (πΉ βΎ (π βͺ {π¦}))) β€ (π Ξ£g (πΊ βΎ (π βͺ {π¦})))))) |
194 | 61, 193 | syl5 34 |
. . . . . 6
β’ ((π β Fin β§ Β¬ π¦ β π) β (((π β§ π β π΄) β (π Ξ£g (πΉ βΎ π)) β€ (π Ξ£g (πΊ βΎ π))) β ((π β§ (π βͺ {π¦}) β π΄) β (π Ξ£g (πΉ βΎ (π βͺ {π¦}))) β€ (π Ξ£g (πΊ βΎ (π βͺ {π¦})))))) |
195 | 10, 18, 26, 34, 56, 194 | findcard2s 9112 |
. . . . 5
β’ (π΄ β Fin β ((π β§ π΄ β π΄) β (π Ξ£g (πΉ βΎ π΄)) β€ (π Ξ£g (πΊ βΎ π΄)))) |
196 | 195 | imp 408 |
. . . 4
β’ ((π΄ β Fin β§ (π β§ π΄ β π΄)) β (π Ξ£g (πΉ βΎ π΄)) β€ (π Ξ£g (πΊ βΎ π΄))) |
197 | 2, 196 | mpanr2 703 |
. . 3
β’ ((π΄ β Fin β§ π) β (π Ξ£g (πΉ βΎ π΄)) β€ (π Ξ£g (πΊ βΎ π΄))) |
198 | 1, 197 | mpancom 687 |
. 2
β’ (π β (π Ξ£g (πΉ βΎ π΄)) β€ (π Ξ£g (πΊ βΎ π΄))) |
199 | | fnresdm 6621 |
. . . 4
β’ (πΉ Fn π΄ β (πΉ βΎ π΄) = πΉ) |
200 | 104, 199 | syl 17 |
. . 3
β’ (π β (πΉ βΎ π΄) = πΉ) |
201 | 200 | oveq2d 7374 |
. 2
β’ (π β (π Ξ£g (πΉ βΎ π΄)) = (π Ξ£g πΉ)) |
202 | | fnresdm 6621 |
. . . 4
β’ (πΊ Fn π΄ β (πΊ βΎ π΄) = πΊ) |
203 | 105, 202 | syl 17 |
. . 3
β’ (π β (πΊ βΎ π΄) = πΊ) |
204 | 203 | oveq2d 7374 |
. 2
β’ (π β (π Ξ£g (πΊ βΎ π΄)) = (π Ξ£g πΊ)) |
205 | 198, 201,
204 | 3brtr3d 5137 |
1
β’ (π β (π Ξ£g πΉ) β€ (π Ξ£g πΊ)) |