Step | Hyp | Ref
| Expression |
1 | | fprodcnlem.1 |
. . . . 5
β’
β²ππ |
2 | | nfv 1918 |
. . . . 5
β’
β²π π₯ β π |
3 | 1, 2 | nfan 1903 |
. . . 4
β’
β²π(π β§ π₯ β π) |
4 | | nfcsb1v 3919 |
. . . 4
β’
β²πβ¦π / πβ¦π΅ |
5 | | fprodcnlem.a |
. . . . . 6
β’ (π β π΄ β Fin) |
6 | | fprodcnlem.z |
. . . . . 6
β’ (π β π β π΄) |
7 | 5, 6 | ssfid 9267 |
. . . . 5
β’ (π β π β Fin) |
8 | 7 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β π) β π β Fin) |
9 | | fprodcnlem.w |
. . . . 5
β’ (π β π β (π΄ β π)) |
10 | 9 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β π) β π β (π΄ β π)) |
11 | 10 | eldifbd 3962 |
. . . 4
β’ ((π β§ π₯ β π) β Β¬ π β π) |
12 | 6 | sselda 3983 |
. . . . . 6
β’ ((π β§ π β π) β π β π΄) |
13 | 12 | adantlr 714 |
. . . . 5
β’ (((π β§ π₯ β π) β§ π β π) β π β π΄) |
14 | | fprodcnlem.j |
. . . . . . . . . 10
β’ (π β π½ β (TopOnβπ)) |
15 | 14 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β π½ β (TopOnβπ)) |
16 | | fprodcnlem.k |
. . . . . . . . . . 11
β’ πΎ =
(TopOpenββfld) |
17 | 16 | cnfldtopon 24299 |
. . . . . . . . . 10
β’ πΎ β
(TopOnββ) |
18 | 17 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β πΎ β
(TopOnββ)) |
19 | | fprodcnlem.b |
. . . . . . . . 9
β’ ((π β§ π β π΄) β (π₯ β π β¦ π΅) β (π½ Cn πΎ)) |
20 | | cnf2 22753 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnββ) β§ (π₯ β π β¦ π΅) β (π½ Cn πΎ)) β (π₯ β π β¦ π΅):πβΆβ) |
21 | 15, 18, 19, 20 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ π β π΄) β (π₯ β π β¦ π΅):πβΆβ) |
22 | | eqid 2733 |
. . . . . . . . 9
β’ (π₯ β π β¦ π΅) = (π₯ β π β¦ π΅) |
23 | 22 | fmpt 7110 |
. . . . . . . 8
β’
(βπ₯ β
π π΅ β β β (π₯ β π β¦ π΅):πβΆβ) |
24 | 21, 23 | sylibr 233 |
. . . . . . 7
β’ ((π β§ π β π΄) β βπ₯ β π π΅ β β) |
25 | 24 | adantlr 714 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ π β π΄) β βπ₯ β π π΅ β β) |
26 | | simplr 768 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ π β π΄) β π₯ β π) |
27 | | rspa 3246 |
. . . . . 6
β’
((βπ₯ β
π π΅ β β β§ π₯ β π) β π΅ β β) |
28 | 25, 26, 27 | syl2anc 585 |
. . . . 5
β’ (((π β§ π₯ β π) β§ π β π΄) β π΅ β β) |
29 | 13, 28 | syldan 592 |
. . . 4
β’ (((π β§ π₯ β π) β§ π β π) β π΅ β β) |
30 | | csbeq1a 3908 |
. . . 4
β’ (π = π β π΅ = β¦π / πβ¦π΅) |
31 | 10 | eldifad 3961 |
. . . . 5
β’ ((π β§ π₯ β π) β π β π΄) |
32 | | simpr 486 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ π β π΄) β π β π΄) |
33 | | nfcv 2904 |
. . . . . . 7
β’
β²ππ |
34 | | nfv 1918 |
. . . . . . . . 9
β’
β²π π β π΄ |
35 | 3, 34 | nfan 1903 |
. . . . . . . 8
β’
β²π((π β§ π₯ β π) β§ π β π΄) |
36 | 4 | nfel1 2920 |
. . . . . . . 8
β’
β²πβ¦π / πβ¦π΅ β β |
37 | 35, 36 | nfim 1900 |
. . . . . . 7
β’
β²π(((π β§ π₯ β π) β§ π β π΄) β β¦π / πβ¦π΅ β β) |
38 | | eleq1 2822 |
. . . . . . . . 9
β’ (π = π β (π β π΄ β π β π΄)) |
39 | 38 | anbi2d 630 |
. . . . . . . 8
β’ (π = π β (((π β§ π₯ β π) β§ π β π΄) β ((π β§ π₯ β π) β§ π β π΄))) |
40 | 30 | eleq1d 2819 |
. . . . . . . 8
β’ (π = π β (π΅ β β β β¦π / πβ¦π΅ β β)) |
41 | 39, 40 | imbi12d 345 |
. . . . . . 7
β’ (π = π β ((((π β§ π₯ β π) β§ π β π΄) β π΅ β β) β (((π β§ π₯ β π) β§ π β π΄) β β¦π / πβ¦π΅ β β))) |
42 | 33, 37, 41, 28 | vtoclgf 3555 |
. . . . . 6
β’ (π β π΄ β (((π β§ π₯ β π) β§ π β π΄) β β¦π / πβ¦π΅ β β)) |
43 | 32, 42 | mpcom 38 |
. . . . 5
β’ (((π β§ π₯ β π) β§ π β π΄) β β¦π / πβ¦π΅ β β) |
44 | 31, 43 | mpdan 686 |
. . . 4
β’ ((π β§ π₯ β π) β β¦π / πβ¦π΅ β β) |
45 | 3, 4, 8, 10, 11, 29, 30, 44 | fprodsplitsn 15933 |
. . 3
β’ ((π β§ π₯ β π) β βπ β (π βͺ {π})π΅ = (βπ β π π΅ Β· β¦π / πβ¦π΅)) |
46 | 45 | mpteq2dva 5249 |
. 2
β’ (π β (π₯ β π β¦ βπ β (π βͺ {π})π΅) = (π₯ β π β¦ (βπ β π π΅ Β· β¦π / πβ¦π΅))) |
47 | | fprodcnlem.p |
. . 3
β’ (π β (π₯ β π β¦ βπ β π π΅) β (π½ Cn πΎ)) |
48 | 9 | eldifad 3961 |
. . . 4
β’ (π β π β π΄) |
49 | 1, 34 | nfan 1903 |
. . . . . . 7
β’
β²π(π β§ π β π΄) |
50 | | nfcv 2904 |
. . . . . . . . 9
β’
β²ππ |
51 | 50, 4 | nfmpt 5256 |
. . . . . . . 8
β’
β²π(π₯ β π β¦ β¦π / πβ¦π΅) |
52 | | nfcv 2904 |
. . . . . . . 8
β’
β²π(π½ Cn πΎ) |
53 | 51, 52 | nfel 2918 |
. . . . . . 7
β’
β²π(π₯ β π β¦ β¦π / πβ¦π΅) β (π½ Cn πΎ) |
54 | 49, 53 | nfim 1900 |
. . . . . 6
β’
β²π((π β§ π β π΄) β (π₯ β π β¦ β¦π / πβ¦π΅) β (π½ Cn πΎ)) |
55 | 38 | anbi2d 630 |
. . . . . . 7
β’ (π = π β ((π β§ π β π΄) β (π β§ π β π΄))) |
56 | 30 | mpteq2dv 5251 |
. . . . . . . 8
β’ (π = π β (π₯ β π β¦ π΅) = (π₯ β π β¦ β¦π / πβ¦π΅)) |
57 | 56 | eleq1d 2819 |
. . . . . . 7
β’ (π = π β ((π₯ β π β¦ π΅) β (π½ Cn πΎ) β (π₯ β π β¦ β¦π / πβ¦π΅) β (π½ Cn πΎ))) |
58 | 55, 57 | imbi12d 345 |
. . . . . 6
β’ (π = π β (((π β§ π β π΄) β (π₯ β π β¦ π΅) β (π½ Cn πΎ)) β ((π β§ π β π΄) β (π₯ β π β¦ β¦π / πβ¦π΅) β (π½ Cn πΎ)))) |
59 | 19 | idi 1 |
. . . . . 6
β’ ((π β§ π β π΄) β (π₯ β π β¦ π΅) β (π½ Cn πΎ)) |
60 | 33, 54, 58, 59 | vtoclgf 3555 |
. . . . 5
β’ (π β π΄ β ((π β§ π β π΄) β (π₯ β π β¦ β¦π / πβ¦π΅) β (π½ Cn πΎ))) |
61 | 60 | anabsi7 670 |
. . . 4
β’ ((π β§ π β π΄) β (π₯ β π β¦ β¦π / πβ¦π΅) β (π½ Cn πΎ)) |
62 | 48, 61 | mpdan 686 |
. . 3
β’ (π β (π₯ β π β¦ β¦π / πβ¦π΅) β (π½ Cn πΎ)) |
63 | 16 | mulcn 24383 |
. . . 4
β’ Β·
β ((πΎ
Γt πΎ) Cn
πΎ) |
64 | 63 | a1i 11 |
. . 3
β’ (π β Β· β ((πΎ Γt πΎ) Cn πΎ)) |
65 | 14, 47, 62, 64 | cnmpt12f 23170 |
. 2
β’ (π β (π₯ β π β¦ (βπ β π π΅ Β· β¦π / πβ¦π΅)) β (π½ Cn πΎ)) |
66 | 46, 65 | eqeltrd 2834 |
1
β’ (π β (π₯ β π β¦ βπ β (π βͺ {π})π΅) β (π½ Cn πΎ)) |