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 NrmRing S SubRing W A NrmMod

Proof

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