# Metamath Proof Explorer

## Theorem lflnegl

Description: A functional plus its negative is the zero 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 ${⊢}{V}={\mathrm{Base}}_{{W}}$
lflnegcl.r ${⊢}{R}=\mathrm{Scalar}\left({W}\right)$
lflnegcl.i ${⊢}{I}={inv}_{g}\left({R}\right)$
lflnegcl.n ${⊢}{N}=\left({x}\in {V}⟼{I}\left({G}\left({x}\right)\right)\right)$
lflnegcl.f ${⊢}{F}=\mathrm{LFnl}\left({W}\right)$
lflnegcl.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
lflnegcl.g ${⊢}{\phi }\to {G}\in {F}$
lflnegl.p
lflnegl.o
Assertion lflnegl

### Proof

Step Hyp Ref Expression
1 lflnegcl.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 lflnegcl.r ${⊢}{R}=\mathrm{Scalar}\left({W}\right)$
3 lflnegcl.i ${⊢}{I}={inv}_{g}\left({R}\right)$
4 lflnegcl.n ${⊢}{N}=\left({x}\in {V}⟼{I}\left({G}\left({x}\right)\right)\right)$
5 lflnegcl.f ${⊢}{F}=\mathrm{LFnl}\left({W}\right)$
6 lflnegcl.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
7 lflnegcl.g ${⊢}{\phi }\to {G}\in {F}$
8 lflnegl.p
9 lflnegl.o
10 1 fvexi ${⊢}{V}\in \mathrm{V}$
11 10 a1i ${⊢}{\phi }\to {V}\in \mathrm{V}$
12 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
13 2 12 1 5 lflf ${⊢}\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\to {G}:{V}⟶{\mathrm{Base}}_{{R}}$
14 6 7 13 syl2anc ${⊢}{\phi }\to {G}:{V}⟶{\mathrm{Base}}_{{R}}$
15 9 fvexi
16 15 a1i
17 2 lmodring ${⊢}{W}\in \mathrm{LMod}\to {R}\in \mathrm{Ring}$
18 ringgrp ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Grp}$
19 6 17 18 3syl ${⊢}{\phi }\to {R}\in \mathrm{Grp}$
20 12 3 19 grpinvf1o ${⊢}{\phi }\to {I}:{\mathrm{Base}}_{{R}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{R}}$
21 f1of ${⊢}{I}:{\mathrm{Base}}_{{R}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{R}}\to {I}:{\mathrm{Base}}_{{R}}⟶{\mathrm{Base}}_{{R}}$
22 20 21 syl ${⊢}{\phi }\to {I}:{\mathrm{Base}}_{{R}}⟶{\mathrm{Base}}_{{R}}$
23 4 a1i ${⊢}{\phi }\to {N}=\left({x}\in {V}⟼{I}\left({G}\left({x}\right)\right)\right)$
24 12 8 9 3 grplinv
25 19 24 sylan
26 11 14 16 22 23 25 caofinvl