Metamath Proof Explorer

Theorem nlmvscn

Description: The scalar multiplication of a normed module is continuous. Lemma for nrgtrg and nlmtlm . (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses nlmvscn.f 
|- F = ( Scalar ` W )
nlmvscn.sf 
|- .x. = ( .sf ` W )
nlmvscn.j 
|- J = ( TopOpen ` W )
nlmvscn.kf 
|- K = ( TopOpen ` F )
Assertion nlmvscn 
|- ( W e. NrmMod -> .x. e. ( ( K tX J ) Cn J ) )

Proof

Step Hyp Ref Expression
1 nlmvscn.f 
 |-  F = ( Scalar ` W )
2 nlmvscn.sf 
 |-  .x. = ( .sf ` W )
3 nlmvscn.j 
 |-  J = ( TopOpen ` W )
4 nlmvscn.kf 
 |-  K = ( TopOpen ` F )
5 nlmlmod 
 |-  ( W e. NrmMod -> W e. LMod )
6 eqid 
 |-  ( Base ` W ) = ( Base ` W )
7 eqid 
 |-  ( Base ` F ) = ( Base ` F )
8 6 1 7 2 lmodscaf 
 |-  ( W e. LMod -> .x. : ( ( Base ` F ) X. ( Base ` W ) ) --> ( Base ` W ) )
9 5 8 syl 
 |-  ( W e. NrmMod -> .x. : ( ( Base ` F ) X. ( Base ` W ) ) --> ( Base ` W ) )
10 eqid 
 |-  ( dist ` W ) = ( dist ` W )
11 eqid 
 |-  ( dist ` F ) = ( dist ` F )
12 eqid 
 |-  ( norm ` W ) = ( norm ` W )
13 eqid 
 |-  ( norm ` F ) = ( norm ` F )
14 eqid 
 |-  ( .s ` W ) = ( .s ` W )
15 eqid 
 |-  ( ( r / 2 ) / ( ( ( norm ` F ) ` x ) + 1 ) ) = ( ( r / 2 ) / ( ( ( norm ` F ) ` x ) + 1 ) )
16 eqid 
 |-  ( ( r / 2 ) / ( ( ( norm ` W ) ` y ) + ( ( r / 2 ) / ( ( ( norm ` F ) ` x ) + 1 ) ) ) ) = ( ( r / 2 ) / ( ( ( norm ` W ) ` y ) + ( ( r / 2 ) / ( ( ( norm ` F ) ` x ) + 1 ) ) ) )
17 simpll 
 |-  ( ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) /\ r e. RR+ ) -> W e. NrmMod )
18 simpr 
 |-  ( ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) /\ r e. RR+ ) -> r e. RR+ )
19 simplrl 
 |-  ( ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) /\ r e. RR+ ) -> x e. ( Base ` F ) )
20 simplrr 
 |-  ( ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) /\ r e. RR+ ) -> y e. ( Base ` W ) )
21 1 6 7 10 11 12 13 14 15 16 17 18 19 20 nlmvscnlem1 
 |-  ( ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) /\ r e. RR+ ) -> E. s e. RR+ A. z e. ( Base ` F ) A. w e. ( Base ` W ) ( ( ( x ( dist ` F ) z ) < s /\ ( y ( dist ` W ) w ) < s ) -> ( ( x ( .s ` W ) y ) ( dist ` W ) ( z ( .s ` W ) w ) ) < r ) )
22 21 ralrimiva 
 |-  ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) -> A. r e. RR+ E. s e. RR+ A. z e. ( Base ` F ) A. w e. ( Base ` W ) ( ( ( x ( dist ` F ) z ) < s /\ ( y ( dist ` W ) w ) < s ) -> ( ( x ( .s ` W ) y ) ( dist ` W ) ( z ( .s ` W ) w ) ) < r ) )
23 simplrl 
 |-  ( ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` F ) /\ w e. ( Base ` W ) ) ) -> x e. ( Base ` F ) )
24 simprl 
 |-  ( ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` F ) /\ w e. ( Base ` W ) ) ) -> z e. ( Base ` F ) )
