Theorem 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	⊢ 𝑉 = ( Base ‘ 𝑊 )
	isnlm.n	⊢ 𝑁 = ( norm ‘ 𝑊 )
	isnlm.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	isnlm.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	isnlm.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	isnlm.a	⊢ 𝐴 = ( norm ‘ 𝐹 )
Assertion	isnlm	⊢ ( 𝑊 ∈ NrmMod ↔ ( ( 𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing ) ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐴 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isnlm.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		isnlm.n	⊢ 𝑁 = ( norm ‘ 𝑊 )
3		isnlm.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
4		isnlm.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
5		isnlm.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
6		isnlm.a	⊢ 𝐴 = ( norm ‘ 𝐹 )
7		anass	⊢ ( ( ( 𝑊 ∈ ( NrmGrp ∩ LMod ) ∧ 𝐹 ∈ NrmRing ) ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐴 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) ) ↔ ( 𝑊 ∈ ( NrmGrp ∩ LMod ) ∧ ( 𝐹 ∈ NrmRing ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐴 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) ) ) )
8		df-3an	⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing ) ↔ ( ( 𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ) ∧ 𝐹 ∈ NrmRing ) )
9		elin	⊢ ( 𝑊 ∈ ( NrmGrp ∩ LMod ) ↔ ( 𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ) )
10	9	anbi1i	⊢ ( ( 𝑊 ∈ ( NrmGrp ∩ LMod ) ∧ 𝐹 ∈ NrmRing ) ↔ ( ( 𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ) ∧ 𝐹 ∈ NrmRing ) )
11	8 10	bitr4i	⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing ) ↔ ( 𝑊 ∈ ( NrmGrp ∩ LMod ) ∧ 𝐹 ∈ NrmRing ) )
12	11	anbi1i	⊢ ( ( ( 𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing ) ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐴 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) ) ↔ ( ( 𝑊 ∈ ( NrmGrp ∩ LMod ) ∧ 𝐹 ∈ NrmRing ) ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐴 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) ) )
13		fvexd	⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) ∈ V )
14		id	⊢ ( 𝑓 = ( Scalar ‘ 𝑤 ) → 𝑓 = ( Scalar ‘ 𝑤 ) )
15		fveq2	⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = ( Scalar ‘ 𝑊 ) )
16	15 4	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = 𝐹 )
17	14 16	sylan9eqr	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → 𝑓 = 𝐹 )
18	17	eleq1d	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( 𝑓 ∈ NrmRing ↔ 𝐹 ∈ NrmRing ) )
19	17	fveq2d	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( Base ‘ 𝑓 ) = ( Base ‘ 𝐹 ) )
20	19 5	eqtr4di	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( Base ‘ 𝑓 ) = 𝐾 )
21		simpl	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → 𝑤 = 𝑊 )
22	21	fveq2d	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
23	22 1	eqtr4di	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( Base ‘ 𝑤 ) = 𝑉 )
24	21	fveq2d	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( norm ‘ 𝑤 ) = ( norm ‘ 𝑊 ) )
25	24 2	eqtr4di	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( norm ‘ 𝑤 ) = 𝑁 )
26	21	fveq2d	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( ·𝑠 ‘ 𝑤 ) = ( ·𝑠 ‘ 𝑊 ) )
27	26 3	eqtr4di	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( ·𝑠 ‘ 𝑤 ) = · )
28	27	oveqd	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) = ( 𝑥 · 𝑦 ) )
29	25 28	fveq12d	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( ( norm ‘ 𝑤 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) = ( 𝑁 ‘ ( 𝑥 · 𝑦 ) ) )
30	17	fveq2d	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( norm ‘ 𝑓 ) = ( norm ‘ 𝐹 ) )
31	30 6	eqtr4di	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( norm ‘ 𝑓 ) = 𝐴 )
32	31	fveq1d	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( ( norm ‘ 𝑓 ) ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
33	25	fveq1d	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( ( norm ‘ 𝑤 ) ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) )
34	32 33	oveq12d	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( ( ( norm ‘ 𝑓 ) ‘ 𝑥 ) · ( ( norm ‘ 𝑤 ) ‘ 𝑦 ) ) = ( ( 𝐴 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) )
35	29 34	eqeq12d	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( ( ( norm ‘ 𝑤 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) = ( ( ( norm ‘ 𝑓 ) ‘ 𝑥 ) · ( ( norm ‘ 𝑤 ) ‘ 𝑦 ) ) ↔ ( 𝑁 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐴 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) ) )
36	23 35	raleqbidv	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( norm ‘ 𝑤 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) = ( ( ( norm ‘ 𝑓 ) ‘ 𝑥 ) · ( ( norm ‘ 𝑤 ) ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐴 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) ) )
37	20 36	raleqbidv	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑓 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( norm ‘ 𝑤 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) = ( ( ( norm ‘ 𝑓 ) ‘ 𝑥 ) · ( ( norm ‘ 𝑤 ) ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐴 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) ) )
38	18 37	anbi12d	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( ( 𝑓 ∈ NrmRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑓 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( norm ‘ 𝑤 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) = ( ( ( norm ‘ 𝑓 ) ‘ 𝑥 ) · ( ( norm ‘ 𝑤 ) ‘ 𝑦 ) ) ) ↔ ( 𝐹 ∈ NrmRing ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐴 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) ) ) )
39	13 38	sbcied	⊢ ( 𝑤 = 𝑊 → ( [ ( Scalar ‘ 𝑤 ) / 𝑓 ] ( 𝑓 ∈ NrmRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑓 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( norm ‘ 𝑤 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) = ( ( ( norm ‘ 𝑓 ) ‘ 𝑥 ) · ( ( norm ‘ 𝑤 ) ‘ 𝑦 ) ) ) ↔ ( 𝐹 ∈ NrmRing ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐴 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) ) ) )
40		df-nlm	⊢ NrmMod = { 𝑤 ∈ ( NrmGrp ∩ LMod ) ∣ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] ( 𝑓 ∈ NrmRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑓 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( norm ‘ 𝑤 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) = ( ( ( norm ‘ 𝑓 ) ‘ 𝑥 ) · ( ( norm ‘ 𝑤 ) ‘ 𝑦 ) ) ) }
41	39 40	elrab2	⊢ ( 𝑊 ∈ NrmMod ↔ ( 𝑊 ∈ ( NrmGrp ∩ LMod ) ∧ ( 𝐹 ∈ NrmRing ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐴 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) ) ) )
42	7 12 41	3bitr4ri	⊢ ( 𝑊 ∈ NrmMod ↔ ( ( 𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing ) ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐴 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) ) )