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 ⊢ 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 )
Assertion sranlm ( ( 𝑊 ∈ NrmRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → 𝐴 ∈ NrmMod )

Proof

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