Metamath Proof Explorer

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