Metamath Proof Explorer

Theorem dvheveccl

Description: Properties of a unit vector that we will use later as a convenient reference vector. This vector is called "e" in the remark after Lemma M of Crawley p. 121. line 17. See also dvhopN and dihpN . (Contributed by NM, 27-Mar-2015)

Ref Expression
Hypotheses dvheveccl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dvheveccl.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dvheveccl.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dvheveccl.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dvheveccl.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dvheveccl.z ⊢ 0 = ( 0g ‘ 𝑈 )
dvheveccl.e ⊢ 𝐸 = ⟨ ( I ↾ 𝐵 ) , ( I ↾ 𝑇 ) ⟩
dvheveccl.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion dvheveccl ( 𝜑 → 𝐸 ∈ ( 𝑉 ∖ { 0 } ) )

Proof

Step Hyp Ref Expression
1 dvheveccl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dvheveccl.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
3 dvheveccl.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 dvheveccl.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 dvheveccl.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
6 dvheveccl.z ⊢ 0 = ( 0g ‘ 𝑈 )
7 dvheveccl.e ⊢ 𝐸 = ⟨ ( I ↾ 𝐵 ) , ( I ↾ 𝑇 ) ⟩
8 dvheveccl.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 2 1 3 idltrn ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝐵 ) ∈ 𝑇 )
10 8 9 syl ⊢ ( 𝜑 → ( I ↾ 𝐵 ) ∈ 𝑇 )
11 eqid ⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
12 1 3 11 tendoidcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
13 8 12 syl ⊢ ( 𝜑 → ( I ↾ 𝑇 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
14 1 3 11 4 5 dvhelvbasei ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( I ↾ 𝐵 ) ∈ 𝑇 ∧ ( I ↾ 𝑇 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ⟨ ( I ↾ 𝐵 ) , ( I ↾ 𝑇 ) ⟩ ∈ 𝑉 )
15 8 10 13 14 syl12anc ⊢ ( 𝜑 → ⟨ ( I ↾ 𝐵 ) , ( I ↾ 𝑇 ) ⟩ ∈ 𝑉 )
16 eqid ⊢ ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
17 2 1 3 11 16 tendo1ne0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ≠ ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) )
18 8 17 syl ⊢ ( 𝜑 → ( I ↾ 𝑇 ) ≠ ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) )
19 2 1 3 4 6 16 dvh0g ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 = ⟨ ( I ↾ 𝐵 ) , ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) ⟩ )
20 8 19 syl ⊢ ( 𝜑 → 0 = ⟨ ( I ↾ 𝐵 ) , ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) ⟩ )
21 eqtr ⊢ ( ( ⟨ ( I ↾ 𝐵 ) , ( I ↾ 𝑇 ) ⟩ = 0 ∧ 0 = ⟨ ( I ↾ 𝐵 ) , ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) ⟩ ) → ⟨ ( I ↾ 𝐵 ) , ( I ↾ 𝑇 ) ⟩ = ⟨ ( I ↾ 𝐵 ) , ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) ⟩ )
22 opthg ⊢ ( ( ( I ↾ 𝐵 ) ∈ 𝑇 ∧ ( I ↾ 𝑇 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⟨ ( I ↾ 𝐵 ) , ( I ↾ 𝑇 ) ⟩ = ⟨ ( I ↾ 𝐵 ) , ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) ⟩ ↔ ( ( I ↾ 𝐵 ) = ( I ↾ 𝐵 ) ∧ ( I ↾ 𝑇 ) = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) ) ) )
23 10 13 22 syl2anc ⊢ ( 𝜑 → ( ⟨ ( I ↾ 𝐵 ) , ( I ↾ 𝑇 ) ⟩ = ⟨ ( I ↾ 𝐵 ) , ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) ⟩ ↔ ( ( I ↾ 𝐵 ) = ( I ↾ 𝐵 ) ∧ ( I ↾ 𝑇 ) = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) ) ) )
24 simpr ⊢ ( ( ( I ↾ 𝐵 ) = ( I ↾ 𝐵 ) ∧ ( I ↾ 𝑇 ) = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) ) → ( I ↾ 𝑇 ) = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) )
25 23 24 syl6bi ⊢ ( 𝜑 → ( ⟨ ( I ↾ 𝐵 ) , ( I ↾ 𝑇 ) ⟩ = ⟨ ( I ↾ 𝐵 ) , ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) ⟩ → ( I ↾ 𝑇 ) = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) ) )
26 21 25 syl5 ⊢ ( 𝜑 → ( ( ⟨ ( I ↾ 𝐵 ) , ( I ↾ 𝑇 ) ⟩ = 0 ∧ 0 = ⟨ ( I ↾ 𝐵 ) , ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) ⟩ ) → ( I ↾ 𝑇 ) = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) ) )
27 20 26 mpan2d ⊢ ( 𝜑 → ( ⟨ ( I ↾ 𝐵 ) , ( I ↾ 𝑇 ) ⟩ = 0 → ( I ↾ 𝑇 ) = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) ) )
28 27 necon3d ⊢ ( 𝜑 → ( ( I ↾ 𝑇 ) ≠ ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) → ⟨ ( I ↾ 𝐵 ) , ( I ↾ 𝑇 ) ⟩ ≠ 0 ) )
29 18 28 mpd ⊢ ( 𝜑 → ⟨ ( I ↾ 𝐵 ) , ( I ↾ 𝑇 ) ⟩ ≠ 0 )
30 eldifsn ⊢ ( ⟨ ( I ↾ 𝐵 ) , ( I ↾ 𝑇 ) ⟩ ∈ ( 𝑉 ∖ { 0 } ) ↔ ( ⟨ ( I ↾ 𝐵 ) , ( I ↾ 𝑇 ) ⟩ ∈ 𝑉 ∧ ⟨ ( I ↾ 𝐵 ) , ( I ↾ 𝑇 ) ⟩ ≠ 0 ) )
31 15 29 30 sylanbrc ⊢ ( 𝜑 → ⟨ ( I ↾ 𝐵 ) , ( I ↾ 𝑇 ) ⟩ ∈ ( 𝑉 ∖ { 0 } ) )
32 7 31 eqeltrid ⊢ ( 𝜑 → 𝐸 ∈ ( 𝑉 ∖ { 0 } ) )