Step | Hyp | Ref
| Expression |
1 | | prodeq1 15852 |
. . . 4
β’ (π¦ = β
β βπ β π¦ π΅ = βπ β β
π΅) |
2 | 1 | mpteq2dv 5250 |
. . 3
β’ (π¦ = β
β (π₯ β π β¦ βπ β π¦ π΅) = (π₯ β π β¦ βπ β β
π΅)) |
3 | 2 | eleq1d 2818 |
. 2
β’ (π¦ = β
β ((π₯ β π β¦ βπ β π¦ π΅) β (π½ Cn πΎ) β (π₯ β π β¦ βπ β β
π΅) β (π½ Cn πΎ))) |
4 | | prodeq1 15852 |
. . . 4
β’ (π¦ = π§ β βπ β π¦ π΅ = βπ β π§ π΅) |
5 | 4 | mpteq2dv 5250 |
. . 3
β’ (π¦ = π§ β (π₯ β π β¦ βπ β π¦ π΅) = (π₯ β π β¦ βπ β π§ π΅)) |
6 | 5 | eleq1d 2818 |
. 2
β’ (π¦ = π§ β ((π₯ β π β¦ βπ β π¦ π΅) β (π½ Cn πΎ) β (π₯ β π β¦ βπ β π§ π΅) β (π½ Cn πΎ))) |
7 | | prodeq1 15852 |
. . . 4
β’ (π¦ = (π§ βͺ {π€}) β βπ β π¦ π΅ = βπ β (π§ βͺ {π€})π΅) |
8 | 7 | mpteq2dv 5250 |
. . 3
β’ (π¦ = (π§ βͺ {π€}) β (π₯ β π β¦ βπ β π¦ π΅) = (π₯ β π β¦ βπ β (π§ βͺ {π€})π΅)) |
9 | 8 | eleq1d 2818 |
. 2
β’ (π¦ = (π§ βͺ {π€}) β ((π₯ β π β¦ βπ β π¦ π΅) β (π½ Cn πΎ) β (π₯ β π β¦ βπ β (π§ βͺ {π€})π΅) β (π½ Cn πΎ))) |
10 | | prodeq1 15852 |
. . . 4
β’ (π¦ = π΄ β βπ β π¦ π΅ = βπ β π΄ π΅) |
11 | 10 | mpteq2dv 5250 |
. . 3
β’ (π¦ = π΄ β (π₯ β π β¦ βπ β π¦ π΅) = (π₯ β π β¦ βπ β π΄ π΅)) |
12 | 11 | eleq1d 2818 |
. 2
β’ (π¦ = π΄ β ((π₯ β π β¦ βπ β π¦ π΅) β (π½ Cn πΎ) β (π₯ β π β¦ βπ β π΄ π΅) β (π½ Cn πΎ))) |
13 | | prod0 15886 |
. . . . . 6
β’
βπ β
β
π΅ =
1 |
14 | 13 | mpteq2i 5253 |
. . . . 5
β’ (π₯ β π β¦ βπ β β
π΅) = (π₯ β π β¦ 1) |
15 | | eqidd 2733 |
. . . . . 6
β’ (π₯ = π¦ β 1 = 1) |
16 | 15 | cbvmptv 5261 |
. . . . 5
β’ (π₯ β π β¦ 1) = (π¦ β π β¦ 1) |
17 | 14, 16 | eqtri 2760 |
. . . 4
β’ (π₯ β π β¦ βπ β β
π΅) = (π¦ β π β¦ 1) |
18 | 17 | a1i 11 |
. . 3
β’ (π β (π₯ β π β¦ βπ β β
π΅) = (π¦ β π β¦ 1)) |
19 | | fprodcn.j |
. . . 4
β’ (π β π½ β (TopOnβπ)) |
20 | | fprodcn.k |
. . . . . 6
β’ πΎ =
(TopOpenββfld) |
21 | 20 | cnfldtopon 24298 |
. . . . 5
β’ πΎ β
(TopOnββ) |
22 | 21 | a1i 11 |
. . . 4
β’ (π β πΎ β
(TopOnββ)) |
23 | | 1cnd 11208 |
. . . 4
β’ (π β 1 β
β) |
24 | 19, 22, 23 | cnmptc 23165 |
. . 3
β’ (π β (π¦ β π β¦ 1) β (π½ Cn πΎ)) |
25 | 18, 24 | eqeltrd 2833 |
. 2
β’ (π β (π₯ β π β¦ βπ β β
π΅) β (π½ Cn πΎ)) |
26 | | nfcv 2903 |
. . . . . 6
β’
β²π¦βπ β (π§ βͺ {π€})π΅ |
27 | | nfcv 2903 |
. . . . . . 7
β’
β²π₯(π§ βͺ {π€}) |
28 | | nfcsb1v 3918 |
. . . . . . 7
β’
β²π₯β¦π¦ / π₯β¦π΅ |
29 | 27, 28 | nfcprod 15854 |
. . . . . 6
β’
β²π₯βπ β (π§ βͺ {π€})β¦π¦ / π₯β¦π΅ |
30 | | csbeq1a 3907 |
. . . . . . 7
β’ (π₯ = π¦ β π΅ = β¦π¦ / π₯β¦π΅) |
31 | 30 | prodeq2ad 44298 |
. . . . . 6
β’ (π₯ = π¦ β βπ β (π§ βͺ {π€})π΅ = βπ β (π§ βͺ {π€})β¦π¦ / π₯β¦π΅) |
32 | 26, 29, 31 | cbvmpt 5259 |
. . . . 5
β’ (π₯ β π β¦ βπ β (π§ βͺ {π€})π΅) = (π¦ β π β¦ βπ β (π§ βͺ {π€})β¦π¦ / π₯β¦π΅) |
33 | 32 | a1i 11 |
. . . 4
β’ (((π β§ (π§ β π΄ β§ π€ β (π΄ β π§))) β§ (π₯ β π β¦ βπ β π§ π΅) β (π½ Cn πΎ)) β (π₯ β π β¦ βπ β (π§ βͺ {π€})π΅) = (π¦ β π β¦ βπ β (π§ βͺ {π€})β¦π¦ / π₯β¦π΅)) |
34 | | fprodcn.d |
. . . . . . 7
β’
β²ππ |
35 | | nfv 1917 |
. . . . . . 7
β’
β²π(π§ β π΄ β§ π€ β (π΄ β π§)) |
36 | 34, 35 | nfan 1902 |
. . . . . 6
β’
β²π(π β§ (π§ β π΄ β§ π€ β (π΄ β π§))) |
37 | | nfcv 2903 |
. . . . . . . 8
β’
β²ππ |
38 | | nfcv 2903 |
. . . . . . . . 9
β’
β²ππ§ |
39 | 38 | nfcprod1 15853 |
. . . . . . . 8
β’
β²πβπ β π§ π΅ |
40 | 37, 39 | nfmpt 5255 |
. . . . . . 7
β’
β²π(π₯ β π β¦ βπ β π§ π΅) |
41 | | nfcv 2903 |
. . . . . . 7
β’
β²π(π½ Cn πΎ) |
42 | 40, 41 | nfel 2917 |
. . . . . 6
β’
β²π(π₯ β π β¦ βπ β π§ π΅) β (π½ Cn πΎ) |
43 | 36, 42 | nfan 1902 |
. . . . 5
β’
β²π((π β§ (π§ β π΄ β§ π€ β (π΄ β π§))) β§ (π₯ β π β¦ βπ β π§ π΅) β (π½ Cn πΎ)) |
44 | 19 | ad2antrr 724 |
. . . . 5
β’ (((π β§ (π§ β π΄ β§ π€ β (π΄ β π§))) β§ (π₯ β π β¦ βπ β π§ π΅) β (π½ Cn πΎ)) β π½ β (TopOnβπ)) |
45 | | fprodcn.a |
. . . . . 6
β’ (π β π΄ β Fin) |
46 | 45 | ad2antrr 724 |
. . . . 5
β’ (((π β§ (π§ β π΄ β§ π€ β (π΄ β π§))) β§ (π₯ β π β¦ βπ β π§ π΅) β (π½ Cn πΎ)) β π΄ β Fin) |
47 | | nfcv 2903 |
. . . . . . . . . 10
β’
β²π¦π΅ |
48 | 47, 28, 30 | cbvmpt 5259 |
. . . . . . . . 9
β’ (π₯ β π β¦ π΅) = (π¦ β π β¦ β¦π¦ / π₯β¦π΅) |
49 | 48 | eqcomi 2741 |
. . . . . . . 8
β’ (π¦ β π β¦ β¦π¦ / π₯β¦π΅) = (π₯ β π β¦ π΅) |
50 | 49 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β π΄) β (π¦ β π β¦ β¦π¦ / π₯β¦π΅) = (π₯ β π β¦ π΅)) |
51 | | fprodcn.b |
. . . . . . 7
β’ ((π β§ π β π΄) β (π₯ β π β¦ π΅) β (π½ Cn πΎ)) |
52 | 50, 51 | eqeltrd 2833 |
. . . . . 6
β’ ((π β§ π β π΄) β (π¦ β π β¦ β¦π¦ / π₯β¦π΅) β (π½ Cn πΎ)) |
53 | 52 | ad4ant14 750 |
. . . . 5
β’ ((((π β§ (π§ β π΄ β§ π€ β (π΄ β π§))) β§ (π₯ β π β¦ βπ β π§ π΅) β (π½ Cn πΎ)) β§ π β π΄) β (π¦ β π β¦ β¦π¦ / π₯β¦π΅) β (π½ Cn πΎ)) |
54 | | simplrl 775 |
. . . . 5
β’ (((π β§ (π§ β π΄ β§ π€ β (π΄ β π§))) β§ (π₯ β π β¦ βπ β π§ π΅) β (π½ Cn πΎ)) β π§ β π΄) |
55 | | simplrr 776 |
. . . . 5
β’ (((π β§ (π§ β π΄ β§ π€ β (π΄ β π§))) β§ (π₯ β π β¦ βπ β π§ π΅) β (π½ Cn πΎ)) β π€ β (π΄ β π§)) |
56 | | nfcv 2903 |
. . . . . . . . 9
β’
β²π¦βπ β π§ π΅ |
57 | | nfcv 2903 |
. . . . . . . . . 10
β’
β²π₯π§ |
58 | 57, 28 | nfcprod 15854 |
. . . . . . . . 9
β’
β²π₯βπ β π§ β¦π¦ / π₯β¦π΅ |
59 | 30 | prodeq2sdv 15867 |
. . . . . . . . 9
β’ (π₯ = π¦ β βπ β π§ π΅ = βπ β π§ β¦π¦ / π₯β¦π΅) |
60 | 56, 58, 59 | cbvmpt 5259 |
. . . . . . . 8
β’ (π₯ β π β¦ βπ β π§ π΅) = (π¦ β π β¦ βπ β π§ β¦π¦ / π₯β¦π΅) |
61 | 60 | eleq1i 2824 |
. . . . . . 7
β’ ((π₯ β π β¦ βπ β π§ π΅) β (π½ Cn πΎ) β (π¦ β π β¦ βπ β π§ β¦π¦ / π₯β¦π΅) β (π½ Cn πΎ)) |
62 | 61 | biimpi 215 |
. . . . . 6
β’ ((π₯ β π β¦ βπ β π§ π΅) β (π½ Cn πΎ) β (π¦ β π β¦ βπ β π§ β¦π¦ / π₯β¦π΅) β (π½ Cn πΎ)) |
63 | 62 | adantl 482 |
. . . . 5
β’ (((π β§ (π§ β π΄ β§ π€ β (π΄ β π§))) β§ (π₯ β π β¦ βπ β π§ π΅) β (π½ Cn πΎ)) β (π¦ β π β¦ βπ β π§ β¦π¦ / π₯β¦π΅) β (π½ Cn πΎ)) |
64 | 43, 20, 44, 46, 53, 54, 55, 63 | fprodcnlem 44305 |
. . . 4
β’ (((π β§ (π§ β π΄ β§ π€ β (π΄ β π§))) β§ (π₯ β π β¦ βπ β π§ π΅) β (π½ Cn πΎ)) β (π¦ β π β¦ βπ β (π§ βͺ {π€})β¦π¦ / π₯β¦π΅) β (π½ Cn πΎ)) |
65 | 33, 64 | eqeltrd 2833 |
. . 3
β’ (((π β§ (π§ β π΄ β§ π€ β (π΄ β π§))) β§ (π₯ β π β¦ βπ β π§ π΅) β (π½ Cn πΎ)) β (π₯ β π β¦ βπ β (π§ βͺ {π€})π΅) β (π½ Cn πΎ)) |
66 | 65 | ex 413 |
. 2
β’ ((π β§ (π§ β π΄ β§ π€ β (π΄ β π§))) β ((π₯ β π β¦ βπ β π§ π΅) β (π½ Cn πΎ) β (π₯ β π β¦ βπ β (π§ βͺ {π€})π΅) β (π½ Cn πΎ))) |
67 | 3, 6, 9, 12, 25, 66, 45 | findcard2d 9165 |
1
β’ (π β (π₯ β π β¦ βπ β π΄ π΅) β (π½ Cn πΎ)) |