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	$$⊢\underset{\dot{}}{+}={+}_R$$
	lflnegl.o	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	lflnegl	$$⊢\phi \to N{\underset{\dot{}}{+}}_{f}G=V\times \left\{\underset{\dot{}}{0}\right\}$$

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	$$⊢\underset{\dot{}}{+}={+}_R$$
9		lflnegl.o	$$⊢\underset{\dot{}}{0}=0_R$$
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	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
16	15	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
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	$$⊢\left(R\in \mathrm{Grp}\wedge y\in {\mathrm{Base}}_R\right)\to I\left(y\right)\underset{\dot{}}{+}y=\underset{\dot{}}{0}$$
25	19 24	sylan	$$⊢\left(\phi \wedge y\in {\mathrm{Base}}_R\right)\to I\left(y\right)\underset{\dot{}}{+}y=\underset{\dot{}}{0}$$
26	11 14 16 22 23 25	caofinvl	$$⊢\phi \to N{\underset{\dot{}}{+}}_{f}G=V\times \left\{\underset{\dot{}}{0}\right\}$$