Step | Hyp | Ref
| Expression |
1 | | hdmap14lem1.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
2 | | hdmap14lem1.c |
. . . . . 6
⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) |
3 | | hdmap14lem1.k |
. . . . . 6
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
4 | 1, 2, 3 | lcdlmod 35899 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ LMod) |
5 | | hdmap14lem2.p |
. . . . . 6
⊢ 𝑃 = (Scalar‘𝐶) |
6 | | hdmap14lem2.a |
. . . . . 6
⊢ 𝐴 = (Base‘𝑃) |
7 | | hdmap14lem2.q |
. . . . . 6
⊢ 𝑄 = (0g‘𝑃) |
8 | 5, 6, 7 | lmod0cl 18712 |
. . . . 5
⊢ (𝐶 ∈ LMod → 𝑄 ∈ 𝐴) |
9 | 4, 8 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑄 ∈ 𝐴) |
10 | | hdmap14lem1.u |
. . . . . . 7
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
11 | | hdmap14lem1.v |
. . . . . . 7
⊢ 𝑉 = (Base‘𝑈) |
12 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘𝐶) =
(Base‘𝐶) |
13 | | hdmap14lem1.s |
. . . . . . 7
⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) |
14 | | hdmap14lem3.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) |
15 | 14 | eldifad 3552 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
16 | 1, 10, 11, 2, 12, 13, 3, 15 | hdmapcl 36140 |
. . . . . 6
⊢ (𝜑 → (𝑆‘𝑋) ∈ (Base‘𝐶)) |
17 | | hdmap14lem2.e |
. . . . . . 7
⊢ ∙ = (
·𝑠 ‘𝐶) |
18 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝐶) = (0g‘𝐶) |
19 | 12, 5, 17, 7, 18 | lmod0vs 18719 |
. . . . . 6
⊢ ((𝐶 ∈ LMod ∧ (𝑆‘𝑋) ∈ (Base‘𝐶)) → (𝑄 ∙ (𝑆‘𝑋)) = (0g‘𝐶)) |
20 | 4, 16, 19 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝑄 ∙ (𝑆‘𝑋)) = (0g‘𝐶)) |
21 | 20 | eqcomd 2616 |
. . . 4
⊢ (𝜑 → (0g‘𝐶) = (𝑄 ∙ (𝑆‘𝑋))) |
22 | | oveq1 6556 |
. . . . . 6
⊢ (𝑔 = 𝑄 → (𝑔 ∙ (𝑆‘𝑋)) = (𝑄 ∙ (𝑆‘𝑋))) |
23 | 22 | eqeq2d 2620 |
. . . . 5
⊢ (𝑔 = 𝑄 → ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ↔ (0g‘𝐶) = (𝑄 ∙ (𝑆‘𝑋)))) |
24 | 23 | rspcev 3282 |
. . . 4
⊢ ((𝑄 ∈ 𝐴 ∧ (0g‘𝐶) = (𝑄 ∙ (𝑆‘𝑋))) → ∃𝑔 ∈ 𝐴 (0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋))) |
25 | 9, 21, 24 | syl2anc 691 |
. . 3
⊢ (𝜑 → ∃𝑔 ∈ 𝐴 (0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋))) |
26 | | hdmap14lem3.o |
. . . . . . . . . . 11
⊢ 0 =
(0g‘𝑈) |
27 | 1, 10, 11, 26, 2, 18, 12, 13, 3, 14 | hdmapnzcl 36155 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆‘𝑋) ∈ ((Base‘𝐶) ∖ {(0g‘𝐶)})) |
28 | | eldifsni 4261 |
. . . . . . . . . 10
⊢ ((𝑆‘𝑋) ∈ ((Base‘𝐶) ∖ {(0g‘𝐶)}) → (𝑆‘𝑋) ≠ (0g‘𝐶)) |
29 | 27, 28 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆‘𝑋) ≠ (0g‘𝐶)) |
30 | 29 | neneqd 2787 |
. . . . . . . 8
⊢ (𝜑 → ¬ (𝑆‘𝑋) = (0g‘𝐶)) |
31 | 30 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → ¬ (𝑆‘𝑋) = (0g‘𝐶)) |
32 | | simp3l 1082 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → (0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋))) |
33 | 32 | eqcomd 2616 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → (𝑔 ∙ (𝑆‘𝑋)) = (0g‘𝐶)) |
34 | 1, 2, 3 | lcdlvec 35898 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ LVec) |
35 | 34 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → 𝐶 ∈ LVec) |
36 | | simp2l 1080 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → 𝑔 ∈ 𝐴) |
37 | 16 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → (𝑆‘𝑋) ∈ (Base‘𝐶)) |
38 | 12, 17, 5, 6, 7, 18,
35, 36, 37 | lvecvs0or 18929 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → ((𝑔 ∙ (𝑆‘𝑋)) = (0g‘𝐶) ↔ (𝑔 = 𝑄 ∨ (𝑆‘𝑋) = (0g‘𝐶)))) |
39 | 33, 38 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → (𝑔 = 𝑄 ∨ (𝑆‘𝑋) = (0g‘𝐶))) |
40 | 39 | orcomd 402 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → ((𝑆‘𝑋) = (0g‘𝐶) ∨ 𝑔 = 𝑄)) |
41 | 40 | ord 391 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → (¬ (𝑆‘𝑋) = (0g‘𝐶) → 𝑔 = 𝑄)) |
42 | 31, 41 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → 𝑔 = 𝑄) |
43 | | simp3r 1083 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋))) |
44 | 43 | eqcomd 2616 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → (ℎ ∙ (𝑆‘𝑋)) = (0g‘𝐶)) |
45 | | simp2r 1081 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → ℎ ∈ 𝐴) |
46 | 12, 17, 5, 6, 7, 18,
35, 45, 37 | lvecvs0or 18929 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → ((ℎ ∙ (𝑆‘𝑋)) = (0g‘𝐶) ↔ (ℎ = 𝑄 ∨ (𝑆‘𝑋) = (0g‘𝐶)))) |
47 | 44, 46 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → (ℎ = 𝑄 ∨ (𝑆‘𝑋) = (0g‘𝐶))) |
48 | 47 | orcomd 402 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → ((𝑆‘𝑋) = (0g‘𝐶) ∨ ℎ = 𝑄)) |
49 | 48 | ord 391 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → (¬ (𝑆‘𝑋) = (0g‘𝐶) → ℎ = 𝑄)) |
50 | 31, 49 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → ℎ = 𝑄) |
51 | 42, 50 | eqtr4d 2647 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → 𝑔 = ℎ) |
52 | 51 | 3exp 1256 |
. . . 4
⊢ (𝜑 → ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) → (((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋))) → 𝑔 = ℎ))) |
53 | 52 | ralrimivv 2953 |
. . 3
⊢ (𝜑 → ∀𝑔 ∈ 𝐴 ∀ℎ ∈ 𝐴 (((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋))) → 𝑔 = ℎ)) |
54 | | oveq1 6556 |
. . . . 5
⊢ (𝑔 = ℎ → (𝑔 ∙ (𝑆‘𝑋)) = (ℎ ∙ (𝑆‘𝑋))) |
55 | 54 | eqeq2d 2620 |
. . . 4
⊢ (𝑔 = ℎ → ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ↔ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) |
56 | 55 | reu4 3367 |
. . 3
⊢
(∃!𝑔 ∈
𝐴
(0g‘𝐶) =
(𝑔 ∙ (𝑆‘𝑋)) ↔ (∃𝑔 ∈ 𝐴 (0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ ∀𝑔 ∈ 𝐴 ∀ℎ ∈ 𝐴 (((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋))) → 𝑔 = ℎ))) |
57 | 25, 53, 56 | sylanbrc 695 |
. 2
⊢ (𝜑 → ∃!𝑔 ∈ 𝐴 (0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋))) |
58 | | hdmap14lem6.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹 = 𝑍) |
59 | 58 | oveq1d 6564 |
. . . . . . 7
⊢ (𝜑 → (𝐹 · 𝑋) = (𝑍 · 𝑋)) |
60 | 1, 10, 3 | dvhlmod 35417 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ LMod) |
61 | | hdmap14lem1.r |
. . . . . . . . 9
⊢ 𝑅 = (Scalar‘𝑈) |
62 | | hdmap14lem1.t |
. . . . . . . . 9
⊢ · = (
·𝑠 ‘𝑈) |
63 | | hdmap14lem1.z |
. . . . . . . . 9
⊢ 𝑍 = (0g‘𝑅) |
64 | 11, 61, 62, 63, 26 | lmod0vs 18719 |
. . . . . . . 8
⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑍 · 𝑋) = 0 ) |
65 | 60, 15, 64 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝑍 · 𝑋) = 0 ) |
66 | 59, 65 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → (𝐹 · 𝑋) = 0 ) |
67 | 66 | fveq2d 6107 |
. . . . 5
⊢ (𝜑 → (𝑆‘(𝐹 · 𝑋)) = (𝑆‘ 0 )) |
68 | 1, 10, 26, 2, 18, 13, 3 | hdmapval0 36143 |
. . . . 5
⊢ (𝜑 → (𝑆‘ 0 ) =
(0g‘𝐶)) |
69 | 67, 68 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → (𝑆‘(𝐹 · 𝑋)) = (0g‘𝐶)) |
70 | 69 | eqeq1d 2612 |
. . 3
⊢ (𝜑 → ((𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)) ↔ (0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)))) |
71 | 70 | reubidv 3103 |
. 2
⊢ (𝜑 → (∃!𝑔 ∈ 𝐴 (𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)) ↔ ∃!𝑔 ∈ 𝐴 (0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)))) |
72 | 57, 71 | mpbird 246 |
1
⊢ (𝜑 → ∃!𝑔 ∈ 𝐴 (𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋))) |