lssnlm

Description: A subspace of a normed module is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	lssnlm.x	$⊢ X = W ↾_{𝑠} U$
	lssnlm.s	$⊢ S = LSubSp (W)$
Assertion	lssnlm	$⊢ (W \in NrmMod \land U \in S) \to X \in NrmMod$

Proof

Step	Hyp	Ref	Expression
1		lssnlm.x	$⊢ X = W ↾_{𝑠} U$
2		lssnlm.s	$⊢ S = LSubSp (W)$
3		nlmngp	$⊢ W \in NrmMod \to W \in NrmGrp$
4		nlmlmod	$⊢ W \in NrmMod \to W \in LMod$
5	2	lsssubg	$⊢ (W \in LMod \land U \in S) \to U \in SubGrp (W)$
6	4 5	sylan	$⊢ (W \in NrmMod \land U \in S) \to U \in SubGrp (W)$
7	1	subgngp	$⊢ (W \in NrmGrp \land U \in SubGrp (W)) \to X \in NrmGrp$
8	3 6 7	syl2an2r	$⊢ (W \in NrmMod \land U \in S) \to X \in NrmGrp$
9	1 2	lsslmod	$⊢ (W \in LMod \land U \in S) \to X \in LMod$
10	4 9	sylan	$⊢ (W \in NrmMod \land U \in S) \to X \in LMod$
11		eqid	$⊢ Scalar (W) = Scalar (W)$
12	1 11	resssca	$⊢ U \in S \to Scalar (W) = Scalar (X)$
13	12	adantl	$⊢ (W \in NrmMod \land U \in S) \to Scalar (W) = Scalar (X)$
14	11	nlmnrg	$⊢ W \in NrmMod \to Scalar (W) \in NrmRing$
15	14	adantr	$⊢ (W \in NrmMod \land U \in S) \to Scalar (W) \in NrmRing$
16	13 15	eqeltrrd	$⊢ (W \in NrmMod \land U \in S) \to Scalar (X) \in NrmRing$
17	8 10 16	3jca	$⊢ (W \in NrmMod \land U \in S) \to (X \in NrmGrp \land X \in LMod \land Scalar (X) \in NrmRing)$
18		simpll	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to W \in NrmMod$
19		simprl	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to x \in {Base}_{Scalar (X)}$
20	13	adantr	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to Scalar (W) = Scalar (X)$
21	20	fveq2d	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to {Base}_{Scalar (W)} = {Base}_{Scalar (X)}$
22	19 21	eleqtrrd	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to x \in {Base}_{Scalar (W)}$
23	6	adantr	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to U \in SubGrp (W)$
24		eqid	$⊢ {Base}_{W} = {Base}_{W}$
25	24	subgss	$⊢ U \in SubGrp (W) \to U \subseteq {Base}_{W}$
26	23 25	syl	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to U \subseteq {Base}_{W}$
27		simprr	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to y \in {Base}_{X}$
28	1	subgbas	$⊢ U \in SubGrp (W) \to U = {Base}_{X}$
29	23 28	syl	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to U = {Base}_{X}$
30	27 29	eleqtrrd	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to y \in U$
31	26 30	sseldd	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to y \in {Base}_{W}$
32		eqid	$⊢ norm (W) = norm (W)$
33		eqid	$⊢ \cdot_{W} = \cdot_{W}$
34		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
35		eqid	$⊢ norm (Scalar (W)) = norm (Scalar (W))$
36	24 32 33 11 34 35	nmvs	$⊢ (W \in NrmMod \land x \in {Base}_{Scalar (W)} \land y \in {Base}_{W}) \to norm (W) (x \cdot_{W} y) = norm (Scalar (W)) (x) norm (W) (y)$
37	18 22 31 36	syl3anc	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to norm (W) (x \cdot_{W} y) = norm (Scalar (W)) (x) norm (W) (y)$
38		simplr	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to U \in S$
39	1 33	ressvsca	$⊢ U \in S \to \cdot_{W} = \cdot_{X}$
40	38 39	syl	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to \cdot_{W} = \cdot_{X}$
41	40	oveqd	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to x \cdot_{W} y = x \cdot_{X} y$
42	41	fveq2d	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to norm (X) (x \cdot_{W} y) = norm (X) (x \cdot_{X} y)$
43	4	ad2antrr	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to W \in LMod$
44	11 33 34 2	lssvscl	$⊢ ((W \in LMod \land U \in S) \land (x \in {Base}_{Scalar (W)} \land y \in U)) \to x \cdot_{W} y \in U$
45	43 38 22 30 44	syl22anc	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to x \cdot_{W} y \in U$
46		eqid	$⊢ norm (X) = norm (X)$
47	1 32 46	subgnm2	$⊢ (U \in SubGrp (W) \land x \cdot_{W} y \in U) \to norm (X) (x \cdot_{W} y) = norm (W) (x \cdot_{W} y)$
48	6 45 47	syl2an2r	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to norm (X) (x \cdot_{W} y) = norm (W) (x \cdot_{W} y)$
49	42 48	eqtr3d	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to norm (X) (x \cdot_{X} y) = norm (W) (x \cdot_{W} y)$
50	20	eqcomd	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to Scalar (X) = Scalar (W)$
51	50	fveq2d	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to norm (Scalar (X)) = norm (Scalar (W))$
52	51	fveq1d	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to norm (Scalar (X)) (x) = norm (Scalar (W)) (x)$
53	1 32 46	subgnm2	$⊢ (U \in SubGrp (W) \land y \in U) \to norm (X) (y) = norm (W) (y)$
54	6 30 53	syl2an2r	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to norm (X) (y) = norm (W) (y)$
55	52 54	oveq12d	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to norm (Scalar (X)) (x) norm (X) (y) = norm (Scalar (W)) (x) norm (W) (y)$
56	37 49 55	3eqtr4d	$⊢ ((W \in NrmMod \land U \in S) \land (x \in {Base}_{Scalar (X)} \land y \in {Base}_{X})) \to norm (X) (x \cdot_{X} y) = norm (Scalar (X)) (x) norm (X) (y)$
57	56	ralrimivva	$⊢ (W \in NrmMod \land U \in S) \to \forall x \in {Base}_{Scalar (X)} \forall y \in {Base}_{X} norm (X) (x \cdot_{X} y) = norm (Scalar (X)) (x) norm (X) (y)$
58		eqid	$⊢ {Base}_{X} = {Base}_{X}$
59		eqid	$⊢ \cdot_{X} = \cdot_{X}$
60		eqid	$⊢ Scalar (X) = Scalar (X)$
61		eqid	$⊢ {Base}_{Scalar (X)} = {Base}_{Scalar (X)}$
62		eqid	$⊢ norm (Scalar (X)) = norm (Scalar (X))$
63	58 46 59 60 61 62	isnlm	$⊢ X \in NrmMod \leftrightarrow ((X \in NrmGrp \land X \in LMod \land Scalar (X) \in NrmRing) \land \forall x \in {Base}_{Scalar (X)} \forall y \in {Base}_{X} norm (X) (x \cdot_{X} y) = norm (Scalar (X)) (x) norm (X) (y))$
64	17 57 63	sylanbrc	$⊢ (W \in NrmMod \land U \in S) \to X \in NrmMod$

Metamath Proof Explorer

Theorem lssnlm

Proof