Step | Hyp | Ref
| Expression |
1 | | nlmlmod 24065 |
. . . 4
β’ (π β NrmMod β π β LMod) |
2 | | eqid 2733 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
3 | | nlmvscn.f |
. . . . 5
β’ πΉ = (Scalarβπ) |
4 | | eqid 2733 |
. . . . 5
β’
(BaseβπΉ) =
(BaseβπΉ) |
5 | | nlmvscn.sf |
. . . . 5
β’ Β· = (
Β·sf βπ) |
6 | 2, 3, 4, 5 | lmodscaf 20388 |
. . . 4
β’ (π β LMod β Β·
:((BaseβπΉ) Γ
(Baseβπ))βΆ(Baseβπ)) |
7 | 1, 6 | syl 17 |
. . 3
β’ (π β NrmMod β Β·
:((BaseβπΉ) Γ
(Baseβπ))βΆ(Baseβπ)) |
8 | | eqid 2733 |
. . . . . . 7
β’
(distβπ) =
(distβπ) |
9 | | eqid 2733 |
. . . . . . 7
β’
(distβπΉ) =
(distβπΉ) |
10 | | eqid 2733 |
. . . . . . 7
β’
(normβπ) =
(normβπ) |
11 | | eqid 2733 |
. . . . . . 7
β’
(normβπΉ) =
(normβπΉ) |
12 | | eqid 2733 |
. . . . . . 7
β’ (
Β·π βπ) = ( Β·π
βπ) |
13 | | eqid 2733 |
. . . . . . 7
β’ ((π / 2) / (((normβπΉ)βπ₯) + 1)) = ((π / 2) / (((normβπΉ)βπ₯) + 1)) |
14 | | eqid 2733 |
. . . . . . 7
β’ ((π / 2) / (((normβπ)βπ¦) + ((π / 2) / (((normβπΉ)βπ₯) + 1)))) = ((π / 2) / (((normβπ)βπ¦) + ((π / 2) / (((normβπΉ)βπ₯) + 1)))) |
15 | | simpll 766 |
. . . . . . 7
β’ (((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β§ π β β+) β π β NrmMod) |
16 | | simpr 486 |
. . . . . . 7
β’ (((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β§ π β β+) β π β
β+) |
17 | | simplrl 776 |
. . . . . . 7
β’ (((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β§ π β β+) β π₯ β (BaseβπΉ)) |
18 | | simplrr 777 |
. . . . . . 7
β’ (((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β§ π β β+) β π¦ β (Baseβπ)) |
19 | 3, 2, 4, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 18 | nlmvscnlem1 24073 |
. . . . . 6
β’ (((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β§ π β β+) β
βπ β
β+ βπ§ β (BaseβπΉ)βπ€ β (Baseβπ)(((π₯(distβπΉ)π§) < π β§ (π¦(distβπ)π€) < π ) β ((π₯( Β·π
βπ)π¦)(distβπ)(π§( Β·π
βπ)π€)) < π)) |
20 | 19 | ralrimiva 3140 |
. . . . 5
β’ ((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β βπ β β+ βπ β β+
βπ§ β
(BaseβπΉ)βπ€ β (Baseβπ)(((π₯(distβπΉ)π§) < π β§ (π¦(distβπ)π€) < π ) β ((π₯( Β·π
βπ)π¦)(distβπ)(π§( Β·π
βπ)π€)) < π)) |
21 | | simplrl 776 |
. . . . . . . . . . . 12
β’ (((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β§ (π§ β (BaseβπΉ) β§ π€ β (Baseβπ))) β π₯ β (BaseβπΉ)) |
22 | | simprl 770 |
. . . . . . . . . . . 12
β’ (((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β§ (π§ β (BaseβπΉ) β§ π€ β (Baseβπ))) β π§ β (BaseβπΉ)) |
23 | 21, 22 | ovresd 7525 |
. . . . . . . . . . 11
β’ (((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β§ (π§ β (BaseβπΉ) β§ π€ β (Baseβπ))) β (π₯((distβπΉ) βΎ ((BaseβπΉ) Γ (BaseβπΉ)))π§) = (π₯(distβπΉ)π§)) |
24 | 23 | breq1d 5119 |
. . . . . . . . . 10
β’ (((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β§ (π§ β (BaseβπΉ) β§ π€ β (Baseβπ))) β ((π₯((distβπΉ) βΎ ((BaseβπΉ) Γ (BaseβπΉ)))π§) < π β (π₯(distβπΉ)π§) < π )) |
25 | | simplrr 777 |
. . . . . . . . . . . 12
β’ (((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β§ (π§ β (BaseβπΉ) β§ π€ β (Baseβπ))) β π¦ β (Baseβπ)) |
26 | | simprr 772 |
. . . . . . . . . . . 12
β’ (((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β§ (π§ β (BaseβπΉ) β§ π€ β (Baseβπ))) β π€ β (Baseβπ)) |
27 | 25, 26 | ovresd 7525 |
. . . . . . . . . . 11
β’ (((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β§ (π§ β (BaseβπΉ) β§ π€ β (Baseβπ))) β (π¦((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π€) = (π¦(distβπ)π€)) |
28 | 27 | breq1d 5119 |
. . . . . . . . . 10
β’ (((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β§ (π§ β (BaseβπΉ) β§ π€ β (Baseβπ))) β ((π¦((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π€) < π β (π¦(distβπ)π€) < π )) |
29 | 24, 28 | anbi12d 632 |
. . . . . . . . 9
β’ (((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β§ (π§ β (BaseβπΉ) β§ π€ β (Baseβπ))) β (((π₯((distβπΉ) βΎ ((BaseβπΉ) Γ (BaseβπΉ)))π§) < π β§ (π¦((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π€) < π ) β ((π₯(distβπΉ)π§) < π β§ (π¦(distβπ)π€) < π ))) |
30 | 2, 3, 4, 5, 12 | scafval 20385 |
. . . . . . . . . . . . 13
β’ ((π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ)) β (π₯ Β· π¦) = (π₯( Β·π
βπ)π¦)) |
31 | 30 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ (((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β§ (π§ β (BaseβπΉ) β§ π€ β (Baseβπ))) β (π₯ Β· π¦) = (π₯( Β·π
βπ)π¦)) |
32 | 2, 3, 4, 5, 12 | scafval 20385 |
. . . . . . . . . . . . 13
β’ ((π§ β (BaseβπΉ) β§ π€ β (Baseβπ)) β (π§ Β· π€) = (π§( Β·π
βπ)π€)) |
33 | 32 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β§ (π§ β (BaseβπΉ) β§ π€ β (Baseβπ))) β (π§ Β· π€) = (π§( Β·π
βπ)π€)) |
34 | 31, 33 | oveq12d 7379 |
. . . . . . . . . . 11
β’ (((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β§ (π§ β (BaseβπΉ) β§ π€ β (Baseβπ))) β ((π₯ Β· π¦)((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))(π§ Β· π€)) = ((π₯( Β·π
βπ)π¦)((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))(π§( Β·π
βπ)π€))) |
35 | 1 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β§ (π§ β (BaseβπΉ) β§ π€ β (Baseβπ))) β π β LMod) |
36 | 2, 3, 12, 4 | lmodvscl 20383 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ)) β (π₯( Β·π
βπ)π¦) β (Baseβπ)) |
37 | 35, 21, 25, 36 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β§ (π§ β (BaseβπΉ) β§ π€ β (Baseβπ))) β (π₯( Β·π
βπ)π¦) β (Baseβπ)) |
38 | 2, 3, 12, 4 | lmodvscl 20383 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ π§ β (BaseβπΉ) β§ π€ β (Baseβπ)) β (π§( Β·π
βπ)π€) β (Baseβπ)) |
39 | 35, 22, 26, 38 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β§ (π§ β (BaseβπΉ) β§ π€ β (Baseβπ))) β (π§( Β·π
βπ)π€) β (Baseβπ)) |
40 | 37, 39 | ovresd 7525 |
. . . . . . . . . . 11
β’ (((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β§ (π§ β (BaseβπΉ) β§ π€ β (Baseβπ))) β ((π₯( Β·π
βπ)π¦)((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))(π§( Β·π
βπ)π€)) = ((π₯( Β·π
βπ)π¦)(distβπ)(π§( Β·π
βπ)π€))) |
41 | 34, 40 | eqtrd 2773 |
. . . . . . . . . 10
β’ (((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β§ (π§ β (BaseβπΉ) β§ π€ β (Baseβπ))) β ((π₯ Β· π¦)((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))(π§ Β· π€)) = ((π₯( Β·π
βπ)π¦)(distβπ)(π§( Β·π
βπ)π€))) |
42 | 41 | breq1d 5119 |
. . . . . . . . 9
β’ (((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β§ (π§ β (BaseβπΉ) β§ π€ β (Baseβπ))) β (((π₯ Β· π¦)((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))(π§ Β· π€)) < π β ((π₯( Β·π
βπ)π¦)(distβπ)(π§( Β·π
βπ)π€)) < π)) |
43 | 29, 42 | imbi12d 345 |
. . . . . . . 8
β’ (((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β§ (π§ β (BaseβπΉ) β§ π€ β (Baseβπ))) β ((((π₯((distβπΉ) βΎ ((BaseβπΉ) Γ (BaseβπΉ)))π§) < π β§ (π¦((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π€) < π ) β ((π₯ Β· π¦)((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))(π§ Β· π€)) < π) β (((π₯(distβπΉ)π§) < π β§ (π¦(distβπ)π€) < π ) β ((π₯( Β·π
βπ)π¦)(distβπ)(π§( Β·π
βπ)π€)) < π))) |
44 | 43 | 2ralbidva 3207 |
. . . . . . 7
β’ ((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β (βπ§ β (BaseβπΉ)βπ€ β (Baseβπ)(((π₯((distβπΉ) βΎ ((BaseβπΉ) Γ (BaseβπΉ)))π§) < π β§ (π¦((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π€) < π ) β ((π₯ Β· π¦)((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))(π§ Β· π€)) < π) β βπ§ β (BaseβπΉ)βπ€ β (Baseβπ)(((π₯(distβπΉ)π§) < π β§ (π¦(distβπ)π€) < π ) β ((π₯( Β·π
βπ)π¦)(distβπ)(π§( Β·π
βπ)π€)) < π))) |
45 | 44 | rexbidv 3172 |
. . . . . 6
β’ ((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β (βπ β β+ βπ§ β (BaseβπΉ)βπ€ β (Baseβπ)(((π₯((distβπΉ) βΎ ((BaseβπΉ) Γ (BaseβπΉ)))π§) < π β§ (π¦((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π€) < π ) β ((π₯ Β· π¦)((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))(π§ Β· π€)) < π) β βπ β β+ βπ§ β (BaseβπΉ)βπ€ β (Baseβπ)(((π₯(distβπΉ)π§) < π β§ (π¦(distβπ)π€) < π ) β ((π₯( Β·π
βπ)π¦)(distβπ)(π§( Β·π
βπ)π€)) < π))) |
46 | 45 | ralbidv 3171 |
. . . . 5
β’ ((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β (βπ β β+ βπ β β+
βπ§ β
(BaseβπΉ)βπ€ β (Baseβπ)(((π₯((distβπΉ) βΎ ((BaseβπΉ) Γ (BaseβπΉ)))π§) < π β§ (π¦((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π€) < π ) β ((π₯ Β· π¦)((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))(π§ Β· π€)) < π) β βπ β β+ βπ β β+
βπ§ β
(BaseβπΉ)βπ€ β (Baseβπ)(((π₯(distβπΉ)π§) < π β§ (π¦(distβπ)π€) < π ) β ((π₯( Β·π
βπ)π¦)(distβπ)(π§( Β·π
βπ)π€)) < π))) |
47 | 20, 46 | mpbird 257 |
. . . 4
β’ ((π β NrmMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (Baseβπ))) β βπ β β+ βπ β β+
βπ§ β
(BaseβπΉ)βπ€ β (Baseβπ)(((π₯((distβπΉ) βΎ ((BaseβπΉ) Γ (BaseβπΉ)))π§) < π β§ (π¦((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π€) < π ) β ((π₯ Β· π¦)((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))(π§ Β· π€)) < π)) |
48 | 47 | ralrimivva 3194 |
. . 3
β’ (π β NrmMod β
βπ₯ β
(BaseβπΉ)βπ¦ β (Baseβπ)βπ β β+ βπ β β+
βπ§ β
(BaseβπΉ)βπ€ β (Baseβπ)(((π₯((distβπΉ) βΎ ((BaseβπΉ) Γ (BaseβπΉ)))π§) < π β§ (π¦((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π€) < π ) β ((π₯ Β· π¦)((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))(π§ Β· π€)) < π)) |
49 | 3 | nlmngp2 24067 |
. . . . . 6
β’ (π β NrmMod β πΉ β NrmGrp) |
50 | | ngpms 23979 |
. . . . . 6
β’ (πΉ β NrmGrp β πΉ β MetSp) |
51 | 49, 50 | syl 17 |
. . . . 5
β’ (π β NrmMod β πΉ β MetSp) |
52 | | msxms 23830 |
. . . . 5
β’ (πΉ β MetSp β πΉ β
βMetSp) |
53 | | eqid 2733 |
. . . . . 6
β’
((distβπΉ)
βΎ ((BaseβπΉ)
Γ (BaseβπΉ))) =
((distβπΉ) βΎ
((BaseβπΉ) Γ
(BaseβπΉ))) |
54 | 4, 53 | xmsxmet 23832 |
. . . . 5
β’ (πΉ β βMetSp β
((distβπΉ) βΎ
((BaseβπΉ) Γ
(BaseβπΉ))) β
(βMetβ(BaseβπΉ))) |
55 | 51, 52, 54 | 3syl 18 |
. . . 4
β’ (π β NrmMod β
((distβπΉ) βΎ
((BaseβπΉ) Γ
(BaseβπΉ))) β
(βMetβ(BaseβπΉ))) |
56 | | nlmngp 24064 |
. . . . . 6
β’ (π β NrmMod β π β NrmGrp) |
57 | | ngpms 23979 |
. . . . . 6
β’ (π β NrmGrp β π β MetSp) |
58 | 56, 57 | syl 17 |
. . . . 5
β’ (π β NrmMod β π β MetSp) |
59 | | msxms 23830 |
. . . . 5
β’ (π β MetSp β π β
βMetSp) |
60 | | eqid 2733 |
. . . . . 6
β’
((distβπ)
βΎ ((Baseβπ)
Γ (Baseβπ))) =
((distβπ) βΎ
((Baseβπ) Γ
(Baseβπ))) |
61 | 2, 60 | xmsxmet 23832 |
. . . . 5
β’ (π β βMetSp β
((distβπ) βΎ
((Baseβπ) Γ
(Baseβπ))) β
(βMetβ(Baseβπ))) |
62 | 58, 59, 61 | 3syl 18 |
. . . 4
β’ (π β NrmMod β
((distβπ) βΎ
((Baseβπ) Γ
(Baseβπ))) β
(βMetβ(Baseβπ))) |
63 | | eqid 2733 |
. . . . 5
β’
(MetOpenβ((distβπΉ) βΎ ((BaseβπΉ) Γ (BaseβπΉ)))) = (MetOpenβ((distβπΉ) βΎ ((BaseβπΉ) Γ (BaseβπΉ)))) |
64 | | eqid 2733 |
. . . . 5
β’
(MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))) = (MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))) |
65 | 63, 64, 64 | txmetcn 23927 |
. . . 4
β’
((((distβπΉ)
βΎ ((BaseβπΉ)
Γ (BaseβπΉ)))
β (βMetβ(BaseβπΉ)) β§ ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ))) β
(βMetβ(Baseβπ)) β§ ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ))) β
(βMetβ(Baseβπ))) β ( Β· β
(((MetOpenβ((distβπΉ) βΎ ((BaseβπΉ) Γ (BaseβπΉ)))) Γt
(MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ))))) Cn (MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ))))) β ( Β·
:((BaseβπΉ) Γ
(Baseβπ))βΆ(Baseβπ) β§ βπ₯ β (BaseβπΉ)βπ¦ β (Baseβπ)βπ β β+ βπ β β+
βπ§ β
(BaseβπΉ)βπ€ β (Baseβπ)(((π₯((distβπΉ) βΎ ((BaseβπΉ) Γ (BaseβπΉ)))π§) < π β§ (π¦((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π€) < π ) β ((π₯ Β· π¦)((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))(π§ Β· π€)) < π)))) |
66 | 55, 62, 62, 65 | syl3anc 1372 |
. . 3
β’ (π β NrmMod β ( Β· β
(((MetOpenβ((distβπΉ) βΎ ((BaseβπΉ) Γ (BaseβπΉ)))) Γt
(MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ))))) Cn (MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ))))) β ( Β·
:((BaseβπΉ) Γ
(Baseβπ))βΆ(Baseβπ) β§ βπ₯ β (BaseβπΉ)βπ¦ β (Baseβπ)βπ β β+ βπ β β+
βπ§ β
(BaseβπΉ)βπ€ β (Baseβπ)(((π₯((distβπΉ) βΎ ((BaseβπΉ) Γ (BaseβπΉ)))π§) < π β§ (π¦((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π€) < π ) β ((π₯ Β· π¦)((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))(π§ Β· π€)) < π)))) |
67 | 7, 48, 66 | mpbir2and 712 |
. 2
β’ (π β NrmMod β Β· β
(((MetOpenβ((distβπΉ) βΎ ((BaseβπΉ) Γ (BaseβπΉ)))) Γt
(MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ))))) Cn (MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))))) |
68 | | nlmvscn.kf |
. . . . . 6
β’ πΎ = (TopOpenβπΉ) |
69 | 68, 4, 53 | mstopn 23828 |
. . . . 5
β’ (πΉ β MetSp β πΎ =
(MetOpenβ((distβπΉ) βΎ ((BaseβπΉ) Γ (BaseβπΉ))))) |
70 | 51, 69 | syl 17 |
. . . 4
β’ (π β NrmMod β πΎ =
(MetOpenβ((distβπΉ) βΎ ((BaseβπΉ) Γ (BaseβπΉ))))) |
71 | | nlmvscn.j |
. . . . . 6
β’ π½ = (TopOpenβπ) |
72 | 71, 2, 60 | mstopn 23828 |
. . . . 5
β’ (π β MetSp β π½ =
(MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ))))) |
73 | 58, 72 | syl 17 |
. . . 4
β’ (π β NrmMod β π½ =
(MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ))))) |
74 | 70, 73 | oveq12d 7379 |
. . 3
β’ (π β NrmMod β (πΎ Γt π½) =
((MetOpenβ((distβπΉ) βΎ ((BaseβπΉ) Γ (BaseβπΉ)))) Γt
(MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))))) |
75 | 74, 73 | oveq12d 7379 |
. 2
β’ (π β NrmMod β ((πΎ Γt π½) Cn π½) = (((MetOpenβ((distβπΉ) βΎ ((BaseβπΉ) Γ (BaseβπΉ)))) Γt
(MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ))))) Cn (MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))))) |
76 | 67, 75 | eleqtrrd 2837 |
1
β’ (π β NrmMod β Β· β
((πΎ Γt
π½) Cn π½)) |