Metamath Proof Explorer

Theorem ldualvsub

Description: The value of vector subtraction in the dual of a vector space. (Contributed by NM, 27-Feb-2015)

Ref Expression
Hypotheses ldualvsub.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
ldualvsub.n ⊢ 𝑁 = ( invg ‘ 𝑅 )
ldualvsub.u ⊢ 1 = ( 1r ‘ 𝑅 )
ldualvsub.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
ldualvsub.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
ldualvsub.p ⊢ + = ( +g ‘ 𝐷 )
ldualvsub.t ⊢ · = ( ·𝑠 ‘ 𝐷 )
ldualvsub.m ⊢ − = ( -g ‘ 𝐷 )
ldualvsub.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
ldualvsub.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
ldualvsub.h ⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
Assertion ldualvsub ( 𝜑 → ( 𝐺 − 𝐻 ) = ( 𝐺 + ( ( 𝑁 ‘ 1 ) · 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 ldualvsub.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
2 ldualvsub.n ⊢ 𝑁 = ( invg ‘ 𝑅 )
3 ldualvsub.u ⊢ 1 = ( 1r ‘ 𝑅 )
4 ldualvsub.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
5 ldualvsub.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
6 ldualvsub.p ⊢ + = ( +g ‘ 𝐷 )
7 ldualvsub.t ⊢ · = ( ·𝑠 ‘ 𝐷 )
8 ldualvsub.m ⊢ − = ( -g ‘ 𝐷 )
9 ldualvsub.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
10 ldualvsub.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
11 ldualvsub.h ⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
12 5 9 lduallmod ⊢ ( 𝜑 → 𝐷 ∈ LMod )
13 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
14 4 5 13 9 10 ldualelvbase ⊢ ( 𝜑 → 𝐺 ∈ ( Base ‘ 𝐷 ) )
15 4 5 13 9 11 ldualelvbase ⊢ ( 𝜑 → 𝐻 ∈ ( Base ‘ 𝐷 ) )
16 eqid ⊢ ( Scalar ‘ 𝐷 ) = ( Scalar ‘ 𝐷 )
17 eqid ⊢ ( invg ‘ ( Scalar ‘ 𝐷 ) ) = ( invg ‘ ( Scalar ‘ 𝐷 ) )
18 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝐷 ) ) = ( 1r ‘ ( Scalar ‘ 𝐷 ) )
19 13 6 8 16 7 17 18 lmodvsubval2 ⊢ ( ( 𝐷 ∈ LMod ∧ 𝐺 ∈ ( Base ‘ 𝐷 ) ∧ 𝐻 ∈ ( Base ‘ 𝐷 ) ) → ( 𝐺 − 𝐻 ) = ( 𝐺 + ( ( ( invg ‘ ( Scalar ‘ 𝐷 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐷 ) ) ) · 𝐻 ) ) )
20 12 14 15 19 syl3anc ⊢ ( 𝜑 → ( 𝐺 − 𝐻 ) = ( 𝐺 + ( ( ( invg ‘ ( Scalar ‘ 𝐷 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐷 ) ) ) · 𝐻 ) ) )
21 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
22 21 2 opprneg ⊢ 𝑁 = ( invg ‘ ( oppr ‘ 𝑅 ) )
23 1 21 5 16 9 ldualsca ⊢ ( 𝜑 → ( Scalar ‘ 𝐷 ) = ( oppr ‘ 𝑅 ) )
24 23 fveq2d ⊢ ( 𝜑 → ( invg ‘ ( Scalar ‘ 𝐷 ) ) = ( invg ‘ ( oppr ‘ 𝑅 ) ) )
25 22 24 eqtr4id ⊢ ( 𝜑 → 𝑁 = ( invg ‘ ( Scalar ‘ 𝐷 ) ) )
26 21 3 oppr1 ⊢ 1 = ( 1r ‘ ( oppr ‘ 𝑅 ) )
27 23 fveq2d ⊢ ( 𝜑 → ( 1r ‘ ( Scalar ‘ 𝐷 ) ) = ( 1r ‘ ( oppr ‘ 𝑅 ) ) )
28 26 27 eqtr4id ⊢ ( 𝜑 → 1 = ( 1r ‘ ( Scalar ‘ 𝐷 ) ) )
29 25 28 fveq12d ⊢ ( 𝜑 → ( 𝑁 ‘ 1 ) = ( ( invg ‘ ( Scalar ‘ 𝐷 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐷 ) ) ) )
30 29 oveq1d ⊢ ( 𝜑 → ( ( 𝑁 ‘ 1 ) · 𝐻 ) = ( ( ( invg ‘ ( Scalar ‘ 𝐷 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐷 ) ) ) · 𝐻 ) )
31 30 oveq2d ⊢ ( 𝜑 → ( 𝐺 + ( ( 𝑁 ‘ 1 ) · 𝐻 ) ) = ( 𝐺 + ( ( ( invg ‘ ( Scalar ‘ 𝐷 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐷 ) ) ) · 𝐻 ) ) )
32 20 31 eqtr4d ⊢ ( 𝜑 → ( 𝐺 − 𝐻 ) = ( 𝐺 + ( ( 𝑁 ‘ 1 ) · 𝐻 ) ) )