Metamath Proof Explorer

Theorem sranlm

Description: The subring algebra over a normed ring is a normed left module. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypothesis sranlm.a 
|- A = ( ( subringAlg ` W ) ` S )
Assertion sranlm 
|- ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> A e. NrmMod )

Proof

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 )