ldualvsubval

Description: The value of the value of vector subtraction in the dual of a vector space. TODO: shorten with ldualvsub ? (Requires D to oppR conversion.) (Contributed by NM, 26-Feb-2015)

	Ref	Expression
Hypotheses	ldualvsubval.v	$⊢ V = {Base}_{W}$
	ldualvsubval.r	$⊢ R = Scalar (W)$
	ldualvsubval.s	$⊢ S = -_{R}$
	ldualvsubval.f	$⊢ F = LFnl (W)$
	ldualvsubval.d	$⊢ D = LDual (W)$
	ldualvsubval.m	$⊢ \underset{˙}{-} = -_{D}$
	ldualvsubval.w	$⊢ φ \to W \in LMod$
	ldualvsubval.g	$⊢ φ \to G \in F$
	ldualvsubval.h	$⊢ φ \to H \in F$
	ldualvsubval.x	$⊢ φ \to X \in V$
Assertion	ldualvsubval	$⊢ φ \to (G \underset{˙}{-} H) (X) = G (X) S H (X)$

Proof

Step	Hyp	Ref	Expression
1		ldualvsubval.v	$⊢ V = {Base}_{W}$
2		ldualvsubval.r	$⊢ R = Scalar (W)$
3		ldualvsubval.s	$⊢ S = -_{R}$
4		ldualvsubval.f	$⊢ F = LFnl (W)$
5		ldualvsubval.d	$⊢ D = LDual (W)$
6		ldualvsubval.m	$⊢ \underset{˙}{-} = -_{D}$
7		ldualvsubval.w	$⊢ φ \to W \in LMod$
8		ldualvsubval.g	$⊢ φ \to G \in F$
9		ldualvsubval.h	$⊢ φ \to H \in F$
10		ldualvsubval.x	$⊢ φ \to X \in V$
11	5 7	lduallmod	$⊢ φ \to D \in LMod$
12		eqid	$⊢ {Base}_{D} = {Base}_{D}$
13	4 5 12 7 8	ldualelvbase	$⊢ φ \to G \in {Base}_{D}$
14	4 5 12 7 9	ldualelvbase	$⊢ φ \to H \in {Base}_{D}$
15		eqid	$⊢ +_{D} = +_{D}$
16		eqid	$⊢ Scalar (D) = Scalar (D)$
17		eqid	$⊢ \cdot_{D} = \cdot_{D}$
18		eqid	$⊢ {inv}_{g} (Scalar (D)) = {inv}_{g} (Scalar (D))$
19		eqid	$⊢ 1_{Scalar (D)} = 1_{Scalar (D)}$
20	12 15 6 16 17 18 19	lmodvsubval2	$⊢ (D \in LMod \land G \in {Base}_{D} \land H \in {Base}_{D}) \to G \underset{˙}{-} H = G +_{D} ({inv}_{g} (Scalar (D)) (1_{Scalar (D)}) \cdot_{D} H)$
21	11 13 14 20	syl3anc	$⊢ φ \to G \underset{˙}{-} H = G +_{D} ({inv}_{g} (Scalar (D)) (1_{Scalar (D)}) \cdot_{D} H)$
22	21	fveq1d	$⊢ φ \to (G \underset{˙}{-} H) (X) = (G +_{D} ({inv}_{g} (Scalar (D)) (1_{Scalar (D)}) \cdot_{D} H)) (X)$
23		eqid	$⊢ +_{R} = +_{R}$
24		eqid	$⊢ {Base}_{R} = {Base}_{R}$
25	16	lmodfgrp	$⊢ D \in LMod \to Scalar (D) \in Grp$
26	11 25	syl	$⊢ φ \to Scalar (D) \in Grp$
27	16	lmodring	$⊢ D \in LMod \to Scalar (D) \in Ring$
28	11 27	syl	$⊢ φ \to Scalar (D) \in Ring$
29		eqid	$⊢ {Base}_{Scalar (D)} = {Base}_{Scalar (D)}$
30	29 19	ringidcl	$⊢ Scalar (D) \in Ring \to 1_{Scalar (D)} \in {Base}_{Scalar (D)}$
31	28 30	syl	$⊢ φ \to 1_{Scalar (D)} \in {Base}_{Scalar (D)}$
32	29 18	grpinvcl	$⊢ (Scalar (D) \in Grp \land 1_{Scalar (D)} \in {Base}_{Scalar (D)}) \to {inv}_{g} (Scalar (D)) (1_{Scalar (D)}) \in {Base}_{Scalar (D)}$
33	26 31 32	syl2anc	$⊢ φ \to {inv}_{g} (Scalar (D)) (1_{Scalar (D)}) \in {Base}_{Scalar (D)}$
34	2 24 5 16 29 7	ldualsbase	$⊢ φ \to {Base}_{Scalar (D)} = {Base}_{R}$
35	33 34	eleqtrd	$⊢ φ \to {inv}_{g} (Scalar (D)) (1_{Scalar (D)}) \in {Base}_{R}$
36	4 2 24 5 17 7 35 9	ldualvscl	$⊢ φ \to {inv}_{g} (Scalar (D)) (1_{Scalar (D)}) \cdot_{D} H \in F$
37	1 2 23 4 5 15 7 8 36 10	ldualvaddval	$⊢ φ \to (G +_{D} ({inv}_{g} (Scalar (D)) (1_{Scalar (D)}) \cdot_{D} H)) (X) = G (X) +_{R} ({inv}_{g} (Scalar (D)) (1_{Scalar (D)}) \cdot_{D} H) (X)$
38		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
39	2 38 5 16 18 7	ldualneg	$⊢ φ \to {inv}_{g} (Scalar (D)) = {inv}_{g} (R)$
40		eqid	$⊢ 1_{R} = 1_{R}$
41	2 40 5 16 19 7	ldual1	$⊢ φ \to 1_{Scalar (D)} = 1_{R}$
42	39 41	fveq12d	$⊢ φ \to {inv}_{g} (Scalar (D)) (1_{Scalar (D)}) = {inv}_{g} (R) (1_{R})$
43	42	oveq1d	$⊢ φ \to {inv}_{g} (Scalar (D)) (1_{Scalar (D)}) \cdot_{D} H = {inv}_{g} (R) (1_{R}) \cdot_{D} H$
44	43	fveq1d	$⊢ φ \to ({inv}_{g} (Scalar (D)) (1_{Scalar (D)}) \cdot_{D} H) (X) = ({inv}_{g} (R) (1_{R}) \cdot_{D} H) (X)$
45		eqid	$⊢ \cdot_{R} = \cdot_{R}$
46	2	lmodring	$⊢ W \in LMod \to R \in Ring$
47	7 46	syl	$⊢ φ \to R \in Ring$
48		ringgrp	$⊢ R \in Ring \to R \in Grp$
49	47 48	syl	$⊢ φ \to R \in Grp$
50	2 24 40	lmod1cl	$⊢ W \in LMod \to 1_{R} \in {Base}_{R}$
51	7 50	syl	$⊢ φ \to 1_{R} \in {Base}_{R}$
52	24 38	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	4 1 2 24 45 5 17 7 53 9 10	ldualvsval	$⊢ φ \to ({inv}_{g} (R) (1_{R}) \cdot_{D} H) (X) = H (X) \cdot_{R} {inv}_{g} (R) (1_{R})$
55	2 24 1 4	lflcl	$⊢ (W \in LMod \land H \in F \land X \in V) \to H (X) \in {Base}_{R}$
56	7 9 10 55	syl3anc	$⊢ φ \to H (X) \in {Base}_{R}$
57	24 45 40 38 47 56	ringnegr	$⊢ φ \to H (X) \cdot_{R} {inv}_{g} (R) (1_{R}) = {inv}_{g} (R) (H (X))$
58	44 54 57	3eqtrd	$⊢ φ \to ({inv}_{g} (Scalar (D)) (1_{Scalar (D)}) \cdot_{D} H) (X) = {inv}_{g} (R) (H (X))$
59	58	oveq2d	$⊢ φ \to G (X) +_{R} ({inv}_{g} (Scalar (D)) (1_{Scalar (D)}) \cdot_{D} H) (X) = G (X) +_{R} {inv}_{g} (R) (H (X))$
60	2 24 1 4	lflcl	$⊢ (W \in LMod \land G \in F \land X \in V) \to G (X) \in {Base}_{R}$
61	7 8 10 60	syl3anc	$⊢ φ \to G (X) \in {Base}_{R}$
62	24 23 38 3	grpsubval	$⊢ (G (X) \in {Base}_{R} \land H (X) \in {Base}_{R}) \to G (X) S H (X) = G (X) +_{R} {inv}_{g} (R) (H (X))$
63	61 56 62	syl2anc	$⊢ φ \to G (X) S H (X) = G (X) +_{R} {inv}_{g} (R) (H (X))$
64	59 63	eqtr4d	$⊢ φ \to G (X) +_{R} ({inv}_{g} (Scalar (D)) (1_{Scalar (D)}) \cdot_{D} H) (X) = G (X) S H (X)$
65	22 37 64	3eqtrd	$⊢ φ \to (G \underset{˙}{-} H) (X) = G (X) S H (X)$

Metamath Proof Explorer

Theorem ldualvsubval

Proof