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 = ( Base ` W )
	lflnegcl.r	\|- R = ( Scalar ` W )
	lflnegcl.i	\|- I = ( invg ` R )
	lflnegcl.n	\|- N = ( x e. V \|-> ( I ` ( G ` x ) ) )
	lflnegcl.f	\|- F = ( LFnl ` W )
	lflnegcl.w	\|- ( ph -> W e. LMod )
	lflnegcl.g	\|- ( ph -> G e. F )
	lflnegl.p	\|- .+ = ( +g ` R )
	lflnegl.o	\|- .0. = ( 0g ` R )
Assertion	lflnegl	\|- ( ph -> ( N oF .+ G ) = ( V X. { .0. } ) )

Proof

Step	Hyp	Ref	Expression
1		lflnegcl.v	\|- V = ( Base ` W )
2		lflnegcl.r	\|- R = ( Scalar ` W )
3		lflnegcl.i	\|- I = ( invg ` R )
4		lflnegcl.n	\|- N = ( x e. V \|-> ( I ` ( G ` x ) ) )
5		lflnegcl.f	\|- F = ( LFnl ` W )
6		lflnegcl.w	\|- ( ph -> W e. LMod )
7		lflnegcl.g	\|- ( ph -> G e. F )
8		lflnegl.p	\|- .+ = ( +g ` R )
9		lflnegl.o	\|- .0. = ( 0g ` R )
10	1	fvexi	\|- V e. _V
11	10	a1i	\|- ( ph -> V e. _V )
12		eqid	\|- ( Base ` R ) = ( Base ` R )
13	2 12 1 5	lflf	\|- ( ( W e. LMod /\ G e. F ) -> G : V --> ( Base ` R ) )
14	6 7 13	syl2anc	\|- ( ph -> G : V --> ( Base ` R ) )
15	9	fvexi	\|- .0. e. _V
16	15	a1i	\|- ( ph -> .0. e. _V )
17	2	lmodring	\|- ( W e. LMod -> R e. Ring )
18		ringgrp	\|- ( R e. Ring -> R e. Grp )
19	6 17 18	3syl	\|- ( ph -> R e. Grp )
20	12 3 19	grpinvf1o	\|- ( ph -> I : ( Base ` R ) -1-1-onto-> ( Base ` R ) )
21		f1of	\|- ( I : ( Base ` R ) -1-1-onto-> ( Base ` R ) -> I : ( Base ` R ) --> ( Base ` R ) )
22	20 21	syl	\|- ( ph -> I : ( Base ` R ) --> ( Base ` R ) )
23	4	a1i	\|- ( ph -> N = ( x e. V \|-> ( I ` ( G ` x ) ) ) )
24	12 8 9 3	grplinv	\|- ( ( R e. Grp /\ y e. ( Base ` R ) ) -> ( ( I ` y ) .+ y ) = .0. )
25	19 24	sylan	\|- ( ( ph /\ y e. ( Base ` R ) ) -> ( ( I ` y ) .+ y ) = .0. )
26	11 14 16 22 23 25	caofinvl	\|- ( ph -> ( N oF .+ G ) = ( V X. { .0. } ) )

Metamath Proof Explorer

Theorem lflnegl

Proof