Step |
Hyp |
Ref |
Expression |
1 |
|
sranlm.a |
|- A = ( ( subringAlg ` W ) ` S ) |
2 |
|
nrgngp |
|- ( W e. NrmRing -> W e. NrmGrp ) |
3 |
2
|
adantr |
|- ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> W e. NrmGrp ) |
4 |
|
eqidd |
|- ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> ( Base ` W ) = ( Base ` W ) ) |
5 |
1
|
a1i |
|- ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> A = ( ( subringAlg ` W ) ` S ) ) |
6 |
|
eqid |
|- ( Base ` W ) = ( Base ` W ) |
7 |
6
|
subrgss |
|- ( S e. ( SubRing ` W ) -> S C_ ( Base ` W ) ) |
8 |
7
|
adantl |
|- ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> S C_ ( Base ` W ) ) |
9 |
5 8
|
srabase |
|- ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> ( Base ` W ) = ( Base ` A ) ) |
10 |
5 8
|
sraaddg |
|- ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> ( +g ` W ) = ( +g ` A ) ) |
11 |
10
|
oveqdr |
|- ( ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( x ( +g ` W ) y ) = ( x ( +g ` A ) y ) ) |
12 |
5 8
|
srads |
|- ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> ( dist ` W ) = ( dist ` A ) ) |
13 |
12
|
reseq1d |
|- ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) = ( ( dist ` A ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) |
14 |
5 8
|
sratopn |
|- ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> ( TopOpen ` W ) = ( TopOpen ` A ) ) |
15 |
4 9 11 13 14
|
ngppropd |
|- ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> ( W e. NrmGrp <-> A e. NrmGrp ) ) |
16 |
3 15
|
mpbid |
|- ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> A e. NrmGrp ) |
17 |
1
|
sralmod |
|- ( S e. ( SubRing ` W ) -> A e. LMod ) |
18 |
17
|
adantl |
|- ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> A e. LMod ) |
19 |
5 8
|
srasca |
|- ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> ( W |`s S ) = ( Scalar ` A ) ) |
20 |
|
eqid |
|- ( W |`s S ) = ( W |`s S ) |
21 |
20
|
subrgnrg |
|- ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> ( W |`s S ) e. NrmRing ) |
22 |
19 21
|
eqeltrrd |
|- ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> ( Scalar ` A ) e. NrmRing ) |
23 |
16 18 22
|
3jca |
|- ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> ( A e. NrmGrp /\ A e. LMod /\ ( Scalar ` A ) e. NrmRing ) ) |
24 |
|
eqid |
|- ( norm ` W ) = ( norm ` W ) |
25 |
|
eqid |
|- ( AbsVal ` W ) = ( AbsVal ` W ) |
26 |
24 25
|
nrgabv |
|- ( W e. NrmRing -> ( norm ` W ) e. ( AbsVal ` W ) ) |
27 |
26
|
ad2antrr |
|- ( ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> ( norm ` W ) e. ( AbsVal ` W ) ) |
28 |
8
|
adantr |
|- ( ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> S C_ ( Base ` W ) ) |
29 |
|
simprl |
|- ( ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> x e. ( Base ` ( Scalar ` A ) ) ) |
30 |
20
|
subrgbas |
|- ( S e. ( SubRing ` W ) -> S = ( Base ` ( W |`s S ) ) ) |
31 |
30
|
adantl |
|- ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> S = ( Base ` ( W |`s S ) ) ) |
32 |
19
|
fveq2d |
|- ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> ( Base ` ( W |`s S ) ) = ( Base ` ( Scalar ` A ) ) ) |
33 |
31 32
|
eqtrd |
|- ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> S = ( Base ` ( Scalar ` A ) ) ) |
34 |
33
|
adantr |
|- ( ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> S = ( Base ` ( Scalar ` A ) ) ) |
35 |
29 34
|
eleqtrrd |
|- ( ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> x e. S ) |
36 |
28 35
|
sseldd |
|- ( ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> x e. ( Base ` W ) ) |
37 |
|
simprr |
|- ( ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> y e. ( Base ` A ) ) |
38 |
9
|
adantr |
|- ( ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> ( Base ` W ) = ( Base ` A ) ) |
39 |
37 38
|
eleqtrrd |
|- ( ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> y e. ( Base ` W ) ) |
40 |
|
eqid |
|- ( .r ` W ) = ( .r ` W ) |
41 |
25 6 40
|
abvmul |
|- ( ( ( norm ` W ) e. ( AbsVal ` W ) /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) -> ( ( norm ` W ) ` ( x ( .r ` W ) y ) ) = ( ( ( norm ` W ) ` x ) x. ( ( norm ` W ) ` y ) ) ) |
42 |
27 36 39 41
|
syl3anc |
|- ( ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> ( ( norm ` W ) ` ( x ( .r ` W ) y ) ) = ( ( ( norm ` W ) ` x ) x. ( ( norm ` W ) ` y ) ) ) |
43 |
9 10 12
|
nmpropd |
|- ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> ( norm ` W ) = ( norm ` A ) ) |
44 |
43
|
adantr |
|- ( ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> ( norm ` W ) = ( norm ` A ) ) |
45 |
5 8
|
sravsca |
|- ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> ( .r ` W ) = ( .s ` A ) ) |
46 |
45
|
oveqdr |
|- ( ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> ( x ( .r ` W ) y ) = ( x ( .s ` A ) y ) ) |
47 |
44 46
|
fveq12d |
|- ( ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> ( ( norm ` W ) ` ( x ( .r ` W ) y ) ) = ( ( norm ` A ) ` ( x ( .s ` A ) y ) ) ) |
48 |
42 47
|
eqtr3d |
|- ( ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> ( ( ( norm ` W ) ` x ) x. ( ( norm ` W ) ` y ) ) = ( ( norm ` A ) ` ( x ( .s ` A ) y ) ) ) |
49 |
|
subrgsubg |
|- ( S e. ( SubRing ` W ) -> S e. ( SubGrp ` W ) ) |
50 |
49
|
ad2antlr |
|- ( ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> S e. ( SubGrp ` W ) ) |
51 |
|
eqid |
|- ( norm ` ( W |`s S ) ) = ( norm ` ( W |`s S ) ) |
52 |
20 24 51
|
subgnm2 |
|- ( ( S e. ( SubGrp ` W ) /\ x e. S ) -> ( ( norm ` ( W |`s S ) ) ` x ) = ( ( norm ` W ) ` x ) ) |
53 |
50 35 52
|
syl2anc |
|- ( ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> ( ( norm ` ( W |`s S ) ) ` x ) = ( ( norm ` W ) ` x ) ) |
54 |
19
|
adantr |
|- ( ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> ( W |`s S ) = ( Scalar ` A ) ) |
55 |
54
|
fveq2d |
|- ( ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> ( norm ` ( W |`s S ) ) = ( norm ` ( Scalar ` A ) ) ) |
56 |
55
|
fveq1d |
|- ( ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> ( ( norm ` ( W |`s S ) ) ` x ) = ( ( norm ` ( Scalar ` A ) ) ` x ) ) |
57 |
53 56
|
eqtr3d |
|- ( ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> ( ( norm ` W ) ` x ) = ( ( norm ` ( Scalar ` A ) ) ` x ) ) |
58 |
44
|
fveq1d |
|- ( ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> ( ( norm ` W ) ` y ) = ( ( norm ` A ) ` y ) ) |
59 |
57 58
|
oveq12d |
|- ( ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> ( ( ( norm ` W ) ` x ) x. ( ( norm ` W ) ` y ) ) = ( ( ( norm ` ( Scalar ` A ) ) ` x ) x. ( ( norm ` A ) ` y ) ) ) |
60 |
48 59
|
eqtr3d |
|- ( ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> ( ( norm ` A ) ` ( x ( .s ` A ) y ) ) = ( ( ( norm ` ( Scalar ` A ) ) ` x ) x. ( ( norm ` A ) ` y ) ) ) |
61 |
60
|
ralrimivva |
|- ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> A. x e. ( Base ` ( Scalar ` A ) ) A. y e. ( Base ` A ) ( ( norm ` A ) ` ( x ( .s ` A ) y ) ) = ( ( ( norm ` ( Scalar ` A ) ) ` x ) x. ( ( norm ` A ) ` y ) ) ) |
62 |
|
eqid |
|- ( Base ` A ) = ( Base ` A ) |
63 |
|
eqid |
|- ( norm ` A ) = ( norm ` A ) |
64 |
|
eqid |
|- ( .s ` A ) = ( .s ` A ) |
65 |
|
eqid |
|- ( Scalar ` A ) = ( Scalar ` A ) |
66 |
|
eqid |
|- ( Base ` ( Scalar ` A ) ) = ( Base ` ( Scalar ` A ) ) |
67 |
|
eqid |
|- ( norm ` ( Scalar ` A ) ) = ( norm ` ( Scalar ` A ) ) |
68 |
62 63 64 65 66 67
|
isnlm |
|- ( A e. NrmMod <-> ( ( A e. NrmGrp /\ A e. LMod /\ ( Scalar ` A ) e. NrmRing ) /\ A. x e. ( Base ` ( Scalar ` A ) ) A. y e. ( Base ` A ) ( ( norm ` A ) ` ( x ( .s ` A ) y ) ) = ( ( ( norm ` ( Scalar ` A ) ) ` x ) x. ( ( norm ` A ) ` y ) ) ) ) |
69 |
23 61 68
|
sylanbrc |
|- ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> A e. NrmMod ) |