Metamath Proof Explorer


Theorem hdmapip1

Description: Construct a proportional vector Y whose inner product with the original X equals one. (Contributed by NM, 13-Jun-2015)

Ref Expression
Hypotheses hdmapip1.h 𝐻 = ( LHyp ‘ 𝐾 )
hdmapip1.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmapip1.v 𝑉 = ( Base ‘ 𝑈 )
hdmapip1.t · = ( ·𝑠𝑈 )
hdmapip1.o 0 = ( 0g𝑈 )
hdmapip1.r 𝑅 = ( Scalar ‘ 𝑈 )
hdmapip1.i 1 = ( 1r𝑅 )
hdmapip1.n 𝑁 = ( invr𝑅 )
hdmapip1.s 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapip1.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
hdmapip1.x ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
hdmapip1.y 𝑌 = ( ( 𝑁 ‘ ( ( 𝑆𝑋 ) ‘ 𝑋 ) ) · 𝑋 )
Assertion hdmapip1 ( 𝜑 → ( ( 𝑆𝑋 ) ‘ 𝑌 ) = 1 )

Proof

Step Hyp Ref Expression
1 hdmapip1.h 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmapip1.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hdmapip1.v 𝑉 = ( Base ‘ 𝑈 )
4 hdmapip1.t · = ( ·𝑠𝑈 )
5 hdmapip1.o 0 = ( 0g𝑈 )
6 hdmapip1.r 𝑅 = ( Scalar ‘ 𝑈 )
7 hdmapip1.i 1 = ( 1r𝑅 )
8 hdmapip1.n 𝑁 = ( invr𝑅 )
9 hdmapip1.s 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
10 hdmapip1.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
11 hdmapip1.x ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
12 hdmapip1.y 𝑌 = ( ( 𝑁 ‘ ( ( 𝑆𝑋 ) ‘ 𝑋 ) ) · 𝑋 )
13 12 fveq2i ( ( 𝑆𝑋 ) ‘ 𝑌 ) = ( ( 𝑆𝑋 ) ‘ ( ( 𝑁 ‘ ( ( 𝑆𝑋 ) ‘ 𝑋 ) ) · 𝑋 ) )
14 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
15 eqid ( .r𝑅 ) = ( .r𝑅 )
16 11 eldifad ( 𝜑𝑋𝑉 )
17 1 2 10 dvhlvec ( 𝜑𝑈 ∈ LVec )
18 6 lvecdrng ( 𝑈 ∈ LVec → 𝑅 ∈ DivRing )
19 17 18 syl ( 𝜑𝑅 ∈ DivRing )
20 1 2 3 6 14 9 10 16 16 hdmapipcl ( 𝜑 → ( ( 𝑆𝑋 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) )
21 eldifsni ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) → 𝑋0 )
22 11 21 syl ( 𝜑𝑋0 )
23 eqid ( 0g𝑅 ) = ( 0g𝑅 )
24 1 2 3 5 6 23 9 10 16 hdmapip0 ( 𝜑 → ( ( ( 𝑆𝑋 ) ‘ 𝑋 ) = ( 0g𝑅 ) ↔ 𝑋 = 0 ) )
25 24 necon3bid ( 𝜑 → ( ( ( 𝑆𝑋 ) ‘ 𝑋 ) ≠ ( 0g𝑅 ) ↔ 𝑋0 ) )
26 22 25 mpbird ( 𝜑 → ( ( 𝑆𝑋 ) ‘ 𝑋 ) ≠ ( 0g𝑅 ) )
27 14 23 8 drnginvrcl ( ( 𝑅 ∈ DivRing ∧ ( ( 𝑆𝑋 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑆𝑋 ) ‘ 𝑋 ) ≠ ( 0g𝑅 ) ) → ( 𝑁 ‘ ( ( 𝑆𝑋 ) ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑅 ) )
28 19 20 26 27 syl3anc ( 𝜑 → ( 𝑁 ‘ ( ( 𝑆𝑋 ) ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑅 ) )
29 1 2 3 4 6 14 15 9 10 16 16 28 hdmaplnm1 ( 𝜑 → ( ( 𝑆𝑋 ) ‘ ( ( 𝑁 ‘ ( ( 𝑆𝑋 ) ‘ 𝑋 ) ) · 𝑋 ) ) = ( ( 𝑁 ‘ ( ( 𝑆𝑋 ) ‘ 𝑋 ) ) ( .r𝑅 ) ( ( 𝑆𝑋 ) ‘ 𝑋 ) ) )
30 14 23 15 7 8 drnginvrl ( ( 𝑅 ∈ DivRing ∧ ( ( 𝑆𝑋 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑆𝑋 ) ‘ 𝑋 ) ≠ ( 0g𝑅 ) ) → ( ( 𝑁 ‘ ( ( 𝑆𝑋 ) ‘ 𝑋 ) ) ( .r𝑅 ) ( ( 𝑆𝑋 ) ‘ 𝑋 ) ) = 1 )
31 19 20 26 30 syl3anc ( 𝜑 → ( ( 𝑁 ‘ ( ( 𝑆𝑋 ) ‘ 𝑋 ) ) ( .r𝑅 ) ( ( 𝑆𝑋 ) ‘ 𝑋 ) ) = 1 )
32 29 31 eqtrd ( 𝜑 → ( ( 𝑆𝑋 ) ‘ ( ( 𝑁 ‘ ( ( 𝑆𝑋 ) ‘ 𝑋 ) ) · 𝑋 ) ) = 1 )
33 13 32 syl5eq ( 𝜑 → ( ( 𝑆𝑋 ) ‘ 𝑌 ) = 1 )