Metamath Proof Explorer

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 ) ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐴 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) ) )