Metamath Proof Explorer


Theorem lflnegcl

Description: Closure of the negative of a functional. (This is specialized for the purpose of proving ldualgrp , and we do not define a general operation here.) (Contributed by NM, 22-Oct-2014)

Ref Expression
Hypotheses lflnegcl.v 𝑉 = ( Base ‘ 𝑊 )
lflnegcl.r 𝑅 = ( Scalar ‘ 𝑊 )
lflnegcl.i 𝐼 = ( invg𝑅 )
lflnegcl.n 𝑁 = ( 𝑥𝑉 ↦ ( 𝐼 ‘ ( 𝐺𝑥 ) ) )
lflnegcl.f 𝐹 = ( LFnl ‘ 𝑊 )
lflnegcl.w ( 𝜑𝑊 ∈ LMod )
lflnegcl.g ( 𝜑𝐺𝐹 )
Assertion lflnegcl ( 𝜑𝑁𝐹 )

Proof

Step Hyp Ref Expression
1 lflnegcl.v 𝑉 = ( Base ‘ 𝑊 )
2 lflnegcl.r 𝑅 = ( Scalar ‘ 𝑊 )
3 lflnegcl.i 𝐼 = ( invg𝑅 )
4 lflnegcl.n 𝑁 = ( 𝑥𝑉 ↦ ( 𝐼 ‘ ( 𝐺𝑥 ) ) )
5 lflnegcl.f 𝐹 = ( LFnl ‘ 𝑊 )
6 lflnegcl.w ( 𝜑𝑊 ∈ LMod )
7 lflnegcl.g ( 𝜑𝐺𝐹 )
8 2 lmodring ( 𝑊 ∈ LMod → 𝑅 ∈ Ring )
9 6 8 syl ( 𝜑𝑅 ∈ Ring )
10 ringgrp ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
11 9 10 syl ( 𝜑𝑅 ∈ Grp )
12 11 adantr ( ( 𝜑𝑥𝑉 ) → 𝑅 ∈ Grp )
13 6 adantr ( ( 𝜑𝑥𝑉 ) → 𝑊 ∈ LMod )
14 7 adantr ( ( 𝜑𝑥𝑉 ) → 𝐺𝐹 )
15 simpr ( ( 𝜑𝑥𝑉 ) → 𝑥𝑉 )
16 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
17 2 16 1 5 lflcl ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹𝑥𝑉 ) → ( 𝐺𝑥 ) ∈ ( Base ‘ 𝑅 ) )
18 13 14 15 17 syl3anc ( ( 𝜑𝑥𝑉 ) → ( 𝐺𝑥 ) ∈ ( Base ‘ 𝑅 ) )
19 16 3 grpinvcl ( ( 𝑅 ∈ Grp ∧ ( 𝐺𝑥 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝐼 ‘ ( 𝐺𝑥 ) ) ∈ ( Base ‘ 𝑅 ) )
20 12 18 19 syl2anc ( ( 𝜑𝑥𝑉 ) → ( 𝐼 ‘ ( 𝐺𝑥 ) ) ∈ ( Base ‘ 𝑅 ) )
21 20 4 fmptd ( 𝜑𝑁 : 𝑉 ⟶ ( Base ‘ 𝑅 ) )
22 ringabl ( 𝑅 ∈ Ring → 𝑅 ∈ Abel )
23 9 22 syl ( 𝜑𝑅 ∈ Abel )
24 23 adantr ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → 𝑅 ∈ Abel )
25 9 adantr ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → 𝑅 ∈ Ring )
26 simpr1 ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → 𝑘 ∈ ( Base ‘ 𝑅 ) )
27 6 adantr ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → 𝑊 ∈ LMod )
28 7 adantr ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → 𝐺𝐹 )
29 simpr2 ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → 𝑦𝑉 )
30 2 16 1 5 lflcl ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹𝑦𝑉 ) → ( 𝐺𝑦 ) ∈ ( Base ‘ 𝑅 ) )
31 27 28 29 30 syl3anc ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → ( 𝐺𝑦 ) ∈ ( Base ‘ 𝑅 ) )
32 eqid ( .r𝑅 ) = ( .r𝑅 )
33 16 32 ringcl ( ( 𝑅 ∈ Ring ∧ 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐺𝑦 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑘 ( .r𝑅 ) ( 𝐺𝑦 ) ) ∈ ( Base ‘ 𝑅 ) )
34 25 26 31 33 syl3anc ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → ( 𝑘 ( .r𝑅 ) ( 𝐺𝑦 ) ) ∈ ( Base ‘ 𝑅 ) )
35 simpr3 ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → 𝑧𝑉 )
36 2 16 1 5 lflcl ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹𝑧𝑉 ) → ( 𝐺𝑧 ) ∈ ( Base ‘ 𝑅 ) )
37 27 28 35 36 syl3anc ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → ( 𝐺𝑧 ) ∈ ( Base ‘ 𝑅 ) )
38 eqid ( +g𝑅 ) = ( +g𝑅 )
39 16 38 3 ablinvadd ( ( 𝑅 ∈ Abel ∧ ( 𝑘 ( .r𝑅 ) ( 𝐺𝑦 ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐺𝑧 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝐼 ‘ ( ( 𝑘 ( .r𝑅 ) ( 𝐺𝑦 ) ) ( +g𝑅 ) ( 𝐺𝑧 ) ) ) = ( ( 𝐼 ‘ ( 𝑘 ( .r𝑅 ) ( 𝐺𝑦 ) ) ) ( +g𝑅 ) ( 𝐼 ‘ ( 𝐺𝑧 ) ) ) )
40 24 34 37 39 syl3anc ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → ( 𝐼 ‘ ( ( 𝑘 ( .r𝑅 ) ( 𝐺𝑦 ) ) ( +g𝑅 ) ( 𝐺𝑧 ) ) ) = ( ( 𝐼 ‘ ( 𝑘 ( .r𝑅 ) ( 𝐺𝑦 ) ) ) ( +g𝑅 ) ( 𝐼 ‘ ( 𝐺𝑧 ) ) ) )
41 eqid ( +g𝑊 ) = ( +g𝑊 )
42 eqid ( ·𝑠𝑊 ) = ( ·𝑠𝑊 )
43 1 41 2 42 16 38 32 5 lfli ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → ( 𝐺 ‘ ( ( 𝑘 ( ·𝑠𝑊 ) 𝑦 ) ( +g𝑊 ) 𝑧 ) ) = ( ( 𝑘 ( .r𝑅 ) ( 𝐺𝑦 ) ) ( +g𝑅 ) ( 𝐺𝑧 ) ) )
44 27 28 26 29 35 43 syl113anc ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → ( 𝐺 ‘ ( ( 𝑘 ( ·𝑠𝑊 ) 𝑦 ) ( +g𝑊 ) 𝑧 ) ) = ( ( 𝑘 ( .r𝑅 ) ( 𝐺𝑦 ) ) ( +g𝑅 ) ( 𝐺𝑧 ) ) )
45 44 fveq2d ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → ( 𝐼 ‘ ( 𝐺 ‘ ( ( 𝑘 ( ·𝑠𝑊 ) 𝑦 ) ( +g𝑊 ) 𝑧 ) ) ) = ( 𝐼 ‘ ( ( 𝑘 ( .r𝑅 ) ( 𝐺𝑦 ) ) ( +g𝑅 ) ( 𝐺𝑧 ) ) ) )
46 16 32 3 25 26 31 ringmneg2 ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → ( 𝑘 ( .r𝑅 ) ( 𝐼 ‘ ( 𝐺𝑦 ) ) ) = ( 𝐼 ‘ ( 𝑘 ( .r𝑅 ) ( 𝐺𝑦 ) ) ) )
47 46 oveq1d ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → ( ( 𝑘 ( .r𝑅 ) ( 𝐼 ‘ ( 𝐺𝑦 ) ) ) ( +g𝑅 ) ( 𝐼 ‘ ( 𝐺𝑧 ) ) ) = ( ( 𝐼 ‘ ( 𝑘 ( .r𝑅 ) ( 𝐺𝑦 ) ) ) ( +g𝑅 ) ( 𝐼 ‘ ( 𝐺𝑧 ) ) ) )
48 40 45 47 3eqtr4d ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → ( 𝐼 ‘ ( 𝐺 ‘ ( ( 𝑘 ( ·𝑠𝑊 ) 𝑦 ) ( +g𝑊 ) 𝑧 ) ) ) = ( ( 𝑘 ( .r𝑅 ) ( 𝐼 ‘ ( 𝐺𝑦 ) ) ) ( +g𝑅 ) ( 𝐼 ‘ ( 𝐺𝑧 ) ) ) )
49 1 2 42 16 lmodvscl ( ( 𝑊 ∈ LMod ∧ 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉 ) → ( 𝑘 ( ·𝑠𝑊 ) 𝑦 ) ∈ 𝑉 )
50 27 26 29 49 syl3anc ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → ( 𝑘 ( ·𝑠𝑊 ) 𝑦 ) ∈ 𝑉 )
51 1 41 lmodvacl ( ( 𝑊 ∈ LMod ∧ ( 𝑘 ( ·𝑠𝑊 ) 𝑦 ) ∈ 𝑉𝑧𝑉 ) → ( ( 𝑘 ( ·𝑠𝑊 ) 𝑦 ) ( +g𝑊 ) 𝑧 ) ∈ 𝑉 )
52 27 50 35 51 syl3anc ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → ( ( 𝑘 ( ·𝑠𝑊 ) 𝑦 ) ( +g𝑊 ) 𝑧 ) ∈ 𝑉 )
53 2fveq3 ( 𝑥 = ( ( 𝑘 ( ·𝑠𝑊 ) 𝑦 ) ( +g𝑊 ) 𝑧 ) → ( 𝐼 ‘ ( 𝐺𝑥 ) ) = ( 𝐼 ‘ ( 𝐺 ‘ ( ( 𝑘 ( ·𝑠𝑊 ) 𝑦 ) ( +g𝑊 ) 𝑧 ) ) ) )
54 fvex ( 𝐼 ‘ ( 𝐺 ‘ ( ( 𝑘 ( ·𝑠𝑊 ) 𝑦 ) ( +g𝑊 ) 𝑧 ) ) ) ∈ V
55 53 4 54 fvmpt ( ( ( 𝑘 ( ·𝑠𝑊 ) 𝑦 ) ( +g𝑊 ) 𝑧 ) ∈ 𝑉 → ( 𝑁 ‘ ( ( 𝑘 ( ·𝑠𝑊 ) 𝑦 ) ( +g𝑊 ) 𝑧 ) ) = ( 𝐼 ‘ ( 𝐺 ‘ ( ( 𝑘 ( ·𝑠𝑊 ) 𝑦 ) ( +g𝑊 ) 𝑧 ) ) ) )
56 52 55 syl ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → ( 𝑁 ‘ ( ( 𝑘 ( ·𝑠𝑊 ) 𝑦 ) ( +g𝑊 ) 𝑧 ) ) = ( 𝐼 ‘ ( 𝐺 ‘ ( ( 𝑘 ( ·𝑠𝑊 ) 𝑦 ) ( +g𝑊 ) 𝑧 ) ) ) )
57 2fveq3 ( 𝑥 = 𝑦 → ( 𝐼 ‘ ( 𝐺𝑥 ) ) = ( 𝐼 ‘ ( 𝐺𝑦 ) ) )
58 fvex ( 𝐼 ‘ ( 𝐺𝑦 ) ) ∈ V
59 57 4 58 fvmpt ( 𝑦𝑉 → ( 𝑁𝑦 ) = ( 𝐼 ‘ ( 𝐺𝑦 ) ) )
60 29 59 syl ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → ( 𝑁𝑦 ) = ( 𝐼 ‘ ( 𝐺𝑦 ) ) )
61 60 oveq2d ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → ( 𝑘 ( .r𝑅 ) ( 𝑁𝑦 ) ) = ( 𝑘 ( .r𝑅 ) ( 𝐼 ‘ ( 𝐺𝑦 ) ) ) )
62 2fveq3 ( 𝑥 = 𝑧 → ( 𝐼 ‘ ( 𝐺𝑥 ) ) = ( 𝐼 ‘ ( 𝐺𝑧 ) ) )
63 fvex ( 𝐼 ‘ ( 𝐺𝑧 ) ) ∈ V
64 62 4 63 fvmpt ( 𝑧𝑉 → ( 𝑁𝑧 ) = ( 𝐼 ‘ ( 𝐺𝑧 ) ) )
65 35 64 syl ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → ( 𝑁𝑧 ) = ( 𝐼 ‘ ( 𝐺𝑧 ) ) )
66 61 65 oveq12d ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → ( ( 𝑘 ( .r𝑅 ) ( 𝑁𝑦 ) ) ( +g𝑅 ) ( 𝑁𝑧 ) ) = ( ( 𝑘 ( .r𝑅 ) ( 𝐼 ‘ ( 𝐺𝑦 ) ) ) ( +g𝑅 ) ( 𝐼 ‘ ( 𝐺𝑧 ) ) ) )
67 48 56 66 3eqtr4d ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦𝑉𝑧𝑉 ) ) → ( 𝑁 ‘ ( ( 𝑘 ( ·𝑠𝑊 ) 𝑦 ) ( +g𝑊 ) 𝑧 ) ) = ( ( 𝑘 ( .r𝑅 ) ( 𝑁𝑦 ) ) ( +g𝑅 ) ( 𝑁𝑧 ) ) )
68 67 ralrimivvva ( 𝜑 → ∀ 𝑘 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦𝑉𝑧𝑉 ( 𝑁 ‘ ( ( 𝑘 ( ·𝑠𝑊 ) 𝑦 ) ( +g𝑊 ) 𝑧 ) ) = ( ( 𝑘 ( .r𝑅 ) ( 𝑁𝑦 ) ) ( +g𝑅 ) ( 𝑁𝑧 ) ) )
69 1 41 2 42 16 38 32 5 islfl ( 𝑊 ∈ LMod → ( 𝑁𝐹 ↔ ( 𝑁 : 𝑉 ⟶ ( Base ‘ 𝑅 ) ∧ ∀ 𝑘 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦𝑉𝑧𝑉 ( 𝑁 ‘ ( ( 𝑘 ( ·𝑠𝑊 ) 𝑦 ) ( +g𝑊 ) 𝑧 ) ) = ( ( 𝑘 ( .r𝑅 ) ( 𝑁𝑦 ) ) ( +g𝑅 ) ( 𝑁𝑧 ) ) ) ) )
70 6 69 syl ( 𝜑 → ( 𝑁𝐹 ↔ ( 𝑁 : 𝑉 ⟶ ( Base ‘ 𝑅 ) ∧ ∀ 𝑘 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦𝑉𝑧𝑉 ( 𝑁 ‘ ( ( 𝑘 ( ·𝑠𝑊 ) 𝑦 ) ( +g𝑊 ) 𝑧 ) ) = ( ( 𝑘 ( .r𝑅 ) ( 𝑁𝑦 ) ) ( +g𝑅 ) ( 𝑁𝑧 ) ) ) ) )
71 21 68 70 mpbir2and ( 𝜑𝑁𝐹 )