Metamath Proof Explorer

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 rngnegr ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) ( .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 ⊢ ( 𝜑 → ( ( 𝐹 − 𝐺 ) ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑋 ) 𝑆 ( 𝐺 ‘ 𝑋 ) ) )