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 eqtrid ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) ‘ 𝑌 ) = 1 )