lcdvsubval

Description: The value of the value of vector addition in the closed kernel vector space dual. (Contributed by NM, 11-Jun-2015)

	Ref	Expression
Hypotheses	lcdvsubval.h	$⊢ H = LHyp (K)$
	lcdvsubval.u	$⊢ U = DVecH (K) (W)$
	lcdvsubval.v	$⊢ V = {Base}_{U}$
	lcdvsubval.r	$⊢ R = Scalar (U)$
	lcdvsubval.s	$⊢ S = -_{R}$
	lcdvsubval.c	$⊢ C = LCDual (K) (W)$
	lcdvsubval.d	$⊢ D = {Base}_{C}$
	lcdvsubval.m	$⊢ \underset{˙}{-} = -_{C}$
	lcdvsubval.k	$⊢ φ \to (K \in HL \land W \in H)$
	lcdvsubval.f	$⊢ φ \to F \in D$
	lcdvsubval.g	$⊢ φ \to G \in D$
	lcdvsubval.x	$⊢ φ \to X \in V$
Assertion	lcdvsubval	$⊢ φ \to (F \underset{˙}{-} G) (X) = F (X) S G (X)$

Proof

Step	Hyp	Ref	Expression
1		lcdvsubval.h	$⊢ H = LHyp (K)$
2		lcdvsubval.u	$⊢ U = DVecH (K) (W)$
3		lcdvsubval.v	$⊢ V = {Base}_{U}$
4		lcdvsubval.r	$⊢ R = Scalar (U)$
5		lcdvsubval.s	$⊢ S = -_{R}$
6		lcdvsubval.c	$⊢ C = LCDual (K) (W)$
7		lcdvsubval.d	$⊢ D = {Base}_{C}$
8		lcdvsubval.m	$⊢ \underset{˙}{-} = -_{C}$
9		lcdvsubval.k	$⊢ φ \to (K \in HL \land W \in H)$
10		lcdvsubval.f	$⊢ φ \to F \in D$
11		lcdvsubval.g	$⊢ φ \to G \in D$
12		lcdvsubval.x	$⊢ φ \to X \in V$
13	1 6 9	lcdlmod	$⊢ φ \to C \in LMod$
14		eqid	$⊢ +_{C} = +_{C}$
15		eqid	$⊢ Scalar (C) = Scalar (C)$
16		eqid	$⊢ \cdot_{C} = \cdot_{C}$
17		eqid	$⊢ {inv}_{g} (Scalar (C)) = {inv}_{g} (Scalar (C))$
18		eqid	$⊢ 1_{Scalar (C)} = 1_{Scalar (C)}$
19	7 14 8 15 16 17 18	lmodvsubval2	$⊢ (C \in LMod \land F \in D \land G \in D) \to F \underset{˙}{-} G = F +_{C} ({inv}_{g} (Scalar (C)) (1_{Scalar (C)}) \cdot_{C} G)$
20	13 10 11 19	syl3anc	$⊢ φ \to F \underset{˙}{-} G = F +_{C} ({inv}_{g} (Scalar (C)) (1_{Scalar (C)}) \cdot_{C} G)$
21	20	fveq1d	$⊢ φ \to (F \underset{˙}{-} G) (X) = (F +_{C} ({inv}_{g} (Scalar (C)) (1_{Scalar (C)}) \cdot_{C} G)) (X)$
22		eqid	$⊢ +_{R} = +_{R}$
23		eqid	$⊢ {Base}_{R} = {Base}_{R}$
24	15	lmodfgrp	$⊢ C \in LMod \to Scalar (C) \in Grp$
25	13 24	syl	$⊢ φ \to Scalar (C) \in Grp$
26	15	lmodring	$⊢ C \in LMod \to Scalar (C) \in Ring$
27	13 26	syl	$⊢ φ \to Scalar (C) \in Ring$
28		eqid	$⊢ {Base}_{Scalar (C)} = {Base}_{Scalar (C)}$
29	28 18	ringidcl	$⊢ Scalar (C) \in Ring \to 1_{Scalar (C)} \in {Base}_{Scalar (C)}$
30	27 29	syl	$⊢ φ \to 1_{Scalar (C)} \in {Base}_{Scalar (C)}$
31	28 17	grpinvcl	$⊢ (Scalar (C) \in Grp \land 1_{Scalar (C)} \in {Base}_{Scalar (C)}) \to {inv}_{g} (Scalar (C)) (1_{Scalar (C)}) \in {Base}_{Scalar (C)}$
32	25 30 31	syl2anc	$⊢ φ \to {inv}_{g} (Scalar (C)) (1_{Scalar (C)}) \in {Base}_{Scalar (C)}$
33	1 2 4 23 6 15 28 9	lcdsbase	$⊢ φ \to {Base}_{Scalar (C)} = {Base}_{R}$
34	32 33	eleqtrd	$⊢ φ \to {inv}_{g} (Scalar (C)) (1_{Scalar (C)}) \in {Base}_{R}$
35	1 2 4 23 6 7 16 9 34 11	lcdvscl	$⊢ φ \to {inv}_{g} (Scalar (C)) (1_{Scalar (C)}) \cdot_{C} G \in D$
36	1 2 3 4 22 6 7 14 9 10 35 12	lcdvaddval	$⊢ φ \to (F +_{C} ({inv}_{g} (Scalar (C)) (1_{Scalar (C)}) \cdot_{C} G)) (X) = F (X) +_{R} ({inv}_{g} (Scalar (C)) (1_{Scalar (C)}) \cdot_{C} G) (X)$
37		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
38	1 2 4 37 6 15 17 9	lcdneg	$⊢ φ \to {inv}_{g} (Scalar (C)) = {inv}_{g} (R)$
39		eqid	$⊢ 1_{R} = 1_{R}$
40	1 2 4 39 6 15 18 9	lcd1	$⊢ φ \to 1_{Scalar (C)} = 1_{R}$
41	38 40	fveq12d	$⊢ φ \to {inv}_{g} (Scalar (C)) (1_{Scalar (C)}) = {inv}_{g} (R) (1_{R})$
42	41	oveq1d	$⊢ φ \to {inv}_{g} (Scalar (C)) (1_{Scalar (C)}) \cdot_{C} G = {inv}_{g} (R) (1_{R}) \cdot_{C} G$
43	42	fveq1d	$⊢ φ \to ({inv}_{g} (Scalar (C)) (1_{Scalar (C)}) \cdot_{C} G) (X) = ({inv}_{g} (R) (1_{R}) \cdot_{C} G) (X)$
44		eqid	$⊢ \cdot_{R} = \cdot_{R}$
45	1 2 9	dvhlmod	$⊢ φ \to U \in LMod$
46	4	lmodring	$⊢ U \in LMod \to R \in Ring$
47	45 46	syl	$⊢ φ \to R \in Ring$
48		ringgrp	$⊢ R \in Ring \to R \in Grp$
49	47 48	syl	$⊢ φ \to R \in Grp$
50	4 23 39	lmod1cl	$⊢ U \in LMod \to 1_{R} \in {Base}_{R}$
51	45 50	syl	$⊢ φ \to 1_{R} \in {Base}_{R}$
52	23 37	grpinvcl	$⊢ (R \in Grp \land 1_{R} \in {Base}_{R}) \to {inv}_{g} (R) (1_{R}) \in {Base}_{R}$
53	49 51 52	syl2anc	$⊢ φ \to {inv}_{g} (R) (1_{R}) \in {Base}_{R}$
54	1 2 3 4 23 44 6 7 16 9 53 11 12	lcdvsval	$⊢ φ \to ({inv}_{g} (R) (1_{R}) \cdot_{C} G) (X) = G (X) \cdot_{R} {inv}_{g} (R) (1_{R})$
55	1 2 3 4 23 6 7 9 11 12	lcdvbasecl	$⊢ φ \to G (X) \in {Base}_{R}$
56	23 44 39 37 47 55	ringnegr	$⊢ φ \to G (X) \cdot_{R} {inv}_{g} (R) (1_{R}) = {inv}_{g} (R) (G (X))$
57	43 54 56	3eqtrd	$⊢ φ \to ({inv}_{g} (Scalar (C)) (1_{Scalar (C)}) \cdot_{C} G) (X) = {inv}_{g} (R) (G (X))$
58	57	oveq2d	$⊢ φ \to F (X) +_{R} ({inv}_{g} (Scalar (C)) (1_{Scalar (C)}) \cdot_{C} G) (X) = F (X) +_{R} {inv}_{g} (R) (G (X))$
59	1 2 3 4 23 6 7 9 10 12	lcdvbasecl	$⊢ φ \to F (X) \in {Base}_{R}$
60	23 22 37 5	grpsubval	$⊢ (F (X) \in {Base}_{R} \land G (X) \in {Base}_{R}) \to F (X) S G (X) = F (X) +_{R} {inv}_{g} (R) (G (X))$
61	59 55 60	syl2anc	$⊢ φ \to F (X) S G (X) = F (X) +_{R} {inv}_{g} (R) (G (X))$
62	58 61	eqtr4d	$⊢ φ \to F (X) +_{R} ({inv}_{g} (Scalar (C)) (1_{Scalar (C)}) \cdot_{C} G) (X) = F (X) S G (X)$
63	21 36 62	3eqtrd	$⊢ φ \to (F \underset{˙}{-} G) (X) = F (X) S G (X)$

Metamath Proof Explorer

Theorem lcdvsubval

Proof