Metamath Proof Explorer

Theorem lflvscl

Description: Closure of a scalar product with a functional. Note that this is the scalar product for a right vector space with the scalar after the vector; reversing these fails closure. (Contributed by NM, 9-Oct-2014) (Revised by Mario Carneiro, 22-Apr-2015)

Ref Expression
Hypotheses lflsccl.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lflsccl.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
lflsccl.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
lflsccl.t ⊢ · = ( .r ‘ 𝐷 )
lflsccl.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
lflsccl.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lflsccl.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
lflsccl.r ⊢ ( 𝜑 → 𝑅 ∈ 𝐾 )
Assertion lflvscl ( 𝜑 → ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ∈ 𝐹 )

Proof

Step Hyp Ref Expression
1 lflsccl.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lflsccl.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
3 lflsccl.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
4 lflsccl.t ⊢ · = ( .r ‘ 𝐷 )
5 lflsccl.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
6 lflsccl.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
7 lflsccl.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
8 lflsccl.r ⊢ ( 𝜑 → 𝑅 ∈ 𝐾 )
9 1 a1i ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑊 ) )
10 eqidd ⊢ ( 𝜑 → ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 ) )
11 2 a1i ⊢ ( 𝜑 → 𝐷 = ( Scalar ‘ 𝑊 ) )
12 eqidd ⊢ ( 𝜑 → ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 ) )
13 3 a1i ⊢ ( 𝜑 → 𝐾 = ( Base ‘ 𝐷 ) )
14 eqidd ⊢ ( 𝜑 → ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 ) )
15 4 a1i ⊢ ( 𝜑 → · = ( .r ‘ 𝐷 ) )
16 5 a1i ⊢ ( 𝜑 → 𝐹 = ( LFnl ‘ 𝑊 ) )
17 2 lmodring ⊢ ( 𝑊 ∈ LMod → 𝐷 ∈ Ring )
18 6 17 syl ⊢ ( 𝜑 → 𝐷 ∈ Ring )
19 3 4 ringcl ⊢ ( ( 𝐷 ∈ Ring ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) → ( 𝑥 · 𝑦 ) ∈ 𝐾 )
20 19 3expb ⊢ ( ( 𝐷 ∈ Ring ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝐾 )
21 18 20 sylan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝐾 )
22 2 3 1 5 lflf ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ 𝐾 )
23 6 7 22 syl2anc ⊢ ( 𝜑 → 𝐺 : 𝑉 ⟶ 𝐾 )
24 fconst6g ⊢ ( 𝑅 ∈ 𝐾 → ( 𝑉 × { 𝑅 } ) : 𝑉 ⟶ 𝐾 )
25 8 24 syl ⊢ ( 𝜑 → ( 𝑉 × { 𝑅 } ) : 𝑉 ⟶ 𝐾 )
26 1 fvexi ⊢ 𝑉 ∈ V
27 26 a1i ⊢ ( 𝜑 → 𝑉 ∈ V )
28 inidm ⊢ ( 𝑉 ∩ 𝑉 ) = 𝑉
29 21 23 25 27 27 28 off ⊢ ( 𝜑 → ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) : 𝑉 ⟶ 𝐾 )
30 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑊 ∈ LMod )
31 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝐺 ∈ 𝐹 )
32 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑟 ∈ 𝐾 )
33 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑥 ∈ 𝑉 )
34 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑦 ∈ 𝑉 )
35 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
36 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
37 eqid ⊢ ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 )
38 1 35 2 36 3 37 4 5 lfli ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑦 ) ) )
39 30 31 32 33 34 38 syl113anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑦 ) ) )
40 39 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) · 𝑅 ) = ( ( ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑦 ) ) · 𝑅 ) )
41 18 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝐷 ∈ Ring )
42 2 3 1 5 lflcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝐾 )
43 30 31 33 42 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝐾 )
44 3 4 ringcl ⊢ ( ( 𝐷 ∈ Ring ∧ 𝑟 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑥 ) ∈ 𝐾 ) → ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐾 )
45 41 32 43 44 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐾 )
46 2 3 1 5 lflcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑦 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐾 )
47 30 31 34 46 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐾 )
48 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑅 ∈ 𝐾 )
49 3 37 4 ringdir ⊢ ( ( 𝐷 ∈ Ring ∧ ( ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑦 ) ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ) ) → ( ( ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑦 ) ) · 𝑅 ) = ( ( ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) · 𝑅 ) ( +g ‘ 𝐷 ) ( ( 𝐺 ‘ 𝑦 ) · 𝑅 ) ) )
50 41 45 47 48 49 syl13anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑦 ) ) · 𝑅 ) = ( ( ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) · 𝑅 ) ( +g ‘ 𝐷 ) ( ( 𝐺 ‘ 𝑦 ) · 𝑅 ) ) )
51 3 4 ringass ⊢ ( ( 𝐷 ∈ Ring ∧ ( 𝑟 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑥 ) ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ) ) → ( ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) · 𝑅 ) = ( 𝑟 · ( ( 𝐺 ‘ 𝑥 ) · 𝑅 ) ) )
52 41 32 43 48 51 syl13anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) · 𝑅 ) = ( 𝑟 · ( ( 𝐺 ‘ 𝑥 ) · 𝑅 ) ) )
53 52 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) · 𝑅 ) ( +g ‘ 𝐷 ) ( ( 𝐺 ‘ 𝑦 ) · 𝑅 ) ) = ( ( 𝑟 · ( ( 𝐺 ‘ 𝑥 ) · 𝑅 ) ) ( +g ‘ 𝐷 ) ( ( 𝐺 ‘ 𝑦 ) · 𝑅 ) ) )
54 40 50 53 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) · 𝑅 ) = ( ( 𝑟 · ( ( 𝐺 ‘ 𝑥 ) · 𝑅 ) ) ( +g ‘ 𝐷 ) ( ( 𝐺 ‘ 𝑦 ) · 𝑅 ) ) )
55 1 2 36 3 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ) → ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ 𝑉 )
56 30 32 33 55 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ 𝑉 )
57 1 35 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ∈ 𝑉 )
58 30 56 34 57 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ∈ 𝑉 )
59 23 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝑉 )
60 eqidd ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ∈ 𝑉 ) → ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) )
61 27 8 59 60 ofc2 ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ∈ 𝑉 ) → ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) · 𝑅 ) )
62 58 61 syldan ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) · 𝑅 ) )
63 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
64 27 8 59 63 ofc2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) · 𝑅 ) )
65 33 64 syldan ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) · 𝑅 ) )
66 65 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑟 · ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑥 ) ) = ( 𝑟 · ( ( 𝐺 ‘ 𝑥 ) · 𝑅 ) ) )
67 eqidd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) )
68 27 8 59 67 ofc2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ 𝑦 ) · 𝑅 ) )
69 34 68 syldan ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ 𝑦 ) · 𝑅 ) )
70 66 69 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝑟 · ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑥 ) ) ( +g ‘ 𝐷 ) ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑦 ) ) = ( ( 𝑟 · ( ( 𝐺 ‘ 𝑥 ) · 𝑅 ) ) ( +g ‘ 𝐷 ) ( ( 𝐺 ‘ 𝑦 ) · 𝑅 ) ) )
71 54 62 70 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝑟 · ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑥 ) ) ( +g ‘ 𝐷 ) ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑦 ) ) )
72 9 10 11 12 13 14 15 16 29 71 6 islfld ⊢ ( 𝜑 → ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ∈ 𝐹 )