25 23 24 ovresd 
 |-  ( ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` F ) /\ w e. ( Base ` W ) ) ) -> ( x ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) ) z ) = ( x ( dist ` F ) z ) )
26 25 breq1d 
 |-  ( ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` F ) /\ w e. ( Base ` W ) ) ) -> ( ( x ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) ) z ) < s <-> ( x ( dist ` F ) z ) < s ) )
27 simplrr 
 |-  ( ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` F ) /\ w e. ( Base ` W ) ) ) -> y e. ( Base ` W ) )
28 simprr 
 |-  ( ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` F ) /\ w e. ( Base ` W ) ) ) -> w e. ( Base ` W ) )
29 27 28 ovresd 
 |-  ( ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` F ) /\ w e. ( Base ` W ) ) ) -> ( y ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) w ) = ( y ( dist ` W ) w ) )
30 29 breq1d 
 |-  ( ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` F ) /\ w e. ( Base ` W ) ) ) -> ( ( y ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) w ) < s <-> ( y ( dist ` W ) w ) < s ) )
31 26 30 anbi12d 
 |-  ( ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` F ) /\ w e. ( Base ` W ) ) ) -> ( ( ( x ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) ) z ) < s /\ ( y ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) w ) < s ) <-> ( ( x ( dist ` F ) z ) < s /\ ( y ( dist ` W ) w ) < s ) ) )
32 6 1 7 2 14 scafval 
 |-  ( ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) -> ( x .x. y ) = ( x ( .s ` W ) y ) )
33 32 ad2antlr 
 |-  ( ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` F ) /\ w e. ( Base ` W ) ) ) -> ( x .x. y ) = ( x ( .s ` W ) y ) )
34 6 1 7 2 14 scafval 
 |-  ( ( z e. ( Base ` F ) /\ w e. ( Base ` W ) ) -> ( z .x. w ) = ( z ( .s ` W ) w ) )
35 34 adantl 
 |-  ( ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` F ) /\ w e. ( Base ` W ) ) ) -> ( z .x. w ) = ( z ( .s ` W ) w ) )
36 33 35 oveq12d 
 |-  ( ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` F ) /\ w e. ( Base ` W ) ) ) -> ( ( x .x. y ) ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ( z .x. w ) ) = ( ( x ( .s ` W ) y ) ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ( z ( .s ` W ) w ) ) )
37 5 ad2antrr 
 |-  ( ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` F ) /\ w e. ( Base ` W ) ) ) -> W e. LMod )
38 6 1 14 7 lmodvscl 
 |-  ( ( W e. LMod /\ x e. ( Base ` F ) /\ y e. ( Base ` W ) ) -> ( x ( .s ` W ) y ) e. ( Base ` W ) )
39 37 23 27 38 syl3anc 
 |-  ( ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` F ) /\ w e. ( Base ` W ) ) ) -> ( x ( .s ` W ) y ) e. ( Base ` W ) )
40 6 1 14 7 lmodvscl 
 |-  ( ( W e. LMod /\ z e. ( Base ` F ) /\ w e. ( Base ` W ) ) -> ( z ( .s ` W ) w ) e. ( Base ` W ) )
41 37 24 28 40 syl3anc 
 |-  ( ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` F ) /\ w e. ( Base ` W ) ) ) -> ( z ( .s ` W ) w ) e. ( Base ` W ) )
42 39 41 ovresd 
 |-  ( ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` F ) /\ w e. ( Base ` W ) ) ) -> ( ( x ( .s ` W ) y ) ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ( z ( .s ` W ) w ) ) = ( ( x ( .s ` W ) y ) ( dist ` W ) ( z ( .s ` W ) w ) ) )
43 36 42 eqtrd 
 |-  ( ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` F ) /\ w e. ( Base ` W ) ) ) -> ( ( x .x. y ) ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ( z .x. w ) ) = ( ( x ( .s ` W ) y ) ( dist ` W ) ( z ( .s ` W ) w ) ) )
