Step | Hyp | Ref
| Expression |
1 | | tsmsxp.2 |
. . . . 5
β’ (π β πΊ β TopGrp) |
2 | | tgpgrp 23445 |
. . . . 5
β’ (πΊ β TopGrp β πΊ β Grp) |
3 | 1, 2 | syl 17 |
. . . 4
β’ (π β πΊ β Grp) |
4 | | tsmsxp.g |
. . . 4
β’ (π β πΊ β CMnd) |
5 | | isabl 19571 |
. . . 4
β’ (πΊ β Abel β (πΊ β Grp β§ πΊ β CMnd)) |
6 | 3, 4, 5 | sylanbrc 584 |
. . 3
β’ (π β πΊ β Abel) |
7 | | tsmsxp.b |
. . . 4
β’ π΅ = (BaseβπΊ) |
8 | | tsmsxp.z |
. . . 4
β’ 0 =
(0gβπΊ) |
9 | | tsmsxp.k |
. . . . . 6
β’ (π β πΎ β (π« π΄ β© Fin)) |
10 | 9 | elin2d 4160 |
. . . . 5
β’ (π β πΎ β Fin) |
11 | | tsmsxp.n |
. . . . . 6
β’ (π β π β (π« πΆ β© Fin)) |
12 | 11 | elin2d 4160 |
. . . . 5
β’ (π β π β Fin) |
13 | | xpfi 9264 |
. . . . 5
β’ ((πΎ β Fin β§ π β Fin) β (πΎ Γ π) β Fin) |
14 | 10, 12, 13 | syl2anc 585 |
. . . 4
β’ (π β (πΎ Γ π) β Fin) |
15 | | tsmsxp.f |
. . . . 5
β’ (π β πΉ:(π΄ Γ πΆ)βΆπ΅) |
16 | | elfpw 9301 |
. . . . . . . 8
β’ (πΎ β (π« π΄ β© Fin) β (πΎ β π΄ β§ πΎ β Fin)) |
17 | 16 | simplbi 499 |
. . . . . . 7
β’ (πΎ β (π« π΄ β© Fin) β πΎ β π΄) |
18 | 9, 17 | syl 17 |
. . . . . 6
β’ (π β πΎ β π΄) |
19 | | elfpw 9301 |
. . . . . . . 8
β’ (π β (π« πΆ β© Fin) β (π β πΆ β§ π β Fin)) |
20 | 19 | simplbi 499 |
. . . . . . 7
β’ (π β (π« πΆ β© Fin) β π β πΆ) |
21 | 11, 20 | syl 17 |
. . . . . 6
β’ (π β π β πΆ) |
22 | | xpss12 5649 |
. . . . . 6
β’ ((πΎ β π΄ β§ π β πΆ) β (πΎ Γ π) β (π΄ Γ πΆ)) |
23 | 18, 21, 22 | syl2anc 585 |
. . . . 5
β’ (π β (πΎ Γ π) β (π΄ Γ πΆ)) |
24 | 15, 23 | fssresd 6710 |
. . . 4
β’ (π β (πΉ βΎ (πΎ Γ π)):(πΎ Γ π)βΆπ΅) |
25 | | tsmsxp.3 |
. . . . 5
β’ (π β 0 β πΏ) |
26 | 24, 14, 25 | fdmfifsupp 9320 |
. . . 4
β’ (π β (πΉ βΎ (πΎ Γ π)) finSupp 0 ) |
27 | 7, 8, 4, 14, 24, 26 | gsumcl 19697 |
. . 3
β’ (π β (πΊ Ξ£g (πΉ βΎ (πΎ Γ π))) β π΅) |
28 | | tsmsxp.h |
. . . . 5
β’ (π β π»:π΄βΆπ΅) |
29 | 28, 18 | fssresd 6710 |
. . . 4
β’ (π β (π» βΎ πΎ):πΎβΆπ΅) |
30 | 29, 10, 25 | fdmfifsupp 9320 |
. . . 4
β’ (π β (π» βΎ πΎ) finSupp 0 ) |
31 | 7, 8, 4, 9, 29, 30 | gsumcl 19697 |
. . 3
β’ (π β (πΊ Ξ£g (π» βΎ πΎ)) β π΅) |
32 | | tsmsxp.p |
. . . 4
β’ + =
(+gβπΊ) |
33 | | tsmsxp.m |
. . . 4
β’ β =
(-gβπΊ) |
34 | 7, 32, 33 | ablpncan3 19600 |
. . 3
β’ ((πΊ β Abel β§ ((πΊ Ξ£g
(πΉ βΎ (πΎ Γ π))) β π΅ β§ (πΊ Ξ£g (π» βΎ πΎ)) β π΅)) β ((πΊ Ξ£g (πΉ βΎ (πΎ Γ π))) + ((πΊ Ξ£g (π» βΎ πΎ)) β (πΊ Ξ£g (πΉ βΎ (πΎ Γ π))))) = (πΊ Ξ£g (π» βΎ πΎ))) |
35 | 6, 27, 31, 34 | syl12anc 836 |
. 2
β’ (π β ((πΊ Ξ£g (πΉ βΎ (πΎ Γ π))) + ((πΊ Ξ£g (π» βΎ πΎ)) β (πΊ Ξ£g (πΉ βΎ (πΎ Γ π))))) = (πΊ Ξ£g (π» βΎ πΎ))) |
36 | | tsmsxp.5 |
. . 3
β’ (π β (πΊ Ξ£g (πΉ βΎ (πΎ Γ π))) β π) |
37 | 4 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π¦ β πΎ) β πΊ β CMnd) |
38 | | snfi 8991 |
. . . . . . . . 9
β’ {π¦} β Fin |
39 | 12 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β πΎ) β π β Fin) |
40 | | xpfi 9264 |
. . . . . . . . 9
β’ (({π¦} β Fin β§ π β Fin) β ({π¦} Γ π) β Fin) |
41 | 38, 39, 40 | sylancr 588 |
. . . . . . . 8
β’ ((π β§ π¦ β πΎ) β ({π¦} Γ π) β Fin) |
42 | 15 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β πΎ) β πΉ:(π΄ Γ πΆ)βΆπ΅) |
43 | 18 | sselda 3945 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β πΎ) β π¦ β π΄) |
44 | 43 | snssd 4770 |
. . . . . . . . . 10
β’ ((π β§ π¦ β πΎ) β {π¦} β π΄) |
45 | 21 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π¦ β πΎ) β π β πΆ) |
46 | | xpss12 5649 |
. . . . . . . . . 10
β’ (({π¦} β π΄ β§ π β πΆ) β ({π¦} Γ π) β (π΄ Γ πΆ)) |
47 | 44, 45, 46 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π¦ β πΎ) β ({π¦} Γ π) β (π΄ Γ πΆ)) |
48 | 42, 47 | fssresd 6710 |
. . . . . . . 8
β’ ((π β§ π¦ β πΎ) β (πΉ βΎ ({π¦} Γ π)):({π¦} Γ π)βΆπ΅) |
49 | 8 | fvexi 6857 |
. . . . . . . . . 10
β’ 0 β
V |
50 | 49 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π¦ β πΎ) β 0 β V) |
51 | 48, 41, 50 | fdmfifsupp 9320 |
. . . . . . . 8
β’ ((π β§ π¦ β πΎ) β (πΉ βΎ ({π¦} Γ π)) finSupp 0 ) |
52 | 7, 8, 37, 41, 48, 51 | gsumcl 19697 |
. . . . . . 7
β’ ((π β§ π¦ β πΎ) β (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π))) β π΅) |
53 | 52 | fmpttd 7064 |
. . . . . 6
β’ (π β (π¦ β πΎ β¦ (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π)))):πΎβΆπ΅) |
54 | | eqid 2733 |
. . . . . . 7
β’ (π¦ β πΎ β¦ (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π)))) = (π¦ β πΎ β¦ (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π)))) |
55 | | ovexd 7393 |
. . . . . . 7
β’ ((π β§ π¦ β πΎ) β (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π))) β V) |
56 | 54, 10, 55, 25 | fsuppmptdm 9321 |
. . . . . 6
β’ (π β (π¦ β πΎ β¦ (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π)))) finSupp 0 ) |
57 | 7, 8, 33, 6, 9, 29, 53, 30, 56 | gsumsub 19730 |
. . . . 5
β’ (π β (πΊ Ξ£g ((π» βΎ πΎ) βf β (π¦ β πΎ β¦ (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π)))))) = ((πΊ Ξ£g (π» βΎ πΎ)) β (πΊ Ξ£g (π¦ β πΎ β¦ (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π))))))) |
58 | | fvexd 6858 |
. . . . . . 7
β’ ((π β§ π¦ β πΎ) β (π»βπ¦) β V) |
59 | 28, 18 | feqresmpt 6912 |
. . . . . . 7
β’ (π β (π» βΎ πΎ) = (π¦ β πΎ β¦ (π»βπ¦))) |
60 | | eqidd 2734 |
. . . . . . 7
β’ (π β (π¦ β πΎ β¦ (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π)))) = (π¦ β πΎ β¦ (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π))))) |
61 | 9, 58, 55, 59, 60 | offval2 7638 |
. . . . . 6
β’ (π β ((π» βΎ πΎ) βf β (π¦ β πΎ β¦ (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π))))) = (π¦ β πΎ β¦ ((π»βπ¦) β (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π)))))) |
62 | 61 | oveq2d 7374 |
. . . . 5
β’ (π β (πΊ Ξ£g ((π» βΎ πΎ) βf β (π¦ β πΎ β¦ (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π)))))) = (πΊ Ξ£g (π¦ β πΎ β¦ ((π»βπ¦) β (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π))))))) |
63 | | cmnmnd 19584 |
. . . . . . . . . . . 12
β’ (πΊ β CMnd β πΊ β Mnd) |
64 | 37, 63 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β πΎ) β πΊ β Mnd) |
65 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β πΎ) β π¦ β πΎ) |
66 | 42 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β πΎ) β§ π§ β π) β πΉ:(π΄ Γ πΆ)βΆπ΅) |
67 | 43 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β πΎ) β§ π§ β π) β π¦ β π΄) |
68 | 45 | sselda 3945 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β πΎ) β§ π§ β π) β π§ β πΆ) |
69 | 66, 67, 68 | fovcdmd 7527 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β πΎ) β§ π§ β π) β (π¦πΉπ§) β π΅) |
70 | 69 | fmpttd 7064 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β πΎ) β (π§ β π β¦ (π¦πΉπ§)):πβΆπ΅) |
71 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (π§ β π β¦ (π¦πΉπ§)) = (π§ β π β¦ (π¦πΉπ§)) |
72 | | ovexd 7393 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β πΎ) β§ π§ β π) β (π¦πΉπ§) β V) |
73 | 71, 39, 72, 50 | fsuppmptdm 9321 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β πΎ) β (π§ β π β¦ (π¦πΉπ§)) finSupp 0 ) |
74 | 7, 8, 37, 39, 70, 73 | gsumcl 19697 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β πΎ) β (πΊ Ξ£g (π§ β π β¦ (π¦πΉπ§))) β π΅) |
75 | | velsn 4603 |
. . . . . . . . . . . . . . . 16
β’ (π€ β {π¦} β π€ = π¦) |
76 | | ovres 7521 |
. . . . . . . . . . . . . . . 16
β’ ((π€ β {π¦} β§ π§ β π) β (π€(πΉ βΎ ({π¦} Γ π))π§) = (π€πΉπ§)) |
77 | 75, 76 | sylanbr 583 |
. . . . . . . . . . . . . . 15
β’ ((π€ = π¦ β§ π§ β π) β (π€(πΉ βΎ ({π¦} Γ π))π§) = (π€πΉπ§)) |
78 | | oveq1 7365 |
. . . . . . . . . . . . . . . 16
β’ (π€ = π¦ β (π€πΉπ§) = (π¦πΉπ§)) |
79 | 78 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π€ = π¦ β§ π§ β π) β (π€πΉπ§) = (π¦πΉπ§)) |
80 | 77, 79 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ ((π€ = π¦ β§ π§ β π) β (π€(πΉ βΎ ({π¦} Γ π))π§) = (π¦πΉπ§)) |
81 | 80 | mpteq2dva 5206 |
. . . . . . . . . . . . 13
β’ (π€ = π¦ β (π§ β π β¦ (π€(πΉ βΎ ({π¦} Γ π))π§)) = (π§ β π β¦ (π¦πΉπ§))) |
82 | 81 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (π€ = π¦ β (πΊ Ξ£g (π§ β π β¦ (π€(πΉ βΎ ({π¦} Γ π))π§))) = (πΊ Ξ£g (π§ β π β¦ (π¦πΉπ§)))) |
83 | 7, 82 | gsumsn 19736 |
. . . . . . . . . . 11
β’ ((πΊ β Mnd β§ π¦ β πΎ β§ (πΊ Ξ£g (π§ β π β¦ (π¦πΉπ§))) β π΅) β (πΊ Ξ£g (π€ β {π¦} β¦ (πΊ Ξ£g (π§ β π β¦ (π€(πΉ βΎ ({π¦} Γ π))π§))))) = (πΊ Ξ£g (π§ β π β¦ (π¦πΉπ§)))) |
84 | 64, 65, 74, 83 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ π¦ β πΎ) β (πΊ Ξ£g (π€ β {π¦} β¦ (πΊ Ξ£g (π§ β π β¦ (π€(πΉ βΎ ({π¦} Γ π))π§))))) = (πΊ Ξ£g (π§ β π β¦ (π¦πΉπ§)))) |
85 | 38 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β πΎ) β {π¦} β Fin) |
86 | 7, 8, 37, 85, 39, 48, 51 | gsumxp 19758 |
. . . . . . . . . 10
β’ ((π β§ π¦ β πΎ) β (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π))) = (πΊ Ξ£g (π€ β {π¦} β¦ (πΊ Ξ£g (π§ β π β¦ (π€(πΉ βΎ ({π¦} Γ π))π§)))))) |
87 | | ovres 7521 |
. . . . . . . . . . . . 13
β’ ((π¦ β πΎ β§ π§ β π) β (π¦(πΉ βΎ (πΎ Γ π))π§) = (π¦πΉπ§)) |
88 | 87 | adantll 713 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β πΎ) β§ π§ β π) β (π¦(πΉ βΎ (πΎ Γ π))π§) = (π¦πΉπ§)) |
89 | 88 | mpteq2dva 5206 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β πΎ) β (π§ β π β¦ (π¦(πΉ βΎ (πΎ Γ π))π§)) = (π§ β π β¦ (π¦πΉπ§))) |
90 | 89 | oveq2d 7374 |
. . . . . . . . . 10
β’ ((π β§ π¦ β πΎ) β (πΊ Ξ£g (π§ β π β¦ (π¦(πΉ βΎ (πΎ Γ π))π§))) = (πΊ Ξ£g (π§ β π β¦ (π¦πΉπ§)))) |
91 | 84, 86, 90 | 3eqtr4d 2783 |
. . . . . . . . 9
β’ ((π β§ π¦ β πΎ) β (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π))) = (πΊ Ξ£g (π§ β π β¦ (π¦(πΉ βΎ (πΎ Γ π))π§)))) |
92 | 91 | mpteq2dva 5206 |
. . . . . . . 8
β’ (π β (π¦ β πΎ β¦ (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π)))) = (π¦ β πΎ β¦ (πΊ Ξ£g (π§ β π β¦ (π¦(πΉ βΎ (πΎ Γ π))π§))))) |
93 | 92 | oveq2d 7374 |
. . . . . . 7
β’ (π β (πΊ Ξ£g (π¦ β πΎ β¦ (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π))))) = (πΊ Ξ£g (π¦ β πΎ β¦ (πΊ Ξ£g (π§ β π β¦ (π¦(πΉ βΎ (πΎ Γ π))π§)))))) |
94 | 7, 8, 4, 10, 12, 24, 26 | gsumxp 19758 |
. . . . . . 7
β’ (π β (πΊ Ξ£g (πΉ βΎ (πΎ Γ π))) = (πΊ Ξ£g (π¦ β πΎ β¦ (πΊ Ξ£g (π§ β π β¦ (π¦(πΉ βΎ (πΎ Γ π))π§)))))) |
95 | 93, 94 | eqtr4d 2776 |
. . . . . 6
β’ (π β (πΊ Ξ£g (π¦ β πΎ β¦ (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π))))) = (πΊ Ξ£g (πΉ βΎ (πΎ Γ π)))) |
96 | 95 | oveq2d 7374 |
. . . . 5
β’ (π β ((πΊ Ξ£g (π» βΎ πΎ)) β (πΊ Ξ£g (π¦ β πΎ β¦ (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π)))))) = ((πΊ Ξ£g (π» βΎ πΎ)) β (πΊ Ξ£g (πΉ βΎ (πΎ Γ π))))) |
97 | 57, 62, 96 | 3eqtr3d 2781 |
. . . 4
β’ (π β (πΊ Ξ£g (π¦ β πΎ β¦ ((π»βπ¦) β (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π)))))) = ((πΊ Ξ£g (π» βΎ πΎ)) β (πΊ Ξ£g (πΉ βΎ (πΎ Γ π))))) |
98 | | oveq2 7366 |
. . . . . 6
β’ (π = (π¦ β πΎ β¦ ((π»βπ¦) β (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π))))) β (πΊ Ξ£g π) = (πΊ Ξ£g (π¦ β πΎ β¦ ((π»βπ¦) β (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π))))))) |
99 | 98 | eleq1d 2819 |
. . . . 5
β’ (π = (π¦ β πΎ β¦ ((π»βπ¦) β (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π))))) β ((πΊ Ξ£g π) β π β (πΊ Ξ£g (π¦ β πΎ β¦ ((π»βπ¦) β (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π)))))) β π)) |
100 | | tsmsxp.6 |
. . . . 5
β’ (π β βπ β (πΏ βm πΎ)(πΊ Ξ£g π) β π) |
101 | | tsmsxp.x |
. . . . . . . 8
β’ (π β βπ₯ β πΎ ((π»βπ₯) β (πΊ Ξ£g (πΉ βΎ ({π₯} Γ π)))) β πΏ) |
102 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β (π»βπ₯) = (π»βπ¦)) |
103 | | sneq 4597 |
. . . . . . . . . . . . . 14
β’ (π₯ = π¦ β {π₯} = {π¦}) |
104 | 103 | xpeq1d 5663 |
. . . . . . . . . . . . 13
β’ (π₯ = π¦ β ({π₯} Γ π) = ({π¦} Γ π)) |
105 | 104 | reseq2d 5938 |
. . . . . . . . . . . 12
β’ (π₯ = π¦ β (πΉ βΎ ({π₯} Γ π)) = (πΉ βΎ ({π¦} Γ π))) |
106 | 105 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β (πΊ Ξ£g (πΉ βΎ ({π₯} Γ π))) = (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π)))) |
107 | 102, 106 | oveq12d 7376 |
. . . . . . . . . 10
β’ (π₯ = π¦ β ((π»βπ₯) β (πΊ Ξ£g (πΉ βΎ ({π₯} Γ π)))) = ((π»βπ¦) β (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π))))) |
108 | 107 | eleq1d 2819 |
. . . . . . . . 9
β’ (π₯ = π¦ β (((π»βπ₯) β (πΊ Ξ£g (πΉ βΎ ({π₯} Γ π)))) β πΏ β ((π»βπ¦) β (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π)))) β πΏ)) |
109 | 108 | rspccva 3579 |
. . . . . . . 8
β’
((βπ₯ β
πΎ ((π»βπ₯) β (πΊ Ξ£g (πΉ βΎ ({π₯} Γ π)))) β πΏ β§ π¦ β πΎ) β ((π»βπ¦) β (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π)))) β πΏ) |
110 | 101, 109 | sylan 581 |
. . . . . . 7
β’ ((π β§ π¦ β πΎ) β ((π»βπ¦) β (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π)))) β πΏ) |
111 | 110 | fmpttd 7064 |
. . . . . 6
β’ (π β (π¦ β πΎ β¦ ((π»βπ¦) β (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π))))):πΎβΆπΏ) |
112 | | tsmsxp.l |
. . . . . . 7
β’ (π β πΏ β π½) |
113 | 112, 9 | elmapd 8782 |
. . . . . 6
β’ (π β ((π¦ β πΎ β¦ ((π»βπ¦) β (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π))))) β (πΏ βm πΎ) β (π¦ β πΎ β¦ ((π»βπ¦) β (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π))))):πΎβΆπΏ)) |
114 | 111, 113 | mpbird 257 |
. . . . 5
β’ (π β (π¦ β πΎ β¦ ((π»βπ¦) β (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π))))) β (πΏ βm πΎ)) |
115 | 99, 100, 114 | rspcdva 3581 |
. . . 4
β’ (π β (πΊ Ξ£g (π¦ β πΎ β¦ ((π»βπ¦) β (πΊ Ξ£g (πΉ βΎ ({π¦} Γ π)))))) β π) |
116 | 97, 115 | eqeltrrd 2835 |
. . 3
β’ (π β ((πΊ Ξ£g (π» βΎ πΎ)) β (πΊ Ξ£g (πΉ βΎ (πΎ Γ π)))) β π) |
117 | | tsmsxp.4 |
. . 3
β’ (π β βπ β π βπ β π (π + π) β π) |
118 | | oveq1 7365 |
. . . . 5
β’ (π = (πΊ Ξ£g (πΉ βΎ (πΎ Γ π))) β (π + π) = ((πΊ Ξ£g (πΉ βΎ (πΎ Γ π))) + π)) |
119 | 118 | eleq1d 2819 |
. . . 4
β’ (π = (πΊ Ξ£g (πΉ βΎ (πΎ Γ π))) β ((π + π) β π β ((πΊ Ξ£g (πΉ βΎ (πΎ Γ π))) + π) β π)) |
120 | | oveq2 7366 |
. . . . 5
β’ (π = ((πΊ Ξ£g (π» βΎ πΎ)) β (πΊ Ξ£g (πΉ βΎ (πΎ Γ π)))) β ((πΊ Ξ£g (πΉ βΎ (πΎ Γ π))) + π) = ((πΊ Ξ£g (πΉ βΎ (πΎ Γ π))) + ((πΊ Ξ£g (π» βΎ πΎ)) β (πΊ Ξ£g (πΉ βΎ (πΎ Γ π)))))) |
121 | 120 | eleq1d 2819 |
. . . 4
β’ (π = ((πΊ Ξ£g (π» βΎ πΎ)) β (πΊ Ξ£g (πΉ βΎ (πΎ Γ π)))) β (((πΊ Ξ£g (πΉ βΎ (πΎ Γ π))) + π) β π β ((πΊ Ξ£g (πΉ βΎ (πΎ Γ π))) + ((πΊ Ξ£g (π» βΎ πΎ)) β (πΊ Ξ£g (πΉ βΎ (πΎ Γ π))))) β π)) |
122 | 119, 121 | rspc2va 3590 |
. . 3
β’ ((((πΊ Ξ£g
(πΉ βΎ (πΎ Γ π))) β π β§ ((πΊ Ξ£g (π» βΎ πΎ)) β (πΊ Ξ£g (πΉ βΎ (πΎ Γ π)))) β π) β§ βπ β π βπ β π (π + π) β π) β ((πΊ Ξ£g (πΉ βΎ (πΎ Γ π))) + ((πΊ Ξ£g (π» βΎ πΎ)) β (πΊ Ξ£g (πΉ βΎ (πΎ Γ π))))) β π) |
123 | 36, 116, 117, 122 | syl21anc 837 |
. 2
β’ (π β ((πΊ Ξ£g (πΉ βΎ (πΎ Γ π))) + ((πΊ Ξ£g (π» βΎ πΎ)) β (πΊ Ξ£g (πΉ βΎ (πΎ Γ π))))) β π) |
124 | 35, 123 | eqeltrrd 2835 |
1
β’ (π β (πΊ Ξ£g (π» βΎ πΎ)) β π) |