Step | Hyp | Ref
| Expression |
1 | | eqid 2730 |
. . . . . . 7
β’
(TopOpenββfld) =
(TopOpenββfld) |
2 | 1 | cnfldtopon 24519 |
. . . . . 6
β’
(TopOpenββfld) β
(TopOnββ) |
3 | 2 | a1i 11 |
. . . . 5
β’ (π β
(TopOpenββfld) β
(TopOnββ)) |
4 | 3 | cnmptid 23385 |
. . . . 5
β’ (π β (π₯ β β β¦ π₯) β
((TopOpenββfld) Cn
(TopOpenββfld))) |
5 | | rmulccn.2 |
. . . . . . 7
β’ (π β πΆ β β) |
6 | 5 | recnd 11246 |
. . . . . 6
β’ (π β πΆ β β) |
7 | 3, 3, 6 | cnmptc 23386 |
. . . . 5
β’ (π β (π₯ β β β¦ πΆ) β
((TopOpenββfld) Cn
(TopOpenββfld))) |
8 | | ax-mulf 11192 |
. . . . . . . . 9
β’ Β·
:(β Γ β)βΆβ |
9 | | ffn 6716 |
. . . . . . . . 9
β’ (
Β· :(β Γ β)βΆβ β Β· Fn (β
Γ β)) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . 8
β’ Β·
Fn (β Γ β) |
11 | | fnov 7542 |
. . . . . . . 8
β’ (
Β· Fn (β Γ β) β Β· = (π¦ β β, π§ β β β¦ (π¦ Β· π§))) |
12 | 10, 11 | mpbi 229 |
. . . . . . 7
β’ Β·
= (π¦ β β, π§ β β β¦ (π¦ Β· π§)) |
13 | 1 | mulcn 24603 |
. . . . . . 7
β’ Β·
β (((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld)) |
14 | 12, 13 | eqeltrri 2828 |
. . . . . 6
β’ (π¦ β β, π§ β β β¦ (π¦ Β· π§)) β
(((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld)) |
15 | 14 | a1i 11 |
. . . . 5
β’ (π β (π¦ β β, π§ β β β¦ (π¦ Β· π§)) β
(((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld))) |
16 | | oveq12 7420 |
. . . . 5
β’ ((π¦ = π₯ β§ π§ = πΆ) β (π¦ Β· π§) = (π₯ Β· πΆ)) |
17 | 3, 4, 7, 3, 3, 15,
16 | cnmpt12 23391 |
. . . 4
β’ (π β (π₯ β β β¦ (π₯ Β· πΆ)) β
((TopOpenββfld) Cn
(TopOpenββfld))) |
18 | | ax-resscn 11169 |
. . . 4
β’ β
β β |
19 | 2 | toponunii 22638 |
. . . . 5
β’ β =
βͺ
(TopOpenββfld) |
20 | 19 | cnrest 23009 |
. . . 4
β’ (((π₯ β β β¦ (π₯ Β· πΆ)) β
((TopOpenββfld) Cn
(TopOpenββfld)) β§ β β β) β
((π₯ β β β¦
(π₯ Β· πΆ)) βΎ β) β
(((TopOpenββfld) βΎt β) Cn
(TopOpenββfld))) |
21 | 17, 18, 20 | sylancl 584 |
. . 3
β’ (π β ((π₯ β β β¦ (π₯ Β· πΆ)) βΎ β) β
(((TopOpenββfld) βΎt β) Cn
(TopOpenββfld))) |
22 | | simpr 483 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β π₯ β β) |
23 | 6 | adantr 479 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β πΆ β β) |
24 | 22, 23 | mulcld 11238 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β (π₯ Β· πΆ) β β) |
25 | 24 | ralrimiva 3144 |
. . . . . . 7
β’ (π β βπ₯ β β (π₯ Β· πΆ) β β) |
26 | | eqid 2730 |
. . . . . . . 8
β’ (π₯ β β β¦ (π₯ Β· πΆ)) = (π₯ β β β¦ (π₯ Β· πΆ)) |
27 | 26 | fnmpt 6689 |
. . . . . . 7
β’
(βπ₯ β
β (π₯ Β· πΆ) β β β (π₯ β β β¦ (π₯ Β· πΆ)) Fn β) |
28 | 25, 27 | syl 17 |
. . . . . 6
β’ (π β (π₯ β β β¦ (π₯ Β· πΆ)) Fn β) |
29 | | fnssres 6672 |
. . . . . 6
β’ (((π₯ β β β¦ (π₯ Β· πΆ)) Fn β β§ β β β)
β ((π₯ β β
β¦ (π₯ Β· πΆ)) βΎ β) Fn
β) |
30 | 28, 18, 29 | sylancl 584 |
. . . . 5
β’ (π β ((π₯ β β β¦ (π₯ Β· πΆ)) βΎ β) Fn
β) |
31 | | simpr 483 |
. . . . . . . 8
β’ ((π β§ π€ β β) β π€ β β) |
32 | | fvres 6909 |
. . . . . . . . 9
β’ (π€ β β β (((π₯ β β β¦ (π₯ Β· πΆ)) βΎ β)βπ€) = ((π₯ β β β¦ (π₯ Β· πΆ))βπ€)) |
33 | | recn 11202 |
. . . . . . . . . 10
β’ (π€ β β β π€ β
β) |
34 | | oveq1 7418 |
. . . . . . . . . . 11
β’ (π₯ = π€ β (π₯ Β· πΆ) = (π€ Β· πΆ)) |
35 | | ovex 7444 |
. . . . . . . . . . 11
β’ (π€ Β· πΆ) β V |
36 | 34, 26, 35 | fvmpt 6997 |
. . . . . . . . . 10
β’ (π€ β β β ((π₯ β β β¦ (π₯ Β· πΆ))βπ€) = (π€ Β· πΆ)) |
37 | 33, 36 | syl 17 |
. . . . . . . . 9
β’ (π€ β β β ((π₯ β β β¦ (π₯ Β· πΆ))βπ€) = (π€ Β· πΆ)) |
38 | 32, 37 | eqtrd 2770 |
. . . . . . . 8
β’ (π€ β β β (((π₯ β β β¦ (π₯ Β· πΆ)) βΎ β)βπ€) = (π€ Β· πΆ)) |
39 | 31, 38 | syl 17 |
. . . . . . 7
β’ ((π β§ π€ β β) β (((π₯ β β β¦ (π₯ Β· πΆ)) βΎ β)βπ€) = (π€ Β· πΆ)) |
40 | 5 | adantr 479 |
. . . . . . . 8
β’ ((π β§ π€ β β) β πΆ β β) |
41 | 31, 40 | remulcld 11248 |
. . . . . . 7
β’ ((π β§ π€ β β) β (π€ Β· πΆ) β β) |
42 | 39, 41 | eqeltrd 2831 |
. . . . . 6
β’ ((π β§ π€ β β) β (((π₯ β β β¦ (π₯ Β· πΆ)) βΎ β)βπ€) β β) |
43 | 42 | ralrimiva 3144 |
. . . . 5
β’ (π β βπ€ β β (((π₯ β β β¦ (π₯ Β· πΆ)) βΎ β)βπ€) β β) |
44 | | fnfvrnss 7121 |
. . . . 5
β’ ((((π₯ β β β¦ (π₯ Β· πΆ)) βΎ β) Fn β β§
βπ€ β β
(((π₯ β β β¦
(π₯ Β· πΆ)) βΎ β)βπ€) β β) β ran
((π₯ β β β¦
(π₯ Β· πΆ)) βΎ β) β
β) |
45 | 30, 43, 44 | syl2anc 582 |
. . . 4
β’ (π β ran ((π₯ β β β¦ (π₯ Β· πΆ)) βΎ β) β
β) |
46 | 18 | a1i 11 |
. . . 4
β’ (π β β β
β) |
47 | | cnrest2 23010 |
. . . 4
β’
(((TopOpenββfld) β (TopOnββ)
β§ ran ((π₯ β
β β¦ (π₯ Β·
πΆ)) βΎ β)
β β β§ β β β) β (((π₯ β β β¦ (π₯ Β· πΆ)) βΎ β) β
(((TopOpenββfld) βΎt β) Cn
(TopOpenββfld)) β ((π₯ β β β¦ (π₯ Β· πΆ)) βΎ β) β
(((TopOpenββfld) βΎt β) Cn
((TopOpenββfld) βΎt
β)))) |
48 | 3, 45, 46, 47 | syl3anc 1369 |
. . 3
β’ (π β (((π₯ β β β¦ (π₯ Β· πΆ)) βΎ β) β
(((TopOpenββfld) βΎt β) Cn
(TopOpenββfld)) β ((π₯ β β β¦ (π₯ Β· πΆ)) βΎ β) β
(((TopOpenββfld) βΎt β) Cn
((TopOpenββfld) βΎt
β)))) |
49 | 21, 48 | mpbid 231 |
. 2
β’ (π β ((π₯ β β β¦ (π₯ Β· πΆ)) βΎ β) β
(((TopOpenββfld) βΎt β) Cn
((TopOpenββfld) βΎt
β))) |
50 | | resmpt 6036 |
. . 3
β’ (β
β β β ((π₯
β β β¦ (π₯
Β· πΆ)) βΎ
β) = (π₯ β
β β¦ (π₯ Β·
πΆ))) |
51 | 18, 50 | ax-mp 5 |
. 2
β’ ((π₯ β β β¦ (π₯ Β· πΆ)) βΎ β) = (π₯ β β β¦ (π₯ Β· πΆ)) |
52 | | rmulccn.1 |
. . . . 5
β’ π½ = (topGenβran
(,)) |
53 | 1 | tgioo2 24539 |
. . . . 5
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
54 | 52, 53 | eqtri 2758 |
. . . 4
β’ π½ =
((TopOpenββfld) βΎt
β) |
55 | 54, 54 | oveq12i 7423 |
. . 3
β’ (π½ Cn π½) = (((TopOpenββfld)
βΎt β) Cn ((TopOpenββfld)
βΎt β)) |
56 | 55 | eqcomi 2739 |
. 2
β’
(((TopOpenββfld) βΎt β) Cn
((TopOpenββfld) βΎt β)) = (π½ Cn π½) |
57 | 49, 51, 56 | 3eltr3g 2847 |
1
β’ (π β (π₯ β β β¦ (π₯ Β· πΆ)) β (π½ Cn π½)) |