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 ↾ 𝑇 ) ⟩ = 00 = ⟨ ( 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 ↾ 𝑇 ) ⟩ = 00 = ⟨ ( 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 } ) )