lflsub

Description: Property of a linear functional. ( lnfnaddi analog.) (Contributed by NM, 18-Apr-2014)

	Ref	Expression
Hypotheses	lflsub.d	$⊢ D = Scalar (W)$
	lflsub.m	$⊢ M = -_{D}$
	lflsub.v	$⊢ V = {Base}_{W}$
	lflsub.a	$⊢ \underset{˙}{-} = -_{W}$
	lflsub.f	$⊢ F = LFnl (W)$
Assertion	lflsub	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to G (X \underset{˙}{-} Y) = G (X) M G (Y)$

Proof

Step	Hyp	Ref	Expression
1		lflsub.d	$⊢ D = Scalar (W)$
2		lflsub.m	$⊢ M = -_{D}$
3		lflsub.v	$⊢ V = {Base}_{W}$
4		lflsub.a	$⊢ \underset{˙}{-} = -_{W}$
5		lflsub.f	$⊢ F = LFnl (W)$
6		simp1	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to W \in LMod$
7		simp3l	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to X \in V$
8	1	lmodring	$⊢ W \in LMod \to D \in Ring$
9	8	3ad2ant1	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to D \in Ring$
10		ringgrp	$⊢ D \in Ring \to D \in Grp$
11	9 10	syl	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to D \in Grp$
12		eqid	$⊢ {Base}_{D} = {Base}_{D}$
13		eqid	$⊢ 1_{D} = 1_{D}$
14	12 13	ringidcl	$⊢ D \in Ring \to 1_{D} \in {Base}_{D}$
15	9 14	syl	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to 1_{D} \in {Base}_{D}$
16		eqid	$⊢ {inv}_{g} (D) = {inv}_{g} (D)$
17	12 16	grpinvcl	$⊢ (D \in Grp \land 1_{D} \in {Base}_{D}) \to {inv}_{g} (D) (1_{D}) \in {Base}_{D}$
18	11 15 17	syl2anc	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to {inv}_{g} (D) (1_{D}) \in {Base}_{D}$
19		simp3r	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to Y \in V$
20		eqid	$⊢ \cdot_{W} = \cdot_{W}$
21	3 1 20 12	lmodvscl	$⊢ (W \in LMod \land {inv}_{g} (D) (1_{D}) \in {Base}_{D} \land Y \in V) \to {inv}_{g} (D) (1_{D}) \cdot_{W} Y \in V$
22	6 18 19 21	syl3anc	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to {inv}_{g} (D) (1_{D}) \cdot_{W} Y \in V$
23		eqid	$⊢ +_{W} = +_{W}$
24	3 23	lmodcom	$⊢ (W \in LMod \land X \in V \land {inv}_{g} (D) (1_{D}) \cdot_{W} Y \in V) \to X +_{W} ({inv}_{g} (D) (1_{D}) \cdot_{W} Y) = ({inv}_{g} (D) (1_{D}) \cdot_{W} Y) +_{W} X$
25	6 7 22 24	syl3anc	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to X +_{W} ({inv}_{g} (D) (1_{D}) \cdot_{W} Y) = ({inv}_{g} (D) (1_{D}) \cdot_{W} Y) +_{W} X$
26	25	fveq2d	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to G (X +_{W} ({inv}_{g} (D) (1_{D}) \cdot_{W} Y)) = G (({inv}_{g} (D) (1_{D}) \cdot_{W} Y) +_{W} X)$
27		simp2	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to G \in F$
28		eqid	$⊢ +_{D} = +_{D}$
29		eqid	$⊢ \cdot_{D} = \cdot_{D}$
30	3 23 1 20 12 28 29 5	lfli	$⊢ (W \in LMod \land G \in F \land ({inv}_{g} (D) (1_{D}) \in {Base}_{D} \land Y \in V \land X \in V)) \to G (({inv}_{g} (D) (1_{D}) \cdot_{W} Y) +_{W} X) = ({inv}_{g} (D) (1_{D}) \cdot_{D} G (Y)) +_{D} G (X)$
31	6 27 18 19 7 30	syl113anc	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to G (({inv}_{g} (D) (1_{D}) \cdot_{W} Y) +_{W} X) = ({inv}_{g} (D) (1_{D}) \cdot_{D} G (Y)) +_{D} G (X)$
32	1 12 3 5	lflcl	$⊢ (W \in LMod \land G \in F \land Y \in V) \to G (Y) \in {Base}_{D}$
33	32	3adant3l	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to G (Y) \in {Base}_{D}$
34	12 29 13 16 9 33	ringnegl	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to {inv}_{g} (D) (1_{D}) \cdot_{D} G (Y) = {inv}_{g} (D) (G (Y))$
35	34	oveq1d	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to ({inv}_{g} (D) (1_{D}) \cdot_{D} G (Y)) +_{D} G (X) = {inv}_{g} (D) (G (Y)) +_{D} G (X)$
36		ringabl	$⊢ D \in Ring \to D \in Abel$
37	9 36	syl	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to D \in Abel$
38	12 16	grpinvcl	$⊢ (D \in Grp \land G (Y) \in {Base}_{D}) \to {inv}_{g} (D) (G (Y)) \in {Base}_{D}$
39	11 33 38	syl2anc	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to {inv}_{g} (D) (G (Y)) \in {Base}_{D}$
40	1 12 3 5	lflcl	$⊢ (W \in LMod \land G \in F \land X \in V) \to G (X) \in {Base}_{D}$
41	40	3adant3r	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to G (X) \in {Base}_{D}$
42	12 28	ablcom	$⊢ (D \in Abel \land {inv}_{g} (D) (G (Y)) \in {Base}_{D} \land G (X) \in {Base}_{D}) \to {inv}_{g} (D) (G (Y)) +_{D} G (X) = G (X) +_{D} {inv}_{g} (D) (G (Y))$
43	37 39 41 42	syl3anc	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to {inv}_{g} (D) (G (Y)) +_{D} G (X) = G (X) +_{D} {inv}_{g} (D) (G (Y))$
44	35 43	eqtrd	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to ({inv}_{g} (D) (1_{D}) \cdot_{D} G (Y)) +_{D} G (X) = G (X) +_{D} {inv}_{g} (D) (G (Y))$
45	26 31 44	3eqtrd	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to G (X +_{W} ({inv}_{g} (D) (1_{D}) \cdot_{W} Y)) = G (X) +_{D} {inv}_{g} (D) (G (Y))$
46	3 23 4 1 20 16 13	lmodvsubval2	$⊢ (W \in LMod \land X \in V \land Y \in V) \to X \underset{˙}{-} Y = X +_{W} ({inv}_{g} (D) (1_{D}) \cdot_{W} Y)$
47	6 7 19 46	syl3anc	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to X \underset{˙}{-} Y = X +_{W} ({inv}_{g} (D) (1_{D}) \cdot_{W} Y)$
48	47	fveq2d	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to G (X \underset{˙}{-} Y) = G (X +_{W} ({inv}_{g} (D) (1_{D}) \cdot_{W} Y))$
49	12 28 16 2	grpsubval	$⊢ (G (X) \in {Base}_{D} \land G (Y) \in {Base}_{D}) \to G (X) M G (Y) = G (X) +_{D} {inv}_{g} (D) (G (Y))$
50	41 33 49	syl2anc	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to G (X) M G (Y) = G (X) +_{D} {inv}_{g} (D) (G (Y))$
51	45 48 50	3eqtr4d	$⊢ (W \in LMod \land G \in F \land (X \in V \land Y \in V)) \to G (X \underset{˙}{-} Y) = G (X) M G (Y)$

Metamath Proof Explorer

Theorem lflsub

Proof