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 · ( 𝑉 × { 𝑅 } ) ) ∈ 𝐹 )