Metamath Proof Explorer

Theorem hdmapval3N

Description: Value of map from vectors to functionals at arguments not colinear with the reference vector E . (Contributed by NM, 17-May-2015) (New usage is discouraged.)

Ref Expression
Hypotheses hdmapval3.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hdmapval3.e ⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
hdmapval3.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmapval3.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
hdmapval3.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
hdmapval3.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
hdmapval3.d ⊢ 𝐷 = ( Base ‘ 𝐶 )
hdmapval3.j ⊢ 𝐽 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapval3.i ⊢ 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
hdmapval3.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapval3.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
hdmapval3.te ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑇 } ) ≠ ( 𝑁 ‘ { 𝐸 } ) )
hdmapval3.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
Assertion hdmapval3N ( 𝜑 → ( 𝑆 ‘ 𝑇 ) = ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑇 ⟩ ) )

Proof

Step Hyp Ref Expression
1 hdmapval3.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmapval3.e ⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
3 hdmapval3.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 hdmapval3.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 hdmapval3.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
6 hdmapval3.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
7 hdmapval3.d ⊢ 𝐷 = ( Base ‘ 𝐶 )
8 hdmapval3.j ⊢ 𝐽 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
9 hdmapval3.i ⊢ 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
10 hdmapval3.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
11 hdmapval3.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12 hdmapval3.te ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑇 } ) ≠ ( 𝑁 ‘ { 𝐸 } ) )
13 hdmapval3.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
14 fveq2 ⊢ ( 𝑇 = ( 0g ‘ 𝑈 ) → ( 𝑆 ‘ 𝑇 ) = ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) )
15 oteq3 ⊢ ( 𝑇 = ( 0g ‘ 𝑈 ) → ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑇 ⟩ = ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , ( 0g ‘ 𝑈 ) ⟩ )
16 15 fveq2d ⊢ ( 𝑇 = ( 0g ‘ 𝑈 ) → ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑇 ⟩ ) = ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , ( 0g ‘ 𝑈 ) ⟩ ) )
17 14 16 eqeq12d ⊢ ( 𝑇 = ( 0g ‘ 𝑈 ) → ( ( 𝑆 ‘ 𝑇 ) = ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑇 ⟩ ) ↔ ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) = ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , ( 0g ‘ 𝑈 ) ⟩ ) ) )
18 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
19 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
20 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
21 1 18 19 3 4 20 2 11 dvheveccl ⊢ ( 𝜑 → 𝐸 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
22 21 eldifad ⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
23 1 3 4 5 11 22 13 dvh3dim ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑉 ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) → ∃ 𝑥 ∈ 𝑉 ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) )
25 simp1l ⊢ ( ( ( 𝜑 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) ∧ 𝑥 ∈ 𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → 𝜑 )
26 25 11 syl ⊢ ( ( ( 𝜑 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) ∧ 𝑥 ∈ 𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
27 25 12 syl ⊢ ( ( ( 𝜑 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) ∧ 𝑥 ∈ 𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ( 𝑁 ‘ { 𝑇 } ) ≠ ( 𝑁 ‘ { 𝐸 } ) )
28 25 13 syl ⊢ ( ( ( 𝜑 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) ∧ 𝑥 ∈ 𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → 𝑇 ∈ 𝑉 )
29 simp1r ⊢ ( ( ( 𝜑 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) ∧ 𝑥 ∈ 𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → 𝑇 ≠ ( 0g ‘ 𝑈 ) )
30 eldifsn ⊢ ( 𝑇 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) ↔ ( 𝑇 ∈ 𝑉 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) )
31 28 29 30 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) ∧ 𝑥 ∈ 𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → 𝑇 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
32 simp2 ⊢ ( ( ( 𝜑 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) ∧ 𝑥 ∈ 𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → 𝑥 ∈ 𝑉 )
33 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) ∧ 𝑥 ∈ 𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) )
34 1 2 3 4 5 6 7 8 9 10 26 27 31 32 33 hdmapval3lemN ⊢ ( ( ( 𝜑 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) ∧ 𝑥 ∈ 𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ) → ( 𝑆 ‘ 𝑇 ) = ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑇 ⟩ ) )
35 34 rexlimdv3a ⊢ ( ( 𝜑 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) → ( ∃ 𝑥 ∈ 𝑉 ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) → ( 𝑆 ‘ 𝑇 ) = ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑇 ⟩ ) ) )
36 24 35 mpd ⊢ ( ( 𝜑 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝑆 ‘ 𝑇 ) = ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑇 ⟩ ) )
37 eqid ⊢ ( 0g ‘ 𝐶 ) = ( 0g ‘ 𝐶 )
38 1 3 20 6 37 10 11 hdmapval0 ⊢ ( 𝜑 → ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) = ( 0g ‘ 𝐶 ) )
39 1 3 4 20 6 7 37 8 11 21 hvmapcl2 ⊢ ( 𝜑 → ( 𝐽 ‘ 𝐸 ) ∈ ( 𝐷 ∖ { ( 0g ‘ 𝐶 ) } ) )
40 39 eldifad ⊢ ( 𝜑 → ( 𝐽 ‘ 𝐸 ) ∈ 𝐷 )
41 1 3 4 20 6 7 37 9 11 40 22 hdmap1val0 ⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , ( 0g ‘ 𝑈 ) ⟩ ) = ( 0g ‘ 𝐶 ) )
42 38 41 eqtr4d ⊢ ( 𝜑 → ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) = ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , ( 0g ‘ 𝑈 ) ⟩ ) )
43 17 36 42 pm2.61ne ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑇 ) = ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑇 ⟩ ) )