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 )