Step | Hyp | Ref
| Expression |
1 | | txlm.f |
. . . . . . 7
β’ (π β πΉ:πβΆπ) |
2 | 1 | ffvelcdmda 7039 |
. . . . . 6
β’ ((π β§ π β π) β (πΉβπ) β π) |
3 | | txlm.g |
. . . . . . 7
β’ (π β πΊ:πβΆπ) |
4 | 3 | ffvelcdmda 7039 |
. . . . . 6
β’ ((π β§ π β π) β (πΊβπ) β π) |
5 | 2, 4 | opelxpd 5675 |
. . . . 5
β’ ((π β§ π β π) β β¨(πΉβπ), (πΊβπ)β© β (π Γ π)) |
6 | | eqidd 2734 |
. . . . 5
β’ (π β (π β π β¦ β¨(πΉβπ), (πΊβπ)β©) = (π β π β¦ β¨(πΉβπ), (πΊβπ)β©)) |
7 | | txlm.j |
. . . . . . . 8
β’ (π β π½ β (TopOnβπ)) |
8 | | txlm.k |
. . . . . . . 8
β’ (π β πΎ β (TopOnβπ)) |
9 | | txtopon 22965 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π½ Γt πΎ) β (TopOnβ(π Γ π))) |
10 | 7, 8, 9 | syl2anc 585 |
. . . . . . 7
β’ (π β (π½ Γt πΎ) β (TopOnβ(π Γ π))) |
11 | | lmcn2.o |
. . . . . . . . 9
β’ (π β π β ((π½ Γt πΎ) Cn π)) |
12 | | cntop2 22615 |
. . . . . . . . 9
β’ (π β ((π½ Γt πΎ) Cn π) β π β Top) |
13 | 11, 12 | syl 17 |
. . . . . . . 8
β’ (π β π β Top) |
14 | | toptopon2 22290 |
. . . . . . . 8
β’ (π β Top β π β (TopOnββͺ π)) |
15 | 13, 14 | sylib 217 |
. . . . . . 7
β’ (π β π β (TopOnββͺ π)) |
16 | | cnf2 22623 |
. . . . . . 7
β’ (((π½ Γt πΎ) β (TopOnβ(π Γ π)) β§ π β (TopOnββͺ π)
β§ π β ((π½ Γt πΎ) Cn π)) β π:(π Γ π)βΆβͺ π) |
17 | 10, 15, 11, 16 | syl3anc 1372 |
. . . . . 6
β’ (π β π:(π Γ π)βΆβͺ π) |
18 | 17 | feqmptd 6914 |
. . . . 5
β’ (π β π = (π₯ β (π Γ π) β¦ (πβπ₯))) |
19 | | fveq2 6846 |
. . . . . 6
β’ (π₯ = β¨(πΉβπ), (πΊβπ)β© β (πβπ₯) = (πββ¨(πΉβπ), (πΊβπ)β©)) |
20 | | df-ov 7364 |
. . . . . 6
β’ ((πΉβπ)π(πΊβπ)) = (πββ¨(πΉβπ), (πΊβπ)β©) |
21 | 19, 20 | eqtr4di 2791 |
. . . . 5
β’ (π₯ = β¨(πΉβπ), (πΊβπ)β© β (πβπ₯) = ((πΉβπ)π(πΊβπ))) |
22 | 5, 6, 18, 21 | fmptco 7079 |
. . . 4
β’ (π β (π β (π β π β¦ β¨(πΉβπ), (πΊβπ)β©)) = (π β π β¦ ((πΉβπ)π(πΊβπ)))) |
23 | | lmcn2.h |
. . . 4
β’ π» = (π β π β¦ ((πΉβπ)π(πΊβπ))) |
24 | 22, 23 | eqtr4di 2791 |
. . 3
β’ (π β (π β (π β π β¦ β¨(πΉβπ), (πΊβπ)β©)) = π») |
25 | | lmcn2.fl |
. . . . 5
β’ (π β πΉ(βπ‘βπ½)π
) |
26 | | lmcn2.gl |
. . . . 5
β’ (π β πΊ(βπ‘βπΎ)π) |
27 | | txlm.z |
. . . . . 6
β’ π =
(β€β₯βπ) |
28 | | txlm.m |
. . . . . 6
β’ (π β π β β€) |
29 | | eqid 2733 |
. . . . . 6
β’ (π β π β¦ β¨(πΉβπ), (πΊβπ)β©) = (π β π β¦ β¨(πΉβπ), (πΊβπ)β©) |
30 | 27, 28, 7, 8, 1, 3, 29 | txlm 23022 |
. . . . 5
β’ (π β ((πΉ(βπ‘βπ½)π
β§ πΊ(βπ‘βπΎ)π) β (π β π β¦ β¨(πΉβπ), (πΊβπ)β©)(βπ‘β(π½ Γt πΎ))β¨π
, πβ©)) |
31 | 25, 26, 30 | mpbi2and 711 |
. . . 4
β’ (π β (π β π β¦ β¨(πΉβπ), (πΊβπ)β©)(βπ‘β(π½ Γt πΎ))β¨π
, πβ©) |
32 | 31, 11 | lmcn 22679 |
. . 3
β’ (π β (π β (π β π β¦ β¨(πΉβπ), (πΊβπ)β©))(βπ‘βπ)(πββ¨π
, πβ©)) |
33 | 24, 32 | eqbrtrrd 5133 |
. 2
β’ (π β π»(βπ‘βπ)(πββ¨π
, πβ©)) |
34 | | df-ov 7364 |
. 2
β’ (π
ππ) = (πββ¨π
, πβ©) |
35 | 33, 34 | breqtrrdi 5151 |
1
β’ (π β π»(βπ‘βπ)(π
ππ)) |