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 \in NrmRing \land S \in SubRing (W)) \to A \in NrmMod$

Proof

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

Metamath Proof Explorer

Theorem sranlm

Proof