Theorem 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	⊢ 𝑉 = ( Base ‘ 𝑊 )
	ldualvsubval.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
	ldualvsubval.s	⊢ 𝑆 = ( -g ‘ 𝑅 )
	ldualvsubval.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	ldualvsubval.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
	ldualvsubval.m	⊢ − = ( -g ‘ 𝐷 )
	ldualvsubval.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	ldualvsubval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
	ldualvsubval.h	⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
	ldualvsubval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	ldualvsubval	⊢ ( 𝜑 → ( ( 𝐺 − 𝐻 ) ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) 𝑆 ( 𝐻 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ldualvsubval.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		ldualvsubval.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
3		ldualvsubval.s	⊢ 𝑆 = ( -g ‘ 𝑅 )
4		ldualvsubval.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
5		ldualvsubval.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
6		ldualvsubval.m	⊢ − = ( -g ‘ 𝐷 )
7		ldualvsubval.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
8		ldualvsubval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
9		ldualvsubval.h	⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
10		ldualvsubval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
11	5 7	lduallmod	⊢ ( 𝜑 → 𝐷 ∈ LMod )
12		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
13	4 5 12 7 8	ldualelvbase	⊢ ( 𝜑 → 𝐺 ∈ ( Base ‘ 𝐷 ) )
14	4 5 12 7 9	ldualelvbase	⊢ ( 𝜑 → 𝐻 ∈ ( Base ‘ 𝐷 ) )
15		eqid	⊢ ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 )
16		eqid	⊢ ( Scalar ‘ 𝐷 ) = ( Scalar ‘ 𝐷 )
17		eqid	⊢ ( ·𝑠 ‘ 𝐷 ) = ( ·𝑠 ‘ 𝐷 )
18		eqid	⊢ ( invg ‘ ( Scalar ‘ 𝐷 ) ) = ( invg ‘ ( Scalar ‘ 𝐷 ) )
19		eqid	⊢ ( 1r ‘ ( Scalar ‘ 𝐷 ) ) = ( 1r ‘ ( Scalar ‘ 𝐷 ) )
20	12 15 6 16 17 18 19	lmodvsubval2	⊢ ( ( 𝐷 ∈ LMod ∧ 𝐺 ∈ ( Base ‘ 𝐷 ) ∧ 𝐻 ∈ ( Base ‘ 𝐷 ) ) → ( 𝐺 − 𝐻 ) = ( 𝐺 ( +g ‘ 𝐷 ) ( ( ( invg ‘ ( Scalar ‘ 𝐷 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐷 ) ) ) ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) )
21	11 13 14 20	syl3anc	⊢ ( 𝜑 → ( 𝐺 − 𝐻 ) = ( 𝐺 ( +g ‘ 𝐷 ) ( ( ( invg ‘ ( Scalar ‘ 𝐷 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐷 ) ) ) ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) )
22	21	fveq1d	⊢ ( 𝜑 → ( ( 𝐺 − 𝐻 ) ‘ 𝑋 ) = ( ( 𝐺 ( +g ‘ 𝐷 ) ( ( ( invg ‘ ( Scalar ‘ 𝐷 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐷 ) ) ) ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) ‘ 𝑋 ) )
23		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
24		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
25	16	lmodfgrp	⊢ ( 𝐷 ∈ LMod → ( Scalar ‘ 𝐷 ) ∈ Grp )
26	11 25	syl	⊢ ( 𝜑 → ( Scalar ‘ 𝐷 ) ∈ Grp )
27	16	lmodring	⊢ ( 𝐷 ∈ LMod → ( Scalar ‘ 𝐷 ) ∈ Ring )
28	11 27	syl	⊢ ( 𝜑 → ( Scalar ‘ 𝐷 ) ∈ Ring )
29		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝐷 ) ) = ( Base ‘ ( Scalar ‘ 𝐷 ) )
30	29 19	ringidcl	⊢ ( ( Scalar ‘ 𝐷 ) ∈ Ring → ( 1r ‘ ( Scalar ‘ 𝐷 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) )
31	28 30	syl	⊢ ( 𝜑 → ( 1r ‘ ( Scalar ‘ 𝐷 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) )
32	29 18	grpinvcl	⊢ ( ( ( Scalar ‘ 𝐷 ) ∈ Grp ∧ ( 1r ‘ ( Scalar ‘ 𝐷 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) ) → ( ( invg ‘ ( Scalar ‘ 𝐷 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐷 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) )
33	26 31 32	syl2anc	⊢ ( 𝜑 → ( ( invg ‘ ( Scalar ‘ 𝐷 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐷 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) )
34	2 24 5 16 29 7	ldualsbase	⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐷 ) ) = ( Base ‘ 𝑅 ) )
35	33 34	eleqtrd	⊢ ( 𝜑 → ( ( invg ‘ ( Scalar ‘ 𝐷 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐷 ) ) ) ∈ ( Base ‘ 𝑅 ) )
36	4 2 24 5 17 7 35 9	ldualvscl	⊢ ( 𝜑 → ( ( ( invg ‘ ( Scalar ‘ 𝐷 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐷 ) ) ) ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ∈ 𝐹 )
37	1 2 23 4 5 15 7 8 36 10	ldualvaddval	⊢ ( 𝜑 → ( ( 𝐺 ( +g ‘ 𝐷 ) ( ( ( invg ‘ ( Scalar ‘ 𝐷 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐷 ) ) ) ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) ( +g ‘ 𝑅 ) ( ( ( ( invg ‘ ( Scalar ‘ 𝐷 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐷 ) ) ) ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ‘ 𝑋 ) ) )
38		eqid	⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
39	2 38 5 16 18 7	ldualneg	⊢ ( 𝜑 → ( invg ‘ ( Scalar ‘ 𝐷 ) ) = ( invg ‘ 𝑅 ) )
40		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
41	2 40 5 16 19 7	ldual1	⊢ ( 𝜑 → ( 1r ‘ ( Scalar ‘ 𝐷 ) ) = ( 1r ‘ 𝑅 ) )
42	39 41	fveq12d	⊢ ( 𝜑 → ( ( invg ‘ ( Scalar ‘ 𝐷 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐷 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) )
43	42	oveq1d	⊢ ( 𝜑 → ( ( ( invg ‘ ( Scalar ‘ 𝐷 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐷 ) ) ) ( ·𝑠 ‘ 𝐷 ) 𝐻 ) = ( ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ( ·𝑠 ‘ 𝐷 ) 𝐻 ) )
44	43	fveq1d	⊢ ( 𝜑 → ( ( ( ( invg ‘ ( Scalar ‘ 𝐷 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐷 ) ) ) ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ‘ 𝑋 ) = ( ( ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ‘ 𝑋 ) )
45		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
46	2	lmodring	⊢ ( 𝑊 ∈ LMod → 𝑅 ∈ Ring )
47	7 46	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
48		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
49	47 48	syl	⊢ ( 𝜑 → 𝑅 ∈ Grp )
50	2 24 40	lmod1cl	⊢ ( 𝑊 ∈ LMod → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
51	7 50	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
52	24 38	grpinvcl	⊢ ( ( 𝑅 ∈ Grp ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
53	49 51 52	syl2anc	⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
54	4 1 2 24 45 5 17 7 53 9 10	ldualvsval	⊢ ( 𝜑 → ( ( ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ‘ 𝑋 ) = ( ( 𝐻 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) )
55	2 24 1 4	lflcl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐻 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) )
56	7 9 10 55	syl3anc	⊢ ( 𝜑 → ( 𝐻 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) )
57	24 45 40 38 47 56	ringnegr	⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐻 ‘ 𝑋 ) ) )
58	44 54 57	3eqtrd	⊢ ( 𝜑 → ( ( ( ( invg ‘ ( Scalar ‘ 𝐷 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐷 ) ) ) ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ‘ 𝑋 ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐻 ‘ 𝑋 ) ) )
59	58	oveq2d	⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) ( +g ‘ 𝑅 ) ( ( ( ( invg ‘ ( Scalar ‘ 𝐷 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐷 ) ) ) ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ‘ 𝑋 ) ) = ( ( 𝐺 ‘ 𝑋 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 𝐻 ‘ 𝑋 ) ) ) )
60	2 24 1 4	lflcl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) )
61	7 8 10 60	syl3anc	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) )
62	24 23 38 3	grpsubval	⊢ ( ( ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐻 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐺 ‘ 𝑋 ) 𝑆 ( 𝐻 ‘ 𝑋 ) ) = ( ( 𝐺 ‘ 𝑋 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 𝐻 ‘ 𝑋 ) ) ) )
63	61 56 62	syl2anc	⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) 𝑆 ( 𝐻 ‘ 𝑋 ) ) = ( ( 𝐺 ‘ 𝑋 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 𝐻 ‘ 𝑋 ) ) ) )
64	59 63	eqtr4d	⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) ( +g ‘ 𝑅 ) ( ( ( ( invg ‘ ( Scalar ‘ 𝐷 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐷 ) ) ) ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ‘ 𝑋 ) ) = ( ( 𝐺 ‘ 𝑋 ) 𝑆 ( 𝐻 ‘ 𝑋 ) ) )
65	22 37 64	3eqtrd	⊢ ( 𝜑 → ( ( 𝐺 − 𝐻 ) ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) 𝑆 ( 𝐻 ‘ 𝑋 ) ) )