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 ) |