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