Step | Hyp | Ref
| Expression |
1 | | nfcv 2904 |
. . . 4
β’
β²π’Ξ£π β π΄ π΅ |
2 | | nfcv 2904 |
. . . 4
β’
β²π£Ξ£π β π΄ π΅ |
3 | | nfcv 2904 |
. . . . 5
β’
β²π₯π΄ |
4 | | nfcv 2904 |
. . . . . 6
β’
β²π₯π£ |
5 | | nfcsb1v 3884 |
. . . . . 6
β’
β²π₯β¦π’ / π₯β¦π΅ |
6 | 4, 5 | nfcsbw 3886 |
. . . . 5
β’
β²π₯β¦π£ / π¦β¦β¦π’ / π₯β¦π΅ |
7 | 3, 6 | nfsum 15584 |
. . . 4
β’
β²π₯Ξ£π β π΄ β¦π£ / π¦β¦β¦π’ / π₯β¦π΅ |
8 | | nfcv 2904 |
. . . . 5
β’
β²π¦π΄ |
9 | | nfcsb1v 3884 |
. . . . 5
β’
β²π¦β¦π£ / π¦β¦β¦π’ / π₯β¦π΅ |
10 | 8, 9 | nfsum 15584 |
. . . 4
β’
β²π¦Ξ£π β π΄ β¦π£ / π¦β¦β¦π’ / π₯β¦π΅ |
11 | | csbeq1a 3873 |
. . . . . 6
β’ (π₯ = π’ β π΅ = β¦π’ / π₯β¦π΅) |
12 | | csbeq1a 3873 |
. . . . . 6
β’ (π¦ = π£ β β¦π’ / π₯β¦π΅ = β¦π£ / π¦β¦β¦π’ / π₯β¦π΅) |
13 | 11, 12 | sylan9eq 2793 |
. . . . 5
β’ ((π₯ = π’ β§ π¦ = π£) β π΅ = β¦π£ / π¦β¦β¦π’ / π₯β¦π΅) |
14 | 13 | sumeq2sdv 15597 |
. . . 4
β’ ((π₯ = π’ β§ π¦ = π£) β Ξ£π β π΄ π΅ = Ξ£π β π΄ β¦π£ / π¦β¦β¦π’ / π₯β¦π΅) |
15 | 1, 2, 7, 10, 14 | cbvmpo 7455 |
. . 3
β’ (π₯ β π, π¦ β π β¦ Ξ£π β π΄ π΅) = (π’ β π, π£ β π β¦ Ξ£π β π΄ β¦π£ / π¦β¦β¦π’ / π₯β¦π΅) |
16 | | vex 3451 |
. . . . . . . 8
β’ π’ β V |
17 | | vex 3451 |
. . . . . . . 8
β’ π£ β V |
18 | 16, 17 | op2ndd 7936 |
. . . . . . 7
β’ (π§ = β¨π’, π£β© β (2nd βπ§) = π£) |
19 | 18 | csbeq1d 3863 |
. . . . . 6
β’ (π§ = β¨π’, π£β© β β¦(2nd
βπ§) / π¦β¦β¦(1st
βπ§) / π₯β¦π΅ = β¦π£ / π¦β¦β¦(1st
βπ§) / π₯β¦π΅) |
20 | 16, 17 | op1std 7935 |
. . . . . . . 8
β’ (π§ = β¨π’, π£β© β (1st βπ§) = π’) |
21 | 20 | csbeq1d 3863 |
. . . . . . 7
β’ (π§ = β¨π’, π£β© β β¦(1st
βπ§) / π₯β¦π΅ = β¦π’ / π₯β¦π΅) |
22 | 21 | csbeq2dv 3866 |
. . . . . 6
β’ (π§ = β¨π’, π£β© β β¦π£ / π¦β¦β¦(1st
βπ§) / π₯β¦π΅ = β¦π£ / π¦β¦β¦π’ / π₯β¦π΅) |
23 | 19, 22 | eqtrd 2773 |
. . . . 5
β’ (π§ = β¨π’, π£β© β β¦(2nd
βπ§) / π¦β¦β¦(1st
βπ§) / π₯β¦π΅ = β¦π£ / π¦β¦β¦π’ / π₯β¦π΅) |
24 | 23 | sumeq2sdv 15597 |
. . . 4
β’ (π§ = β¨π’, π£β© β Ξ£π β π΄ β¦(2nd βπ§) / π¦β¦β¦(1st
βπ§) / π₯β¦π΅ = Ξ£π β π΄ β¦π£ / π¦β¦β¦π’ / π₯β¦π΅) |
25 | 24 | mpompt 7474 |
. . 3
β’ (π§ β (π Γ π) β¦ Ξ£π β π΄ β¦(2nd βπ§) / π¦β¦β¦(1st
βπ§) / π₯β¦π΅) = (π’ β π, π£ β π β¦ Ξ£π β π΄ β¦π£ / π¦β¦β¦π’ / π₯β¦π΅) |
26 | 15, 25 | eqtr4i 2764 |
. 2
β’ (π₯ β π, π¦ β π β¦ Ξ£π β π΄ π΅) = (π§ β (π Γ π) β¦ Ξ£π β π΄ β¦(2nd βπ§) / π¦β¦β¦(1st
βπ§) / π₯β¦π΅) |
27 | | fsumcn.3 |
. . 3
β’ πΎ =
(TopOpenββfld) |
28 | | fsumcn.4 |
. . . 4
β’ (π β π½ β (TopOnβπ)) |
29 | | fsum2cn.7 |
. . . 4
β’ (π β πΏ β (TopOnβπ)) |
30 | | txtopon 22965 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΏ β (TopOnβπ)) β (π½ Γt πΏ) β (TopOnβ(π Γ π))) |
31 | 28, 29, 30 | syl2anc 585 |
. . 3
β’ (π β (π½ Γt πΏ) β (TopOnβ(π Γ π))) |
32 | | fsumcn.5 |
. . 3
β’ (π β π΄ β Fin) |
33 | | nfcv 2904 |
. . . . . 6
β’
β²π’π΅ |
34 | | nfcv 2904 |
. . . . . 6
β’
β²π£π΅ |
35 | 33, 34, 6, 9, 13 | cbvmpo 7455 |
. . . . 5
β’ (π₯ β π, π¦ β π β¦ π΅) = (π’ β π, π£ β π β¦ β¦π£ / π¦β¦β¦π’ / π₯β¦π΅) |
36 | 23 | mpompt 7474 |
. . . . 5
β’ (π§ β (π Γ π) β¦ β¦(2nd
βπ§) / π¦β¦β¦(1st
βπ§) / π₯β¦π΅) = (π’ β π, π£ β π β¦ β¦π£ / π¦β¦β¦π’ / π₯β¦π΅) |
37 | 35, 36 | eqtr4i 2764 |
. . . 4
β’ (π₯ β π, π¦ β π β¦ π΅) = (π§ β (π Γ π) β¦ β¦(2nd
βπ§) / π¦β¦β¦(1st
βπ§) / π₯β¦π΅) |
38 | | fsum2cn.8 |
. . . 4
β’ ((π β§ π β π΄) β (π₯ β π, π¦ β π β¦ π΅) β ((π½ Γt πΏ) Cn πΎ)) |
39 | 37, 38 | eqeltrrid 2839 |
. . 3
β’ ((π β§ π β π΄) β (π§ β (π Γ π) β¦ β¦(2nd
βπ§) / π¦β¦β¦(1st
βπ§) / π₯β¦π΅) β ((π½ Γt πΏ) Cn πΎ)) |
40 | 27, 31, 32, 39 | fsumcn 24256 |
. 2
β’ (π β (π§ β (π Γ π) β¦ Ξ£π β π΄ β¦(2nd βπ§) / π¦β¦β¦(1st
βπ§) / π₯β¦π΅) β ((π½ Γt πΏ) Cn πΎ)) |
41 | 26, 40 | eqeltrid 2838 |
1
β’ (π β (π₯ β π, π¦ β π β¦ Ξ£π β π΄ π΅) β ((π½ Γt πΏ) Cn πΎ)) |