Theorem 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	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcdvsubval.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcdvsubval.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	lcdvsubval.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	lcdvsubval.s	⊢ 𝑆 = ( -g ‘ 𝑅 )
	lcdvsubval.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	lcdvsubval.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
	lcdvsubval.m	⊢ − = ( -g ‘ 𝐶 )
	lcdvsubval.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lcdvsubval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
	lcdvsubval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐷 )
	lcdvsubval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	lcdvsubval	⊢ ( 𝜑 → ( ( 𝐹 − 𝐺 ) ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑋 ) 𝑆 ( 𝐺 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lcdvsubval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcdvsubval.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		lcdvsubval.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		lcdvsubval.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
5		lcdvsubval.s	⊢ 𝑆 = ( -g ‘ 𝑅 )
6		lcdvsubval.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
7		lcdvsubval.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
8		lcdvsubval.m	⊢ − = ( -g ‘ 𝐶 )
9		lcdvsubval.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		lcdvsubval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
11		lcdvsubval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐷 )
12		lcdvsubval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
13	1 6 9	lcdlmod	⊢ ( 𝜑 → 𝐶 ∈ LMod )
14		eqid	⊢ ( +g ‘ 𝐶 ) = ( +g ‘ 𝐶 )
15		eqid	⊢ ( Scalar ‘ 𝐶 ) = ( Scalar ‘ 𝐶 )
16		eqid	⊢ ( ·𝑠 ‘ 𝐶 ) = ( ·𝑠 ‘ 𝐶 )
17		eqid	⊢ ( invg ‘ ( Scalar ‘ 𝐶 ) ) = ( invg ‘ ( Scalar ‘ 𝐶 ) )
18		eqid	⊢ ( 1r ‘ ( Scalar ‘ 𝐶 ) ) = ( 1r ‘ ( Scalar ‘ 𝐶 ) )
19	7 14 8 15 16 17 18	lmodvsubval2	⊢ ( ( 𝐶 ∈ LMod ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ) → ( 𝐹 − 𝐺 ) = ( 𝐹 ( +g ‘ 𝐶 ) ( ( ( invg ‘ ( Scalar ‘ 𝐶 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐶 ) ) ) ( ·𝑠 ‘ 𝐶 ) 𝐺 ) ) )
20	13 10 11 19	syl3anc	⊢ ( 𝜑 → ( 𝐹 − 𝐺 ) = ( 𝐹 ( +g ‘ 𝐶 ) ( ( ( invg ‘ ( Scalar ‘ 𝐶 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐶 ) ) ) ( ·𝑠 ‘ 𝐶 ) 𝐺 ) ) )
21	20	fveq1d	⊢ ( 𝜑 → ( ( 𝐹 − 𝐺 ) ‘ 𝑋 ) = ( ( 𝐹 ( +g ‘ 𝐶 ) ( ( ( invg ‘ ( Scalar ‘ 𝐶 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐶 ) ) ) ( ·𝑠 ‘ 𝐶 ) 𝐺 ) ) ‘ 𝑋 ) )
22		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
23		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
24	15	lmodfgrp	⊢ ( 𝐶 ∈ LMod → ( Scalar ‘ 𝐶 ) ∈ Grp )
25	13 24	syl	⊢ ( 𝜑 → ( Scalar ‘ 𝐶 ) ∈ Grp )
26	15	lmodring	⊢ ( 𝐶 ∈ LMod → ( Scalar ‘ 𝐶 ) ∈ Ring )
27	13 26	syl	⊢ ( 𝜑 → ( Scalar ‘ 𝐶 ) ∈ Ring )
28		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝐶 ) ) = ( Base ‘ ( Scalar ‘ 𝐶 ) )
29	28 18	ringidcl	⊢ ( ( Scalar ‘ 𝐶 ) ∈ Ring → ( 1r ‘ ( Scalar ‘ 𝐶 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
30	27 29	syl	⊢ ( 𝜑 → ( 1r ‘ ( Scalar ‘ 𝐶 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
31	28 17	grpinvcl	⊢ ( ( ( Scalar ‘ 𝐶 ) ∈ Grp ∧ ( 1r ‘ ( Scalar ‘ 𝐶 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) ) → ( ( invg ‘ ( Scalar ‘ 𝐶 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐶 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
32	25 30 31	syl2anc	⊢ ( 𝜑 → ( ( invg ‘ ( Scalar ‘ 𝐶 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐶 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
33	1 2 4 23 6 15 28 9	lcdsbase	⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐶 ) ) = ( Base ‘ 𝑅 ) )
34	32 33	eleqtrd	⊢ ( 𝜑 → ( ( invg ‘ ( Scalar ‘ 𝐶 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐶 ) ) ) ∈ ( Base ‘ 𝑅 ) )
35	1 2 4 23 6 7 16 9 34 11	lcdvscl	⊢ ( 𝜑 → ( ( ( invg ‘ ( Scalar ‘ 𝐶 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐶 ) ) ) ( ·𝑠 ‘ 𝐶 ) 𝐺 ) ∈ 𝐷 )
36	1 2 3 4 22 6 7 14 9 10 35 12	lcdvaddval	⊢ ( 𝜑 → ( ( 𝐹 ( +g ‘ 𝐶 ) ( ( ( invg ‘ ( Scalar ‘ 𝐶 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐶 ) ) ) ( ·𝑠 ‘ 𝐶 ) 𝐺 ) ) ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑋 ) ( +g ‘ 𝑅 ) ( ( ( ( invg ‘ ( Scalar ‘ 𝐶 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐶 ) ) ) ( ·𝑠 ‘ 𝐶 ) 𝐺 ) ‘ 𝑋 ) ) )
37		eqid	⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
38	1 2 4 37 6 15 17 9	lcdneg	⊢ ( 𝜑 → ( invg ‘ ( Scalar ‘ 𝐶 ) ) = ( invg ‘ 𝑅 ) )
39		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
40	1 2 4 39 6 15 18 9	lcd1	⊢ ( 𝜑 → ( 1r ‘ ( Scalar ‘ 𝐶 ) ) = ( 1r ‘ 𝑅 ) )
41	38 40	fveq12d	⊢ ( 𝜑 → ( ( invg ‘ ( Scalar ‘ 𝐶 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐶 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) )
42	41	oveq1d	⊢ ( 𝜑 → ( ( ( invg ‘ ( Scalar ‘ 𝐶 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐶 ) ) ) ( ·𝑠 ‘ 𝐶 ) 𝐺 ) = ( ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ( ·𝑠 ‘ 𝐶 ) 𝐺 ) )
43	42	fveq1d	⊢ ( 𝜑 → ( ( ( ( invg ‘ ( Scalar ‘ 𝐶 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐶 ) ) ) ( ·𝑠 ‘ 𝐶 ) 𝐺 ) ‘ 𝑋 ) = ( ( ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ( ·𝑠 ‘ 𝐶 ) 𝐺 ) ‘ 𝑋 ) )
44		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
45	1 2 9	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
46	4	lmodring	⊢ ( 𝑈 ∈ LMod → 𝑅 ∈ Ring )
47	45 46	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
48		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
49	47 48	syl	⊢ ( 𝜑 → 𝑅 ∈ Grp )
50	4 23 39	lmod1cl	⊢ ( 𝑈 ∈ LMod → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
51	45 50	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
52	23 37	grpinvcl	⊢ ( ( 𝑅 ∈ Grp ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
53	49 51 52	syl2anc	⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
54	1 2 3 4 23 44 6 7 16 9 53 11 12	lcdvsval	⊢ ( 𝜑 → ( ( ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ( ·𝑠 ‘ 𝐶 ) 𝐺 ) ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) )
55	1 2 3 4 23 6 7 9 11 12	lcdvbasecl	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) )
56	23 44 39 37 47 55	ringnegr	⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑋 ) ) )
57	43 54 56	3eqtrd	⊢ ( 𝜑 → ( ( ( ( invg ‘ ( Scalar ‘ 𝐶 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐶 ) ) ) ( ·𝑠 ‘ 𝐶 ) 𝐺 ) ‘ 𝑋 ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑋 ) ) )
58	57	oveq2d	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) ( +g ‘ 𝑅 ) ( ( ( ( invg ‘ ( Scalar ‘ 𝐶 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐶 ) ) ) ( ·𝑠 ‘ 𝐶 ) 𝐺 ) ‘ 𝑋 ) ) = ( ( 𝐹 ‘ 𝑋 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑋 ) ) ) )
59	1 2 3 4 23 6 7 9 10 12	lcdvbasecl	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) )
60	23 22 37 5	grpsubval	⊢ ( ( ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑋 ) 𝑆 ( 𝐺 ‘ 𝑋 ) ) = ( ( 𝐹 ‘ 𝑋 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑋 ) ) ) )
61	59 55 60	syl2anc	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) 𝑆 ( 𝐺 ‘ 𝑋 ) ) = ( ( 𝐹 ‘ 𝑋 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑋 ) ) ) )
62	58 61	eqtr4d	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) ( +g ‘ 𝑅 ) ( ( ( ( invg ‘ ( Scalar ‘ 𝐶 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐶 ) ) ) ( ·𝑠 ‘ 𝐶 ) 𝐺 ) ‘ 𝑋 ) ) = ( ( 𝐹 ‘ 𝑋 ) 𝑆 ( 𝐺 ‘ 𝑋 ) ) )
63	21 36 62	3eqtrd	⊢ ( 𝜑 → ( ( 𝐹 − 𝐺 ) ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑋 ) 𝑆 ( 𝐺 ‘ 𝑋 ) ) )