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 = {inv}_{g} (R)$
	lflnegcl.n	$⊢ N = (x \in V ⟼ I (G (x)))$
	lflnegcl.f	$⊢ F = LFnl (W)$
	lflnegcl.w	$⊢ φ \to W \in LMod$
	lflnegcl.g	$⊢ φ \to G \in F$
	lflnegl.p	$⊢ \underset{˙}{+} = +_{R}$
	lflnegl.o	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	lflnegl	$⊢ φ \to N {\underset{˙}{+}}_{f} G = V \times \{\underset{˙}{0}\}$

Proof

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

Metamath Proof Explorer

Theorem lflnegl

Proof