44 43 breq1d 
 |-  ( ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` F ) /\ w e. ( Base ` W ) ) ) -> ( ( ( x .x. y ) ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ( z .x. w ) ) < r <-> ( ( x ( .s ` W ) y ) ( dist ` W ) ( z ( .s ` W ) w ) ) < r ) )
45 31 44 imbi12d 
 |-  ( ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` F ) /\ w e. ( Base ` W ) ) ) -> ( ( ( ( x ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) ) z ) < s /\ ( y ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) w ) < s ) -> ( ( x .x. y ) ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ( z .x. w ) ) < r ) <-> ( ( ( x ( dist ` F ) z ) < s /\ ( y ( dist ` W ) w ) < s ) -> ( ( x ( .s ` W ) y ) ( dist ` W ) ( z ( .s ` W ) w ) ) < r ) ) )
46 45 2ralbidva 
 |-  ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) -> ( A. z e. ( Base ` F ) A. w e. ( Base ` W ) ( ( ( x ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) ) z ) < s /\ ( y ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) w ) < s ) -> ( ( x .x. y ) ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ( z .x. w ) ) < r ) <-> A. z e. ( Base ` F ) A. w e. ( Base ` W ) ( ( ( x ( dist ` F ) z ) < s /\ ( y ( dist ` W ) w ) < s ) -> ( ( x ( .s ` W ) y ) ( dist ` W ) ( z ( .s ` W ) w ) ) < r ) ) )
47 46 rexbidv 
 |-  ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) -> ( E. s e. RR+ A. z e. ( Base ` F ) A. w e. ( Base ` W ) ( ( ( x ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) ) z ) < s /\ ( y ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) w ) < s ) -> ( ( x .x. y ) ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ( z .x. w ) ) < r ) <-> E. s e. RR+ A. z e. ( Base ` F ) A. w e. ( Base ` W ) ( ( ( x ( dist ` F ) z ) < s /\ ( y ( dist ` W ) w ) < s ) -> ( ( x ( .s ` W ) y ) ( dist ` W ) ( z ( .s ` W ) w ) ) < r ) ) )
48 47 ralbidv 
 |-  ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) -> ( A. r e. RR+ E. s e. RR+ A. z e. ( Base ` F ) A. w e. ( Base ` W ) ( ( ( x ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) ) z ) < s /\ ( y ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) w ) < s ) -> ( ( x .x. y ) ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ( z .x. w ) ) < r ) <-> A. r e. RR+ E. s e. RR+ A. z e. ( Base ` F ) A. w e. ( Base ` W ) ( ( ( x ( dist ` F ) z ) < s /\ ( y ( dist ` W ) w ) < s ) -> ( ( x ( .s ` W ) y ) ( dist ` W ) ( z ( .s ` W ) w ) ) < r ) ) )
49 22 48 mpbird 
 |-  ( ( W e. NrmMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` W ) ) ) -> A. r e. RR+ E. s e. RR+ A. z e. ( Base ` F ) A. w e. ( Base ` W ) ( ( ( x ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) ) z ) < s /\ ( y ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) w ) < s ) -> ( ( x .x. y ) ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ( z .x. w ) ) < r ) )
50 49 ralrimivva 
 |-  ( W e. NrmMod -> A. x e. ( Base ` F ) A. y e. ( Base ` W ) A. r e. RR+ E. s e. RR+ A. z e. ( Base ` F ) A. w e. ( Base ` W ) ( ( ( x ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) ) z ) < s /\ ( y ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) w ) < s ) -> ( ( x .x. y ) ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ( z .x. w ) ) < r ) )
51 1 nlmngp2 
 |-  ( W e. NrmMod -> F e. NrmGrp )
52 ngpms 
 |-  ( F e. NrmGrp -> F e. MetSp )
53 51 52 syl 
 |-  ( W e. NrmMod -> F e. MetSp )
