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	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lflnegcl.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
	lflnegcl.i	⊢ 𝐼 = ( invg ‘ 𝑅 )
	lflnegcl.n	⊢ 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( 𝐼 ‘ ( 𝐺 ‘ 𝑥 ) ) )
	lflnegcl.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	lflnegcl.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lflnegcl.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
	lflnegl.p	⊢ + = ( +g ‘ 𝑅 )
	lflnegl.o	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	lflnegl	⊢ ( 𝜑 → ( 𝑁 ∘f + 𝐺 ) = ( 𝑉 × { 0 } ) )

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		lflnegl.p	⊢ + = ( +g ‘ 𝑅 )
9		lflnegl.o	⊢ 0 = ( 0g ‘ 𝑅 )
10	1	fvexi	⊢ 𝑉 ∈ V
11	10	a1i	⊢ ( 𝜑 → 𝑉 ∈ V )
12		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
13	2 12 1 5	lflf	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ ( Base ‘ 𝑅 ) )
14	6 7 13	syl2anc	⊢ ( 𝜑 → 𝐺 : 𝑉 ⟶ ( Base ‘ 𝑅 ) )
15	9	fvexi	⊢ 0 ∈ V
16	15	a1i	⊢ ( 𝜑 → 0 ∈ V )
17	2	lmodring	⊢ ( 𝑊 ∈ LMod → 𝑅 ∈ Ring )
18		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
19	6 17 18	3syl	⊢ ( 𝜑 → 𝑅 ∈ Grp )
20	12 3 19	grpinvf1o	⊢ ( 𝜑 → 𝐼 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑅 ) )
21		f1of	⊢ ( 𝐼 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑅 ) → 𝐼 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) )
22	20 21	syl	⊢ ( 𝜑 → 𝐼 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) )
23	4	a1i	⊢ ( 𝜑 → 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( 𝐼 ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
24	12 8 9 3	grplinv	⊢ ( ( 𝑅 ∈ Grp ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐼 ‘ 𝑦 ) + 𝑦 ) = 0 )
25	19 24	sylan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐼 ‘ 𝑦 ) + 𝑦 ) = 0 )
26	11 14 16 22 23 25	caofinvl	⊢ ( 𝜑 → ( 𝑁 ∘f + 𝐺 ) = ( 𝑉 × { 0 } ) )