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 )