54 msxms 
 |-  ( F e. MetSp -> F e. *MetSp )
55 eqid 
 |-  ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) ) = ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) )
56 7 55 xmsxmet 
 |-  ( F e. *MetSp -> ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) ) e. ( *Met ` ( Base ` F ) ) )
57 53 54 56 3syl 
 |-  ( W e. NrmMod -> ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) ) e. ( *Met ` ( Base ` F ) ) )
58 nlmngp 
 |-  ( W e. NrmMod -> W e. NrmGrp )
59 ngpms 
 |-  ( W e. NrmGrp -> W e. MetSp )
60 58 59 syl 
 |-  ( W e. NrmMod -> W e. MetSp )
61 msxms 
 |-  ( W e. MetSp -> W e. *MetSp )
62 eqid 
 |-  ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) = ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) )
63 6 62 xmsxmet 
 |-  ( W e. *MetSp -> ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) e. ( *Met ` ( Base ` W ) ) )
64 60 61 63 3syl 
 |-  ( W e. NrmMod -> ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) e. ( *Met ` ( Base ` W ) ) )
65 eqid 
 |-  ( MetOpen ` ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) ) ) = ( MetOpen ` ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) ) )
66 eqid 
 |-  ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) = ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) )
67 65 66 66 txmetcn 
 |-  ( ( ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) ) e. ( *Met ` ( Base ` F ) ) /\ ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) e. ( *Met ` ( Base ` W ) ) /\ ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) e. ( *Met ` ( Base ` W ) ) ) -> ( .x. e. ( ( ( MetOpen ` ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) ) ) tX ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) ) Cn ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) ) <-> ( .x. : ( ( Base ` F ) X. ( Base ` W ) ) --> ( Base ` W ) /\ A. x e. ( Base ` F ) A. y e. ( Base ` W ) A. r e. RR+ E. s e. RR+ A. z e. ( Base ` F ) A. w e. ( Base ` W ) ( ( ( x ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) ) z ) < s /\ ( y ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) w ) < s ) -> ( ( x .x. y ) ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ( z .x. w ) ) < r ) ) ) )
68 57 64 64 67 syl3anc 
 |-  ( W e. NrmMod -> ( .x. e. ( ( ( MetOpen ` ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) ) ) tX ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) ) Cn ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) ) <-> ( .x. : ( ( Base ` F ) X. ( Base ` W ) ) --> ( Base ` W ) /\ A. x e. ( Base ` F ) A. y e. ( Base ` W ) A. r e. RR+ E. s e. RR+ A. z e. ( Base ` F ) A. w e. ( Base ` W ) ( ( ( x ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) ) z ) < s /\ ( y ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) w ) < s ) -> ( ( x .x. y ) ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ( z .x. w ) ) < r ) ) ) )
69 9 50 68 mpbir2and 
 |-  ( W e. NrmMod -> .x. e. ( ( ( MetOpen ` ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) ) ) tX ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) ) Cn ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) ) )
70 4 7 55 mstopn 
 |-  ( F e. MetSp -> K = ( MetOpen ` ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) ) ) )
71 53 70 syl 
 |-  ( W e. NrmMod -> K = ( MetOpen ` ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) ) ) )
72 3 6 62 mstopn 
 |-  ( W e. MetSp -> J = ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) )
73 60 72 syl 
 |-  ( W e. NrmMod -> J = ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) )
74 71 73 oveq12d 
 |-  ( W e. NrmMod -> ( K tX J ) = ( ( MetOpen ` ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) ) ) tX ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) ) )
75 74 73 oveq12d 
 |-  ( W e. NrmMod -> ( ( K tX J ) Cn J ) = ( ( ( MetOpen ` ( ( dist ` F ) |` ( ( Base ` F ) X. ( Base ` F ) ) ) ) tX ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) ) Cn ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) ) )
76 69 75 eleqtrrd 
 |-  ( W e. NrmMod -> .x. e. ( ( K tX J ) Cn J ) )