Step | Hyp | Ref
| Expression |
1 | | gsumvsca.a |
. 2
β’ (π β π΄ β Fin) |
2 | | ssid 3970 |
. . 3
β’ π΄ β π΄ |
3 | | sseq1 3973 |
. . . . . . 7
β’ (π = β
β (π β π΄ β β
β π΄)) |
4 | 3 | anbi2d 630 |
. . . . . 6
β’ (π = β
β ((π β§ π β π΄) β (π β§ β
β π΄))) |
5 | | mpteq1 5202 |
. . . . . . . 8
β’ (π = β
β (π β π β¦ (π Β· π)) = (π β β
β¦ (π Β· π))) |
6 | 5 | oveq2d 7377 |
. . . . . . 7
β’ (π = β
β (π Ξ£g
(π β π β¦ (π Β· π))) = (π Ξ£g (π β β
β¦ (π Β· π)))) |
7 | | mpteq1 5202 |
. . . . . . . . 9
β’ (π = β
β (π β π β¦ π) = (π β β
β¦ π)) |
8 | 7 | oveq2d 7377 |
. . . . . . . 8
β’ (π = β
β (π Ξ£g
(π β π β¦ π)) = (π Ξ£g (π β β
β¦ π))) |
9 | 8 | oveq2d 7377 |
. . . . . . 7
β’ (π = β
β (π Β· (π Ξ£g (π β π β¦ π))) = (π Β· (π Ξ£g (π β β
β¦ π)))) |
10 | 6, 9 | eqeq12d 2749 |
. . . . . 6
β’ (π = β
β ((π Ξ£g
(π β π β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π β¦ π))) β (π Ξ£g (π β β
β¦ (π Β· π))) = (π Β· (π Ξ£g (π β β
β¦ π))))) |
11 | 4, 10 | imbi12d 345 |
. . . . 5
β’ (π = β
β (((π β§ π β π΄) β (π Ξ£g (π β π β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π β¦ π)))) β ((π β§ β
β π΄) β (π Ξ£g (π β β
β¦ (π Β· π))) = (π Β· (π Ξ£g (π β β
β¦ π)))))) |
12 | | sseq1 3973 |
. . . . . . 7
β’ (π = π β (π β π΄ β π β π΄)) |
13 | 12 | anbi2d 630 |
. . . . . 6
β’ (π = π β ((π β§ π β π΄) β (π β§ π β π΄))) |
14 | | mpteq1 5202 |
. . . . . . . 8
β’ (π = π β (π β π β¦ (π Β· π)) = (π β π β¦ (π Β· π))) |
15 | 14 | oveq2d 7377 |
. . . . . . 7
β’ (π = π β (π Ξ£g (π β π β¦ (π Β· π))) = (π Ξ£g (π β π β¦ (π Β· π)))) |
16 | | mpteq1 5202 |
. . . . . . . . 9
β’ (π = π β (π β π β¦ π) = (π β π β¦ π)) |
17 | 16 | oveq2d 7377 |
. . . . . . . 8
β’ (π = π β (π Ξ£g (π β π β¦ π)) = (π Ξ£g (π β π β¦ π))) |
18 | 17 | oveq2d 7377 |
. . . . . . 7
β’ (π = π β (π Β· (π Ξ£g (π β π β¦ π))) = (π Β· (π Ξ£g (π β π β¦ π)))) |
19 | 15, 18 | eqeq12d 2749 |
. . . . . 6
β’ (π = π β ((π Ξ£g (π β π β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π β¦ π))) β (π Ξ£g (π β π β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π β¦ π))))) |
20 | 13, 19 | imbi12d 345 |
. . . . 5
β’ (π = π β (((π β§ π β π΄) β (π Ξ£g (π β π β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π β¦ π)))) β ((π β§ π β π΄) β (π Ξ£g (π β π β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π β¦ π)))))) |
21 | | sseq1 3973 |
. . . . . . 7
β’ (π = (π βͺ {π§}) β (π β π΄ β (π βͺ {π§}) β π΄)) |
22 | 21 | anbi2d 630 |
. . . . . 6
β’ (π = (π βͺ {π§}) β ((π β§ π β π΄) β (π β§ (π βͺ {π§}) β π΄))) |
23 | | mpteq1 5202 |
. . . . . . . 8
β’ (π = (π βͺ {π§}) β (π β π β¦ (π Β· π)) = (π β (π βͺ {π§}) β¦ (π Β· π))) |
24 | 23 | oveq2d 7377 |
. . . . . . 7
β’ (π = (π βͺ {π§}) β (π Ξ£g (π β π β¦ (π Β· π))) = (π Ξ£g (π β (π βͺ {π§}) β¦ (π Β· π)))) |
25 | | mpteq1 5202 |
. . . . . . . . 9
β’ (π = (π βͺ {π§}) β (π β π β¦ π) = (π β (π βͺ {π§}) β¦ π)) |
26 | 25 | oveq2d 7377 |
. . . . . . . 8
β’ (π = (π βͺ {π§}) β (π Ξ£g (π β π β¦ π)) = (π Ξ£g (π β (π βͺ {π§}) β¦ π))) |
27 | 26 | oveq2d 7377 |
. . . . . . 7
β’ (π = (π βͺ {π§}) β (π Β· (π Ξ£g (π β π β¦ π))) = (π Β· (π Ξ£g (π β (π βͺ {π§}) β¦ π)))) |
28 | 24, 27 | eqeq12d 2749 |
. . . . . 6
β’ (π = (π βͺ {π§}) β ((π Ξ£g (π β π β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π β¦ π))) β (π Ξ£g (π β (π βͺ {π§}) β¦ (π Β· π))) = (π Β· (π Ξ£g (π β (π βͺ {π§}) β¦ π))))) |
29 | 22, 28 | imbi12d 345 |
. . . . 5
β’ (π = (π βͺ {π§}) β (((π β§ π β π΄) β (π Ξ£g (π β π β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π β¦ π)))) β ((π β§ (π βͺ {π§}) β π΄) β (π Ξ£g (π β (π βͺ {π§}) β¦ (π Β· π))) = (π Β· (π Ξ£g (π β (π βͺ {π§}) β¦ π)))))) |
30 | | sseq1 3973 |
. . . . . . 7
β’ (π = π΄ β (π β π΄ β π΄ β π΄)) |
31 | 30 | anbi2d 630 |
. . . . . 6
β’ (π = π΄ β ((π β§ π β π΄) β (π β§ π΄ β π΄))) |
32 | | mpteq1 5202 |
. . . . . . . 8
β’ (π = π΄ β (π β π β¦ (π Β· π)) = (π β π΄ β¦ (π Β· π))) |
33 | 32 | oveq2d 7377 |
. . . . . . 7
β’ (π = π΄ β (π Ξ£g (π β π β¦ (π Β· π))) = (π Ξ£g (π β π΄ β¦ (π Β· π)))) |
34 | | mpteq1 5202 |
. . . . . . . . 9
β’ (π = π΄ β (π β π β¦ π) = (π β π΄ β¦ π)) |
35 | 34 | oveq2d 7377 |
. . . . . . . 8
β’ (π = π΄ β (π Ξ£g (π β π β¦ π)) = (π Ξ£g (π β π΄ β¦ π))) |
36 | 35 | oveq2d 7377 |
. . . . . . 7
β’ (π = π΄ β (π Β· (π Ξ£g (π β π β¦ π))) = (π Β· (π Ξ£g (π β π΄ β¦ π)))) |
37 | 33, 36 | eqeq12d 2749 |
. . . . . 6
β’ (π = π΄ β ((π Ξ£g (π β π β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π β¦ π))) β (π Ξ£g (π β π΄ β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π΄ β¦ π))))) |
38 | 31, 37 | imbi12d 345 |
. . . . 5
β’ (π = π΄ β (((π β§ π β π΄) β (π Ξ£g (π β π β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π β¦ π)))) β ((π β§ π΄ β π΄) β (π Ξ£g (π β π΄ β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π΄ β¦ π)))))) |
39 | | gsumvsca.w |
. . . . . . . . 9
β’ (π β π β SLMod) |
40 | | gsumvsca.k |
. . . . . . . . . 10
β’ (π β πΎ β (BaseβπΊ)) |
41 | | gsumvsca1.n |
. . . . . . . . . 10
β’ (π β π β πΎ) |
42 | 40, 41 | sseldd 3949 |
. . . . . . . . 9
β’ (π β π β (BaseβπΊ)) |
43 | | gsumvsca.g |
. . . . . . . . . 10
β’ πΊ = (Scalarβπ) |
44 | | gsumvsca.t |
. . . . . . . . . 10
β’ Β· = (
Β·π βπ) |
45 | | eqid 2733 |
. . . . . . . . . 10
β’
(BaseβπΊ) =
(BaseβπΊ) |
46 | | gsumvsca.z |
. . . . . . . . . 10
β’ 0 =
(0gβπ) |
47 | 43, 44, 45, 46 | slmdvs0 32116 |
. . . . . . . . 9
β’ ((π β SLMod β§ π β (BaseβπΊ)) β (π Β· 0 ) = 0 ) |
48 | 39, 42, 47 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π Β· 0 ) = 0 ) |
49 | 48 | eqcomd 2739 |
. . . . . . 7
β’ (π β 0 = (π Β· 0 )) |
50 | | mpt0 6647 |
. . . . . . . . 9
β’ (π β β
β¦ (π Β· π)) = β
|
51 | 50 | oveq2i 7372 |
. . . . . . . 8
β’ (π Ξ£g
(π β β
β¦
(π Β· π))) = (π Ξ£g
β
) |
52 | 46 | gsum0 18547 |
. . . . . . . 8
β’ (π Ξ£g
β
) = 0 |
53 | 51, 52 | eqtri 2761 |
. . . . . . 7
β’ (π Ξ£g
(π β β
β¦
(π Β· π))) = 0 |
54 | | mpt0 6647 |
. . . . . . . . . 10
β’ (π β β
β¦ π) = β
|
55 | 54 | oveq2i 7372 |
. . . . . . . . 9
β’ (π Ξ£g
(π β β
β¦
π)) = (π Ξ£g
β
) |
56 | 55, 52 | eqtri 2761 |
. . . . . . . 8
β’ (π Ξ£g
(π β β
β¦
π)) = 0 |
57 | 56 | oveq2i 7372 |
. . . . . . 7
β’ (π Β· (π Ξ£g (π β β
β¦ π))) = (π Β· 0 ) |
58 | 49, 53, 57 | 3eqtr4g 2798 |
. . . . . 6
β’ (π β (π Ξ£g (π β β
β¦ (π Β· π))) = (π Β· (π Ξ£g (π β β
β¦ π)))) |
59 | 58 | adantr 482 |
. . . . 5
β’ ((π β§ β
β π΄) β (π Ξ£g (π β β
β¦ (π Β· π))) = (π Β· (π Ξ£g (π β β
β¦ π)))) |
60 | | ssun1 4136 |
. . . . . . . . 9
β’ π β (π βͺ {π§}) |
61 | | sstr2 3955 |
. . . . . . . . 9
β’ (π β (π βͺ {π§}) β ((π βͺ {π§}) β π΄ β π β π΄)) |
62 | 60, 61 | ax-mp 5 |
. . . . . . . 8
β’ ((π βͺ {π§}) β π΄ β π β π΄) |
63 | 62 | anim2i 618 |
. . . . . . 7
β’ ((π β§ (π βͺ {π§}) β π΄) β (π β§ π β π΄)) |
64 | 63 | imim1i 63 |
. . . . . 6
β’ (((π β§ π β π΄) β (π Ξ£g (π β π β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π β¦ π)))) β ((π β§ (π βͺ {π§}) β π΄) β (π Ξ£g (π β π β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π β¦ π))))) |
65 | 39 | ad2antrl 727 |
. . . . . . . . . . 11
β’ (((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β π β SLMod) |
66 | 42 | ad2antrl 727 |
. . . . . . . . . . 11
β’ (((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β π β (BaseβπΊ)) |
67 | | gsumvsca.b |
. . . . . . . . . . . 12
β’ π΅ = (Baseβπ) |
68 | | slmdcmn 32096 |
. . . . . . . . . . . . 13
β’ (π β SLMod β π β CMnd) |
69 | 65, 68 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β π β CMnd) |
70 | | vex 3451 |
. . . . . . . . . . . . 13
β’ π β V |
71 | 70 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β π β V) |
72 | | simplrl 776 |
. . . . . . . . . . . . . 14
β’ ((((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β§ π β π) β π) |
73 | | simprr 772 |
. . . . . . . . . . . . . . . 16
β’ (((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β (π βͺ {π§}) β π΄) |
74 | 73 | unssad 4151 |
. . . . . . . . . . . . . . 15
β’ (((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β π β π΄) |
75 | 74 | sselda 3948 |
. . . . . . . . . . . . . 14
β’ ((((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β§ π β π) β π β π΄) |
76 | | gsumvsca1.c |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β π β π΅) |
77 | 72, 75, 76 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β§ π β π) β π β π΅) |
78 | 77 | fmpttd 7067 |
. . . . . . . . . . . 12
β’ (((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β (π β π β¦ π):πβΆπ΅) |
79 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (π β π β¦ π) = (π β π β¦ π) |
80 | | simpll 766 |
. . . . . . . . . . . . 13
β’ (((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β π β Fin) |
81 | 46 | fvexi 6860 |
. . . . . . . . . . . . . 14
β’ 0 β
V |
82 | 81 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β 0 β V) |
83 | 79, 80, 77, 82 | fsuppmptdm 9324 |
. . . . . . . . . . . 12
β’ (((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β (π β π β¦ π) finSupp 0 ) |
84 | 67, 46, 69, 71, 78, 83 | gsumcl 19700 |
. . . . . . . . . . 11
β’ (((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β (π Ξ£g (π β π β¦ π)) β π΅) |
85 | 73 | unssbd 4152 |
. . . . . . . . . . . . 13
β’ (((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β {π§} β π΄) |
86 | | vex 3451 |
. . . . . . . . . . . . . 14
β’ π§ β V |
87 | 86 | snss 4750 |
. . . . . . . . . . . . 13
β’ (π§ β π΄ β {π§} β π΄) |
88 | 85, 87 | sylibr 233 |
. . . . . . . . . . . 12
β’ (((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β π§ β π΄) |
89 | 76 | ralrimiva 3140 |
. . . . . . . . . . . . 13
β’ (π β βπ β π΄ π β π΅) |
90 | 89 | ad2antrl 727 |
. . . . . . . . . . . 12
β’ (((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β βπ β π΄ π β π΅) |
91 | | rspcsbela 4399 |
. . . . . . . . . . . 12
β’ ((π§ β π΄ β§ βπ β π΄ π β π΅) β β¦π§ / πβ¦π β π΅) |
92 | 88, 90, 91 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β β¦π§ / πβ¦π β π΅) |
93 | | gsumvsca.p |
. . . . . . . . . . . 12
β’ + =
(+gβπ) |
94 | 67, 93, 43, 44, 45 | slmdvsdi 32106 |
. . . . . . . . . . 11
β’ ((π β SLMod β§ (π β (BaseβπΊ) β§ (π Ξ£g (π β π β¦ π)) β π΅ β§ β¦π§ / πβ¦π β π΅)) β (π Β· ((π Ξ£g (π β π β¦ π)) + β¦π§ / πβ¦π)) = ((π Β· (π Ξ£g (π β π β¦ π))) + (π Β·
β¦π§ / πβ¦π))) |
95 | 65, 66, 84, 92, 94 | syl13anc 1373 |
. . . . . . . . . 10
β’ (((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β (π Β· ((π Ξ£g (π β π β¦ π)) + β¦π§ / πβ¦π)) = ((π Β· (π Ξ£g (π β π β¦ π))) + (π Β·
β¦π§ / πβ¦π))) |
96 | 95 | adantr 482 |
. . . . . . . . 9
β’ ((((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β§ (π Ξ£g (π β π β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π β¦ π)))) β (π Β· ((π Ξ£g (π β π β¦ π)) + β¦π§ / πβ¦π)) = ((π Β· (π Ξ£g (π β π β¦ π))) + (π Β·
β¦π§ / πβ¦π))) |
97 | | nfcsb1v 3884 |
. . . . . . . . . . . 12
β’
β²πβ¦π§ / πβ¦π |
98 | 86 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β π§ β V) |
99 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β Β¬ π§ β π) |
100 | | csbeq1a 3873 |
. . . . . . . . . . . 12
β’ (π = π§ β π = β¦π§ / πβ¦π) |
101 | 97, 67, 93, 69, 80, 77, 98, 99, 92, 100 | gsumunsnf 19744 |
. . . . . . . . . . 11
β’ (((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β (π Ξ£g (π β (π βͺ {π§}) β¦ π)) = ((π Ξ£g (π β π β¦ π)) + β¦π§ / πβ¦π)) |
102 | 101 | oveq2d 7377 |
. . . . . . . . . 10
β’ (((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β (π Β· (π Ξ£g (π β (π βͺ {π§}) β¦ π))) = (π Β· ((π Ξ£g (π β π β¦ π)) + β¦π§ / πβ¦π))) |
103 | 102 | adantr 482 |
. . . . . . . . 9
β’ ((((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β§ (π Ξ£g (π β π β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π β¦ π)))) β (π Β· (π Ξ£g (π β (π βͺ {π§}) β¦ π))) = (π Β· ((π Ξ£g (π β π β¦ π)) + β¦π§ / πβ¦π))) |
104 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²ππ |
105 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²π
Β· |
106 | 104, 105,
97 | nfov 7391 |
. . . . . . . . . . . 12
β’
β²π(π Β·
β¦π§ / πβ¦π) |
107 | 72, 39 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β§ π β π) β π β SLMod) |
108 | 72, 42 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β§ π β π) β π β (BaseβπΊ)) |
109 | 67, 43, 44, 45 | slmdvscl 32105 |
. . . . . . . . . . . . 13
β’ ((π β SLMod β§ π β (BaseβπΊ) β§ π β π΅) β (π Β· π) β π΅) |
110 | 107, 108,
77, 109 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β§ π β π) β (π Β· π) β π΅) |
111 | 67, 43, 44, 45 | slmdvscl 32105 |
. . . . . . . . . . . . 13
β’ ((π β SLMod β§ π β (BaseβπΊ) β§ β¦π§ / πβ¦π β π΅) β (π Β·
β¦π§ / πβ¦π) β π΅) |
112 | 65, 66, 92, 111 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β (π Β·
β¦π§ / πβ¦π) β π΅) |
113 | 100 | oveq2d 7377 |
. . . . . . . . . . . 12
β’ (π = π§ β (π Β· π) = (π Β·
β¦π§ / πβ¦π)) |
114 | 106, 67, 93, 69, 80, 110, 98, 99, 112, 113 | gsumunsnf 19744 |
. . . . . . . . . . 11
β’ (((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β (π Ξ£g (π β (π βͺ {π§}) β¦ (π Β· π))) = ((π Ξ£g (π β π β¦ (π Β· π))) + (π Β·
β¦π§ / πβ¦π))) |
115 | 114 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β§ (π Ξ£g (π β π β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π β¦ π)))) β (π Ξ£g (π β (π βͺ {π§}) β¦ (π Β· π))) = ((π Ξ£g (π β π β¦ (π Β· π))) + (π Β·
β¦π§ / πβ¦π))) |
116 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β§ (π Ξ£g (π β π β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π β¦ π)))) β (π Ξ£g (π β π β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π β¦ π)))) |
117 | 116 | oveq1d 7376 |
. . . . . . . . . 10
β’ ((((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β§ (π Ξ£g (π β π β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π β¦ π)))) β ((π Ξ£g (π β π β¦ (π Β· π))) + (π Β·
β¦π§ / πβ¦π)) = ((π Β· (π Ξ£g (π β π β¦ π))) + (π Β·
β¦π§ / πβ¦π))) |
118 | 115, 117 | eqtrd 2773 |
. . . . . . . . 9
β’ ((((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β§ (π Ξ£g (π β π β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π β¦ π)))) β (π Ξ£g (π β (π βͺ {π§}) β¦ (π Β· π))) = ((π Β· (π Ξ£g (π β π β¦ π))) + (π Β·
β¦π§ / πβ¦π))) |
119 | 96, 103, 118 | 3eqtr4rd 2784 |
. . . . . . . 8
β’ ((((π β Fin β§ Β¬ π§ β π) β§ (π β§ (π βͺ {π§}) β π΄)) β§ (π Ξ£g (π β π β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π β¦ π)))) β (π Ξ£g (π β (π βͺ {π§}) β¦ (π Β· π))) = (π Β· (π Ξ£g (π β (π βͺ {π§}) β¦ π)))) |
120 | 119 | exp31 421 |
. . . . . . 7
β’ ((π β Fin β§ Β¬ π§ β π) β ((π β§ (π βͺ {π§}) β π΄) β ((π Ξ£g (π β π β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π β¦ π))) β (π Ξ£g (π β (π βͺ {π§}) β¦ (π Β· π))) = (π Β· (π Ξ£g (π β (π βͺ {π§}) β¦ π)))))) |
121 | 120 | a2d 29 |
. . . . . 6
β’ ((π β Fin β§ Β¬ π§ β π) β (((π β§ (π βͺ {π§}) β π΄) β (π Ξ£g (π β π β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π β¦ π)))) β ((π β§ (π βͺ {π§}) β π΄) β (π Ξ£g (π β (π βͺ {π§}) β¦ (π Β· π))) = (π Β· (π Ξ£g (π β (π βͺ {π§}) β¦ π)))))) |
122 | 64, 121 | syl5 34 |
. . . . 5
β’ ((π β Fin β§ Β¬ π§ β π) β (((π β§ π β π΄) β (π Ξ£g (π β π β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π β¦ π)))) β ((π β§ (π βͺ {π§}) β π΄) β (π Ξ£g (π β (π βͺ {π§}) β¦ (π Β· π))) = (π Β· (π Ξ£g (π β (π βͺ {π§}) β¦ π)))))) |
123 | 11, 20, 29, 38, 59, 122 | findcard2s 9115 |
. . . 4
β’ (π΄ β Fin β ((π β§ π΄ β π΄) β (π Ξ£g (π β π΄ β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π΄ β¦ π))))) |
124 | 123 | imp 408 |
. . 3
β’ ((π΄ β Fin β§ (π β§ π΄ β π΄)) β (π Ξ£g (π β π΄ β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π΄ β¦ π)))) |
125 | 2, 124 | mpanr2 703 |
. 2
β’ ((π΄ β Fin β§ π) β (π Ξ£g (π β π΄ β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π΄ β¦ π)))) |
126 | 1, 125 | mpancom 687 |
1
β’ (π β (π Ξ£g (π β π΄ β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π΄ β¦ π)))) |