Metamath Proof Explorer

Theorem lcdvsub

Description: The value of vector subtraction in the closed kernel dual space. (Contributed by NM, 22-Mar-2015)

Ref Expression
Hypotheses lcdvsub.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
lcdvsub.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lcdvsub.s ⊢ 𝑆 = ( Scalar ‘ 𝑈 )
lcdvsub.n ⊢ 𝑁 = ( invg ‘ 𝑆 )
lcdvsub.e ⊢ 1 = ( 1r ‘ 𝑆 )
lcdvsub.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
lcdvsub.v ⊢ 𝑉 = ( Base ‘ 𝐶 )
lcdvsub.p ⊢ + = ( +g ‘ 𝐶 )
lcdvsub.t ⊢ · = ( ·𝑠 ‘ 𝐶 )
lcdvsub.m ⊢ − = ( -g ‘ 𝐶 )
lcdvsub.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
lcdvsub.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
lcdvsub.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
Assertion lcdvsub ( 𝜑 → ( 𝐹 − 𝐺 ) = ( 𝐹 + ( ( 𝑁 ‘ 1 ) · 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 lcdvsub.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 lcdvsub.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 lcdvsub.s ⊢ 𝑆 = ( Scalar ‘ 𝑈 )
4 lcdvsub.n ⊢ 𝑁 = ( invg ‘ 𝑆 )
5 lcdvsub.e ⊢ 1 = ( 1r ‘ 𝑆 )
6 lcdvsub.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
7 lcdvsub.v ⊢ 𝑉 = ( Base ‘ 𝐶 )
8 lcdvsub.p ⊢ + = ( +g ‘ 𝐶 )
9 lcdvsub.t ⊢ · = ( ·𝑠 ‘ 𝐶 )
10 lcdvsub.m ⊢ − = ( -g ‘ 𝐶 )
11 lcdvsub.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12 lcdvsub.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
13 lcdvsub.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
14 1 6 11 lcdlmod ⊢ ( 𝜑 → 𝐶 ∈ LMod )
15 eqid ⊢ ( Scalar ‘ 𝐶 ) = ( Scalar ‘ 𝐶 )
16 eqid ⊢ ( invg ‘ ( Scalar ‘ 𝐶 ) ) = ( invg ‘ ( Scalar ‘ 𝐶 ) )
17 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝐶 ) ) = ( 1r ‘ ( Scalar ‘ 𝐶 ) )
18 7 8 10 15 9 16 17 lmodvsubval2 ⊢ ( ( 𝐶 ∈ LMod ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) → ( 𝐹 − 𝐺 ) = ( 𝐹 + ( ( ( invg ‘ ( Scalar ‘ 𝐶 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐶 ) ) ) · 𝐺 ) ) )
19 14 12 13 18 syl3anc ⊢ ( 𝜑 → ( 𝐹 − 𝐺 ) = ( 𝐹 + ( ( ( invg ‘ ( Scalar ‘ 𝐶 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐶 ) ) ) · 𝐺 ) ) )
20 eqid ⊢ ( oppr ‘ 𝑆 ) = ( oppr ‘ 𝑆 )
21 20 4 opprneg ⊢ 𝑁 = ( invg ‘ ( oppr ‘ 𝑆 ) )
22 1 2 3 20 6 15 11 lcdsca ⊢ ( 𝜑 → ( Scalar ‘ 𝐶 ) = ( oppr ‘ 𝑆 ) )
23 22 fveq2d ⊢ ( 𝜑 → ( invg ‘ ( Scalar ‘ 𝐶 ) ) = ( invg ‘ ( oppr ‘ 𝑆 ) ) )
24 21 23 eqtr4id ⊢ ( 𝜑 → 𝑁 = ( invg ‘ ( Scalar ‘ 𝐶 ) ) )
25 20 5 oppr1 ⊢ 1 = ( 1r ‘ ( oppr ‘ 𝑆 ) )
26 22 fveq2d ⊢ ( 𝜑 → ( 1r ‘ ( Scalar ‘ 𝐶 ) ) = ( 1r ‘ ( oppr ‘ 𝑆 ) ) )
27 25 26 eqtr4id ⊢ ( 𝜑 → 1 = ( 1r ‘ ( Scalar ‘ 𝐶 ) ) )
28 24 27 fveq12d ⊢ ( 𝜑 → ( 𝑁 ‘ 1 ) = ( ( invg ‘ ( Scalar ‘ 𝐶 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐶 ) ) ) )
29 28 oveq1d ⊢ ( 𝜑 → ( ( 𝑁 ‘ 1 ) · 𝐺 ) = ( ( ( invg ‘ ( Scalar ‘ 𝐶 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐶 ) ) ) · 𝐺 ) )
30 29 oveq2d ⊢ ( 𝜑 → ( 𝐹 + ( ( 𝑁 ‘ 1 ) · 𝐺 ) ) = ( 𝐹 + ( ( ( invg ‘ ( Scalar ‘ 𝐶 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝐶 ) ) ) · 𝐺 ) ) )
31 19 30 eqtr4d ⊢ ( 𝜑 → ( 𝐹 − 𝐺 ) = ( 𝐹 + ( ( 𝑁 ‘ 1 ) · 𝐺 ) ) )