isnlm

Description: A normed (left) module is a module which is also a normed group over a normed ring, such that the norm distributes over scalar multiplication. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	isnlm.v	$⊢ V = {Base}_{W}$
	isnlm.n	$⊢ N = norm (W)$
	isnlm.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	isnlm.f	$⊢ F = Scalar (W)$
	isnlm.k	$⊢ K = {Base}_{F}$
	isnlm.a	$⊢ A = norm (F)$
Assertion	isnlm	$⊢ W \in NrmMod \leftrightarrow ((W \in NrmGrp \land W \in LMod \land F \in NrmRing) \land \forall x \in K \forall y \in V N (x \underset{˙}{\cdot} y) = A (x) N (y))$

Proof

Step	Hyp	Ref	Expression
1		isnlm.v	$⊢ V = {Base}_{W}$
2		isnlm.n	$⊢ N = norm (W)$
3		isnlm.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		isnlm.f	$⊢ F = Scalar (W)$
5		isnlm.k	$⊢ K = {Base}_{F}$
6		isnlm.a	$⊢ A = norm (F)$
7		anass	$⊢ ((W \in (NrmGrp \cap LMod) \land F \in NrmRing) \land \forall x \in K \forall y \in V N (x \underset{˙}{\cdot} y) = A (x) N (y)) \leftrightarrow (W \in (NrmGrp \cap LMod) \land (F \in NrmRing \land \forall x \in K \forall y \in V N (x \underset{˙}{\cdot} y) = A (x) N (y)))$
8		df-3an	$⊢ (W \in NrmGrp \land W \in LMod \land F \in NrmRing) \leftrightarrow ((W \in NrmGrp \land W \in LMod) \land F \in NrmRing)$
9		elin	$⊢ W \in (NrmGrp \cap LMod) \leftrightarrow (W \in NrmGrp \land W \in LMod)$
10	9	anbi1i	$⊢ (W \in (NrmGrp \cap LMod) \land F \in NrmRing) \leftrightarrow ((W \in NrmGrp \land W \in LMod) \land F \in NrmRing)$
11	8 10	bitr4i	$⊢ (W \in NrmGrp \land W \in LMod \land F \in NrmRing) \leftrightarrow (W \in (NrmGrp \cap LMod) \land F \in NrmRing)$
12	11	anbi1i	$⊢ ((W \in NrmGrp \land W \in LMod \land F \in NrmRing) \land \forall x \in K \forall y \in V N (x \underset{˙}{\cdot} y) = A (x) N (y)) \leftrightarrow ((W \in (NrmGrp \cap LMod) \land F \in NrmRing) \land \forall x \in K \forall y \in V N (x \underset{˙}{\cdot} y) = A (x) N (y))$
13		fvexd	$⊢ w = W \to Scalar (w) \in V$
14		id	$⊢ f = Scalar (w) \to f = Scalar (w)$
15		fveq2	$⊢ w = W \to Scalar (w) = Scalar (W)$
16	15 4	eqtr4di	$⊢ w = W \to Scalar (w) = F$
17	14 16	sylan9eqr	$⊢ (w = W \land f = Scalar (w)) \to f = F$
18	17	eleq1d	$⊢ (w = W \land f = Scalar (w)) \to (f \in NrmRing \leftrightarrow F \in NrmRing)$
19	17	fveq2d	$⊢ (w = W \land f = Scalar (w)) \to {Base}_{f} = {Base}_{F}$
20	19 5	eqtr4di	$⊢ (w = W \land f = Scalar (w)) \to {Base}_{f} = K$
21		simpl	$⊢ (w = W \land f = Scalar (w)) \to w = W$
22	21	fveq2d	$⊢ (w = W \land f = Scalar (w)) \to {Base}_{w} = {Base}_{W}$
23	22 1	eqtr4di	$⊢ (w = W \land f = Scalar (w)) \to {Base}_{w} = V$
24	21	fveq2d	$⊢ (w = W \land f = Scalar (w)) \to norm (w) = norm (W)$
25	24 2	eqtr4di	$⊢ (w = W \land f = Scalar (w)) \to norm (w) = N$
26	21	fveq2d	$⊢ (w = W \land f = Scalar (w)) \to \cdot_{w} = \cdot_{W}$
27	26 3	eqtr4di	$⊢ (w = W \land f = Scalar (w)) \to \cdot_{w} = \underset{˙}{\cdot}$
28	27	oveqd	$⊢ (w = W \land f = Scalar (w)) \to x \cdot_{w} y = x \underset{˙}{\cdot} y$
29	25 28	fveq12d	$⊢ (w = W \land f = Scalar (w)) \to norm (w) (x \cdot_{w} y) = N (x \underset{˙}{\cdot} y)$
30	17	fveq2d	$⊢ (w = W \land f = Scalar (w)) \to norm (f) = norm (F)$
31	30 6	eqtr4di	$⊢ (w = W \land f = Scalar (w)) \to norm (f) = A$
32	31	fveq1d	$⊢ (w = W \land f = Scalar (w)) \to norm (f) (x) = A (x)$
33	25	fveq1d	$⊢ (w = W \land f = Scalar (w)) \to norm (w) (y) = N (y)$
34	32 33	oveq12d	$⊢ (w = W \land f = Scalar (w)) \to norm (f) (x) norm (w) (y) = A (x) N (y)$
35	29 34	eqeq12d	$⊢ (w = W \land f = Scalar (w)) \to (norm (w) (x \cdot_{w} y) = norm (f) (x) norm (w) (y) \leftrightarrow N (x \underset{˙}{\cdot} y) = A (x) N (y))$
36	23 35	raleqbidv	$⊢ (w = W \land f = Scalar (w)) \to (\forall y \in {Base}_{w} norm (w) (x \cdot_{w} y) = norm (f) (x) norm (w) (y) \leftrightarrow \forall y \in V N (x \underset{˙}{\cdot} y) = A (x) N (y))$
37	20 36	raleqbidv	$⊢ (w = W \land f = Scalar (w)) \to (\forall x \in {Base}_{f} \forall y \in {Base}_{w} norm (w) (x \cdot_{w} y) = norm (f) (x) norm (w) (y) \leftrightarrow \forall x \in K \forall y \in V N (x \underset{˙}{\cdot} y) = A (x) N (y))$
38	18 37	anbi12d	$⊢ (w = W \land f = Scalar (w)) \to ((f \in NrmRing \land \forall x \in {Base}_{f} \forall y \in {Base}_{w} norm (w) (x \cdot_{w} y) = norm (f) (x) norm (w) (y)) \leftrightarrow (F \in NrmRing \land \forall x \in K \forall y \in V N (x \underset{˙}{\cdot} y) = A (x) N (y)))$
39	13 38	sbcied	$⊢ w = W \to (\underset{˙}{[} Scalar (w) / f \underset{˙}{]} (f \in NrmRing \land \forall x \in {Base}_{f} \forall y \in {Base}_{w} norm (w) (x \cdot_{w} y) = norm (f) (x) norm (w) (y)) \leftrightarrow (F \in NrmRing \land \forall x \in K \forall y \in V N (x \underset{˙}{\cdot} y) = A (x) N (y)))$
40		df-nlm	$⊢ NrmMod = \{w \in (NrmGrp \cap LMod) \| \underset{˙}{[} Scalar (w) / f \underset{˙}{]} (f \in NrmRing \land \forall x \in {Base}_{f} \forall y \in {Base}_{w} norm (w) (x \cdot_{w} y) = norm (f) (x) norm (w) (y))\}$
41	39 40	elrab2	$⊢ W \in NrmMod \leftrightarrow (W \in (NrmGrp \cap LMod) \land (F \in NrmRing \land \forall x \in K \forall y \in V N (x \underset{˙}{\cdot} y) = A (x) N (y)))$
42	7 12 41	3bitr4ri	$⊢ W \in NrmMod \leftrightarrow ((W \in NrmGrp \land W \in LMod \land F \in NrmRing) \land \forall x \in K \forall y \in V N (x \underset{˙}{\cdot} y) = A (x) N (y))$

Metamath Proof Explorer

Theorem isnlm

Proof