Step |
Hyp |
Ref |
Expression |
1 |
|
hdmap12d.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
2 |
|
hdmap12d.u |
⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) |
3 |
|
hdmap12d.v |
⊢ 𝑉 = ( Base ‘ 𝑈 ) |
4 |
|
hdmap12d.s |
⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) |
5 |
|
hdmap12d.k |
⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
6 |
|
hdmap12d.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝑉 ) |
7 |
|
hdmap12d.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝑉 ) |
8 |
|
eqid |
⊢ ( -g ‘ 𝑈 ) = ( -g ‘ 𝑈 ) |
9 |
|
eqid |
⊢ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) |
10 |
|
eqid |
⊢ ( -g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( -g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) |
11 |
1 2 3 8 9 10 4 5 6 7
|
hdmapsub |
⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) ) = ( ( 𝑆 ‘ 𝑋 ) ( -g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑆 ‘ 𝑌 ) ) ) |
12 |
11
|
eqeq1d |
⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ ( ( 𝑆 ‘ 𝑋 ) ( -g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑆 ‘ 𝑌 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) |
13 |
|
eqid |
⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 ) |
14 |
|
eqid |
⊢ ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) |
15 |
1 2 5
|
dvhlmod |
⊢ ( 𝜑 → 𝑈 ∈ LMod ) |
16 |
3 8
|
lmodvsubcl |
⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) ∈ 𝑉 ) |
17 |
15 6 7 16
|
syl3anc |
⊢ ( 𝜑 → ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) ∈ 𝑉 ) |
18 |
1 2 3 13 9 14 4 5 17
|
hdmapeq0 |
⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) = ( 0g ‘ 𝑈 ) ) ) |
19 |
1 9 5
|
lcdlmod |
⊢ ( 𝜑 → ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ LMod ) |
20 |
|
lmodgrp |
⊢ ( ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ LMod → ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ Grp ) |
21 |
19 20
|
syl |
⊢ ( 𝜑 → ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ Grp ) |
22 |
|
eqid |
⊢ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) |
23 |
1 2 3 9 22 4 5 6
|
hdmapcl |
⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) |
24 |
1 2 3 9 22 4 5 7
|
hdmapcl |
⊢ ( 𝜑 → ( 𝑆 ‘ 𝑌 ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) |
25 |
22 14 10
|
grpsubeq0 |
⊢ ( ( ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ Grp ∧ ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ( 𝑆 ‘ 𝑌 ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( ( ( 𝑆 ‘ 𝑋 ) ( -g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑆 ‘ 𝑌 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ ( 𝑆 ‘ 𝑋 ) = ( 𝑆 ‘ 𝑌 ) ) ) |
26 |
21 23 24 25
|
syl3anc |
⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑋 ) ( -g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑆 ‘ 𝑌 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ ( 𝑆 ‘ 𝑋 ) = ( 𝑆 ‘ 𝑌 ) ) ) |
27 |
12 18 26
|
3bitr3rd |
⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) = ( 𝑆 ‘ 𝑌 ) ↔ ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) = ( 0g ‘ 𝑈 ) ) ) |
28 |
|
lmodgrp |
⊢ ( 𝑈 ∈ LMod → 𝑈 ∈ Grp ) |
29 |
15 28
|
syl |
⊢ ( 𝜑 → 𝑈 ∈ Grp ) |
30 |
3 13 8
|
grpsubeq0 |
⊢ ( ( 𝑈 ∈ Grp ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) = ( 0g ‘ 𝑈 ) ↔ 𝑋 = 𝑌 ) ) |
31 |
29 6 7 30
|
syl3anc |
⊢ ( 𝜑 → ( ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) = ( 0g ‘ 𝑈 ) ↔ 𝑋 = 𝑌 ) ) |
32 |
27 31
|
bitrd |
⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) = ( 𝑆 ‘ 𝑌 ) ↔ 𝑋 = 𝑌 ) ) |