Step | Hyp | Ref
| Expression |
1 | | hdmap14lem1.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
2 | | hdmap14lem1.c |
. . . . . 6
⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) |
3 | | hdmap14lem1.k |
. . . . . 6
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
4 | 1, 2, 3 | lcdlmod 39614 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ LMod) |
5 | | hdmap14lem2.p |
. . . . . 6
⊢ 𝑃 = (Scalar‘𝐶) |
6 | | hdmap14lem2.a |
. . . . . 6
⊢ 𝐴 = (Base‘𝑃) |
7 | | hdmap14lem2.q |
. . . . . 6
⊢ 𝑄 = (0g‘𝑃) |
8 | 5, 6, 7 | lmod0cl 20159 |
. . . . 5
⊢ (𝐶 ∈ LMod → 𝑄 ∈ 𝐴) |
9 | 4, 8 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑄 ∈ 𝐴) |
10 | | hdmap14lem1.u |
. . . . . . 7
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
11 | | hdmap14lem1.v |
. . . . . . 7
⊢ 𝑉 = (Base‘𝑈) |
12 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘𝐶) =
(Base‘𝐶) |
13 | | hdmap14lem1.s |
. . . . . . 7
⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) |
14 | | hdmap14lem3.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) |
15 | 14 | eldifad 3898 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
16 | 1, 10, 11, 2, 12, 13, 3, 15 | hdmapcl 39852 |
. . . . . 6
⊢ (𝜑 → (𝑆‘𝑋) ∈ (Base‘𝐶)) |
17 | | hdmap14lem2.e |
. . . . . . 7
⊢ ∙ = (
·𝑠 ‘𝐶) |
18 | | eqid 2738 |
. . . . . . 7
⊢
(0g‘𝐶) = (0g‘𝐶) |
19 | 12, 5, 17, 7, 18 | lmod0vs 20166 |
. . . . . 6
⊢ ((𝐶 ∈ LMod ∧ (𝑆‘𝑋) ∈ (Base‘𝐶)) → (𝑄 ∙ (𝑆‘𝑋)) = (0g‘𝐶)) |
20 | 4, 16, 19 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝑄 ∙ (𝑆‘𝑋)) = (0g‘𝐶)) |
21 | 20 | eqcomd 2744 |
. . . 4
⊢ (𝜑 → (0g‘𝐶) = (𝑄 ∙ (𝑆‘𝑋))) |
22 | | oveq1 7274 |
. . . . 5
⊢ (𝑔 = 𝑄 → (𝑔 ∙ (𝑆‘𝑋)) = (𝑄 ∙ (𝑆‘𝑋))) |
23 | 22 | rspceeqv 3574 |
. . . 4
⊢ ((𝑄 ∈ 𝐴 ∧ (0g‘𝐶) = (𝑄 ∙ (𝑆‘𝑋))) → ∃𝑔 ∈ 𝐴 (0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋))) |
24 | 9, 21, 23 | syl2anc 584 |
. . 3
⊢ (𝜑 → ∃𝑔 ∈ 𝐴 (0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋))) |
25 | | hdmap14lem3.o |
. . . . . . . . . . 11
⊢ 0 =
(0g‘𝑈) |
26 | 1, 10, 11, 25, 2, 18, 12, 13, 3, 14 | hdmapnzcl 39867 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆‘𝑋) ∈ ((Base‘𝐶) ∖ {(0g‘𝐶)})) |
27 | | eldifsni 4723 |
. . . . . . . . . 10
⊢ ((𝑆‘𝑋) ∈ ((Base‘𝐶) ∖ {(0g‘𝐶)}) → (𝑆‘𝑋) ≠ (0g‘𝐶)) |
28 | 26, 27 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆‘𝑋) ≠ (0g‘𝐶)) |
29 | 28 | neneqd 2948 |
. . . . . . . 8
⊢ (𝜑 → ¬ (𝑆‘𝑋) = (0g‘𝐶)) |
30 | 29 | 3ad2ant1 1132 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → ¬ (𝑆‘𝑋) = (0g‘𝐶)) |
31 | | simp3l 1200 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → (0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋))) |
32 | 31 | eqcomd 2744 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → (𝑔 ∙ (𝑆‘𝑋)) = (0g‘𝐶)) |
33 | 1, 2, 3 | lcdlvec 39613 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ LVec) |
34 | 33 | 3ad2ant1 1132 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → 𝐶 ∈ LVec) |
35 | | simp2l 1198 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → 𝑔 ∈ 𝐴) |
36 | 16 | 3ad2ant1 1132 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → (𝑆‘𝑋) ∈ (Base‘𝐶)) |
37 | 12, 17, 5, 6, 7, 18,
34, 35, 36 | lvecvs0or 20380 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → ((𝑔 ∙ (𝑆‘𝑋)) = (0g‘𝐶) ↔ (𝑔 = 𝑄 ∨ (𝑆‘𝑋) = (0g‘𝐶)))) |
38 | 32, 37 | mpbid 231 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → (𝑔 = 𝑄 ∨ (𝑆‘𝑋) = (0g‘𝐶))) |
39 | 38 | orcomd 868 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → ((𝑆‘𝑋) = (0g‘𝐶) ∨ 𝑔 = 𝑄)) |
40 | 39 | ord 861 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → (¬ (𝑆‘𝑋) = (0g‘𝐶) → 𝑔 = 𝑄)) |
41 | 30, 40 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → 𝑔 = 𝑄) |
42 | | simp3r 1201 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋))) |
43 | 42 | eqcomd 2744 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → (ℎ ∙ (𝑆‘𝑋)) = (0g‘𝐶)) |
44 | | simp2r 1199 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → ℎ ∈ 𝐴) |
45 | 12, 17, 5, 6, 7, 18,
34, 44, 36 | lvecvs0or 20380 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → ((ℎ ∙ (𝑆‘𝑋)) = (0g‘𝐶) ↔ (ℎ = 𝑄 ∨ (𝑆‘𝑋) = (0g‘𝐶)))) |
46 | 43, 45 | mpbid 231 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → (ℎ = 𝑄 ∨ (𝑆‘𝑋) = (0g‘𝐶))) |
47 | 46 | orcomd 868 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → ((𝑆‘𝑋) = (0g‘𝐶) ∨ ℎ = 𝑄)) |
48 | 47 | ord 861 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → (¬ (𝑆‘𝑋) = (0g‘𝐶) → ℎ = 𝑄)) |
49 | 30, 48 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → ℎ = 𝑄) |
50 | 41, 49 | eqtr4d 2781 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) → 𝑔 = ℎ) |
51 | 50 | 3exp 1118 |
. . . 4
⊢ (𝜑 → ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) → (((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋))) → 𝑔 = ℎ))) |
52 | 51 | ralrimivv 3114 |
. . 3
⊢ (𝜑 → ∀𝑔 ∈ 𝐴 ∀ℎ ∈ 𝐴 (((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋))) → 𝑔 = ℎ)) |
53 | | oveq1 7274 |
. . . . 5
⊢ (𝑔 = ℎ → (𝑔 ∙ (𝑆‘𝑋)) = (ℎ ∙ (𝑆‘𝑋))) |
54 | 53 | eqeq2d 2749 |
. . . 4
⊢ (𝑔 = ℎ → ((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ↔ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋)))) |
55 | 54 | reu4 3665 |
. . 3
⊢
(∃!𝑔 ∈
𝐴
(0g‘𝐶) =
(𝑔 ∙ (𝑆‘𝑋)) ↔ (∃𝑔 ∈ 𝐴 (0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ ∀𝑔 ∈ 𝐴 ∀ℎ ∈ 𝐴 (((0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)) ∧ (0g‘𝐶) = (ℎ ∙ (𝑆‘𝑋))) → 𝑔 = ℎ))) |
56 | 24, 52, 55 | sylanbrc 583 |
. 2
⊢ (𝜑 → ∃!𝑔 ∈ 𝐴 (0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋))) |
57 | | hdmap14lem6.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹 = 𝑍) |
58 | 57 | oveq1d 7282 |
. . . . . . 7
⊢ (𝜑 → (𝐹 · 𝑋) = (𝑍 · 𝑋)) |
59 | 1, 10, 3 | dvhlmod 39132 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ LMod) |
60 | | hdmap14lem1.r |
. . . . . . . . 9
⊢ 𝑅 = (Scalar‘𝑈) |
61 | | hdmap14lem1.t |
. . . . . . . . 9
⊢ · = (
·𝑠 ‘𝑈) |
62 | | hdmap14lem1.z |
. . . . . . . . 9
⊢ 𝑍 = (0g‘𝑅) |
63 | 11, 60, 61, 62, 25 | lmod0vs 20166 |
. . . . . . . 8
⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑍 · 𝑋) = 0 ) |
64 | 59, 15, 63 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝑍 · 𝑋) = 0 ) |
65 | 58, 64 | eqtrd 2778 |
. . . . . 6
⊢ (𝜑 → (𝐹 · 𝑋) = 0 ) |
66 | 65 | fveq2d 6770 |
. . . . 5
⊢ (𝜑 → (𝑆‘(𝐹 · 𝑋)) = (𝑆‘ 0 )) |
67 | 1, 10, 25, 2, 18, 13, 3 | hdmapval0 39855 |
. . . . 5
⊢ (𝜑 → (𝑆‘ 0 ) =
(0g‘𝐶)) |
68 | 66, 67 | eqtrd 2778 |
. . . 4
⊢ (𝜑 → (𝑆‘(𝐹 · 𝑋)) = (0g‘𝐶)) |
69 | 68 | eqeq1d 2740 |
. . 3
⊢ (𝜑 → ((𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)) ↔ (0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)))) |
70 | 69 | reubidv 3321 |
. 2
⊢ (𝜑 → (∃!𝑔 ∈ 𝐴 (𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)) ↔ ∃!𝑔 ∈ 𝐴 (0g‘𝐶) = (𝑔 ∙ (𝑆‘𝑋)))) |
71 | 56, 70 | mpbird 256 |
1
⊢ (𝜑 → ∃!𝑔 ∈ 𝐴 (𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋))) |