lflnegcl

Description: Closure of the negative of a 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$
Assertion	lflnegcl	$⊢ φ \to N \in F$

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	2	lmodring	$⊢ W \in LMod \to R \in Ring$
9	6 8	syl	$⊢ φ \to R \in Ring$
10		ringgrp	$⊢ R \in Ring \to R \in Grp$
11	9 10	syl	$⊢ φ \to R \in Grp$
12	11	adantr	$⊢ (φ \land x \in V) \to R \in Grp$
13	6	adantr	$⊢ (φ \land x \in V) \to W \in LMod$
14	7	adantr	$⊢ (φ \land x \in V) \to G \in F$
15		simpr	$⊢ (φ \land x \in V) \to x \in V$
16		eqid	$⊢ {Base}_{R} = {Base}_{R}$
17	2 16 1 5	lflcl	$⊢ (W \in LMod \land G \in F \land x \in V) \to G (x) \in {Base}_{R}$
18	13 14 15 17	syl3anc	$⊢ (φ \land x \in V) \to G (x) \in {Base}_{R}$
19	16 3	grpinvcl	$⊢ (R \in Grp \land G (x) \in {Base}_{R}) \to I (G (x)) \in {Base}_{R}$
20	12 18 19	syl2anc	$⊢ (φ \land x \in V) \to I (G (x)) \in {Base}_{R}$
21	20 4	fmptd	$⊢ φ \to N : V ⟶ {Base}_{R}$
22		ringabl	$⊢ R \in Ring \to R \in Abel$
23	9 22	syl	$⊢ φ \to R \in Abel$
24	23	adantr	$⊢ (φ \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to R \in Abel$
25	9	adantr	$⊢ (φ \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to R \in Ring$
26		simpr1	$⊢ (φ \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to k \in {Base}_{R}$
27	6	adantr	$⊢ (φ \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to W \in LMod$
28	7	adantr	$⊢ (φ \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to G \in F$
29		simpr2	$⊢ (φ \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to y \in V$
30	2 16 1 5	lflcl	$⊢ (W \in LMod \land G \in F \land y \in V) \to G (y) \in {Base}_{R}$
31	27 28 29 30	syl3anc	$⊢ (φ \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to G (y) \in {Base}_{R}$
32		eqid	$⊢ \cdot_{R} = \cdot_{R}$
33	16 32	ringcl	$⊢ (R \in Ring \land k \in {Base}_{R} \land G (y) \in {Base}_{R}) \to k \cdot_{R} G (y) \in {Base}_{R}$
34	25 26 31 33	syl3anc	$⊢ (φ \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to k \cdot_{R} G (y) \in {Base}_{R}$
35		simpr3	$⊢ (φ \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to z \in V$
36	2 16 1 5	lflcl	$⊢ (W \in LMod \land G \in F \land z \in V) \to G (z) \in {Base}_{R}$
37	27 28 35 36	syl3anc	$⊢ (φ \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to G (z) \in {Base}_{R}$
38		eqid	$⊢ +_{R} = +_{R}$
39	16 38 3	ablinvadd	$⊢ (R \in Abel \land k \cdot_{R} G (y) \in {Base}_{R} \land G (z) \in {Base}_{R}) \to I ((k \cdot_{R} G (y)) +_{R} G (z)) = I (k \cdot_{R} G (y)) +_{R} I (G (z))$
40	24 34 37 39	syl3anc	$⊢ (φ \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to I ((k \cdot_{R} G (y)) +_{R} G (z)) = I (k \cdot_{R} G (y)) +_{R} I (G (z))$
41		eqid	$⊢ +_{W} = +_{W}$
42		eqid	$⊢ \cdot_{W} = \cdot_{W}$
43	1 41 2 42 16 38 32 5	lfli	$⊢ (W \in LMod \land G \in F \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to G ((k \cdot_{W} y) +_{W} z) = (k \cdot_{R} G (y)) +_{R} G (z)$
44	27 28 26 29 35 43	syl113anc	$⊢ (φ \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to G ((k \cdot_{W} y) +_{W} z) = (k \cdot_{R} G (y)) +_{R} G (z)$
45	44	fveq2d	$⊢ (φ \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to I (G ((k \cdot_{W} y) +_{W} z)) = I ((k \cdot_{R} G (y)) +_{R} G (z))$
46	16 32 3 25 26 31	ringmneg2	$⊢ (φ \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to k \cdot_{R} I (G (y)) = I (k \cdot_{R} G (y))$
47	46	oveq1d	$⊢ (φ \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to (k \cdot_{R} I (G (y))) +_{R} I (G (z)) = I (k \cdot_{R} G (y)) +_{R} I (G (z))$
48	40 45 47	3eqtr4d	$⊢ (φ \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to I (G ((k \cdot_{W} y) +_{W} z)) = (k \cdot_{R} I (G (y))) +_{R} I (G (z))$
49	1 2 42 16	lmodvscl	$⊢ (W \in LMod \land k \in {Base}_{R} \land y \in V) \to k \cdot_{W} y \in V$
50	27 26 29 49	syl3anc	$⊢ (φ \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to k \cdot_{W} y \in V$
51	1 41	lmodvacl	$⊢ (W \in LMod \land k \cdot_{W} y \in V \land z \in V) \to (k \cdot_{W} y) +_{W} z \in V$
52	27 50 35 51	syl3anc	$⊢ (φ \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to (k \cdot_{W} y) +_{W} z \in V$
53		2fveq3	$⊢ x = (k \cdot_{W} y) +_{W} z \to I (G (x)) = I (G ((k \cdot_{W} y) +_{W} z))$
54		fvex	$⊢ I (G ((k \cdot_{W} y) +_{W} z)) \in V$
55	53 4 54	fvmpt	$⊢ (k \cdot_{W} y) +_{W} z \in V \to N ((k \cdot_{W} y) +_{W} z) = I (G ((k \cdot_{W} y) +_{W} z))$
56	52 55	syl	$⊢ (φ \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to N ((k \cdot_{W} y) +_{W} z) = I (G ((k \cdot_{W} y) +_{W} z))$
57		2fveq3	$⊢ x = y \to I (G (x)) = I (G (y))$
58		fvex	$⊢ I (G (y)) \in V$
59	57 4 58	fvmpt	$⊢ y \in V \to N (y) = I (G (y))$
60	29 59	syl	$⊢ (φ \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to N (y) = I (G (y))$
61	60	oveq2d	$⊢ (φ \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to k \cdot_{R} N (y) = k \cdot_{R} I (G (y))$
62		2fveq3	$⊢ x = z \to I (G (x)) = I (G (z))$
63		fvex	$⊢ I (G (z)) \in V$
64	62 4 63	fvmpt	$⊢ z \in V \to N (z) = I (G (z))$
65	35 64	syl	$⊢ (φ \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to N (z) = I (G (z))$
66	61 65	oveq12d	$⊢ (φ \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to (k \cdot_{R} N (y)) +_{R} N (z) = (k \cdot_{R} I (G (y))) +_{R} I (G (z))$
67	48 56 66	3eqtr4d	$⊢ (φ \land (k \in {Base}_{R} \land y \in V \land z \in V)) \to N ((k \cdot_{W} y) +_{W} z) = (k \cdot_{R} N (y)) +_{R} N (z)$
68	67	ralrimivvva	$⊢ φ \to \forall k \in {Base}_{R} \forall y \in V \forall z \in V N ((k \cdot_{W} y) +_{W} z) = (k \cdot_{R} N (y)) +_{R} N (z)$
69	1 41 2 42 16 38 32 5	islfl	$⊢ W \in LMod \to (N \in F \leftrightarrow (N : V ⟶ {Base}_{R} \land \forall k \in {Base}_{R} \forall y \in V \forall z \in V N ((k \cdot_{W} y) +_{W} z) = (k \cdot_{R} N (y)) +_{R} N (z)))$
70	6 69	syl	$⊢ φ \to (N \in F \leftrightarrow (N : V ⟶ {Base}_{R} \land \forall k \in {Base}_{R} \forall y \in V \forall z \in V N ((k \cdot_{W} y) +_{W} z) = (k \cdot_{R} N (y)) +_{R} N (z)))$
71	21 68 70	mpbir2and	$⊢ φ \to N \in F$

Metamath Proof Explorer

Theorem lflnegcl

Proof