Step | Hyp | Ref
| Expression |
1 | | hgmapval0.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
2 | | hgmapval0.u |
. . . 4
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
3 | | eqid 2738 |
. . . 4
⊢
(Base‘𝑈) =
(Base‘𝑈) |
4 | | eqid 2738 |
. . . 4
⊢
(0g‘𝑈) = (0g‘𝑈) |
5 | | hgmapval0.k |
. . . 4
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
6 | 1, 2, 3, 4, 5 | dvh1dim 39456 |
. . 3
⊢ (𝜑 → ∃𝑥 ∈ (Base‘𝑈)𝑥 ≠ (0g‘𝑈)) |
7 | | eqid 2738 |
. . . . . . . . 9
⊢
((LCDual‘𝐾)‘𝑊) = ((LCDual‘𝐾)‘𝑊) |
8 | | eqid 2738 |
. . . . . . . . 9
⊢
(0g‘((LCDual‘𝐾)‘𝑊)) =
(0g‘((LCDual‘𝐾)‘𝑊)) |
9 | | eqid 2738 |
. . . . . . . . 9
⊢
((HDMap‘𝐾)‘𝑊) = ((HDMap‘𝐾)‘𝑊) |
10 | 5 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑈)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
11 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑈)) → 𝑥 ∈ (Base‘𝑈)) |
12 | 1, 2, 3, 4, 7, 8, 9, 10, 11 | hdmapeq0 39858 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑈)) → ((((HDMap‘𝐾)‘𝑊)‘𝑥) = (0g‘((LCDual‘𝐾)‘𝑊)) ↔ 𝑥 = (0g‘𝑈))) |
13 | 12 | biimpd 228 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑈)) → ((((HDMap‘𝐾)‘𝑊)‘𝑥) = (0g‘((LCDual‘𝐾)‘𝑊)) → 𝑥 = (0g‘𝑈))) |
14 | 13 | necon3ad 2956 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑈)) → (𝑥 ≠ (0g‘𝑈) → ¬ (((HDMap‘𝐾)‘𝑊)‘𝑥) = (0g‘((LCDual‘𝐾)‘𝑊)))) |
15 | 14 | 3impia 1116 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑈) ∧ 𝑥 ≠ (0g‘𝑈)) → ¬ (((HDMap‘𝐾)‘𝑊)‘𝑥) = (0g‘((LCDual‘𝐾)‘𝑊))) |
16 | 1, 2, 5 | dvhlmod 39124 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ LMod) |
17 | | hgmapval0.r |
. . . . . . . . . . . . 13
⊢ 𝑅 = (Scalar‘𝑈) |
18 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢ (
·𝑠 ‘𝑈) = ( ·𝑠
‘𝑈) |
19 | | hgmapval0.o |
. . . . . . . . . . . . 13
⊢ 0 =
(0g‘𝑅) |
20 | 3, 17, 18, 19, 4 | lmod0vs 20156 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ LMod ∧ 𝑥 ∈ (Base‘𝑈)) → ( 0 (
·𝑠 ‘𝑈)𝑥) = (0g‘𝑈)) |
21 | 16, 20 | sylan 580 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑈)) → ( 0 (
·𝑠 ‘𝑈)𝑥) = (0g‘𝑈)) |
22 | 21 | fveq2d 6778 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑈)) → (((HDMap‘𝐾)‘𝑊)‘( 0 (
·𝑠 ‘𝑈)𝑥)) = (((HDMap‘𝐾)‘𝑊)‘(0g‘𝑈))) |
23 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
24 | | eqid 2738 |
. . . . . . . . . . 11
⊢ (
·𝑠 ‘((LCDual‘𝐾)‘𝑊)) = ( ·𝑠
‘((LCDual‘𝐾)‘𝑊)) |
25 | | hgmapval0.g |
. . . . . . . . . . 11
⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) |
26 | 17, 23, 19 | lmod0cl 20149 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∈ LMod → 0 ∈
(Base‘𝑅)) |
27 | 16, 26 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈ (Base‘𝑅)) |
28 | 27 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑈)) → 0 ∈ (Base‘𝑅)) |
29 | 1, 2, 3, 18, 17, 23, 7, 24, 9, 25, 10, 11, 28 | hgmapvs 39905 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑈)) → (((HDMap‘𝐾)‘𝑊)‘( 0 (
·𝑠 ‘𝑈)𝑥)) = ((𝐺‘ 0 )(
·𝑠 ‘((LCDual‘𝐾)‘𝑊))(((HDMap‘𝐾)‘𝑊)‘𝑥))) |
30 | 1, 2, 4, 7, 8, 9, 5 | hdmapval0 39847 |
. . . . . . . . . . 11
⊢ (𝜑 → (((HDMap‘𝐾)‘𝑊)‘(0g‘𝑈)) =
(0g‘((LCDual‘𝐾)‘𝑊))) |
31 | 30 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑈)) → (((HDMap‘𝐾)‘𝑊)‘(0g‘𝑈)) =
(0g‘((LCDual‘𝐾)‘𝑊))) |
32 | 22, 29, 31 | 3eqtr3d 2786 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑈)) → ((𝐺‘ 0 )(
·𝑠 ‘((LCDual‘𝐾)‘𝑊))(((HDMap‘𝐾)‘𝑊)‘𝑥)) =
(0g‘((LCDual‘𝐾)‘𝑊))) |
33 | | eqid 2738 |
. . . . . . . . . 10
⊢
(Base‘((LCDual‘𝐾)‘𝑊)) = (Base‘((LCDual‘𝐾)‘𝑊)) |
34 | | eqid 2738 |
. . . . . . . . . 10
⊢
(Scalar‘((LCDual‘𝐾)‘𝑊)) = (Scalar‘((LCDual‘𝐾)‘𝑊)) |
35 | | eqid 2738 |
. . . . . . . . . 10
⊢
(Base‘(Scalar‘((LCDual‘𝐾)‘𝑊))) =
(Base‘(Scalar‘((LCDual‘𝐾)‘𝑊))) |
36 | | eqid 2738 |
. . . . . . . . . 10
⊢
(0g‘(Scalar‘((LCDual‘𝐾)‘𝑊))) =
(0g‘(Scalar‘((LCDual‘𝐾)‘𝑊))) |
37 | 1, 7, 5 | lcdlvec 39605 |
. . . . . . . . . . 11
⊢ (𝜑 → ((LCDual‘𝐾)‘𝑊) ∈ LVec) |
38 | 37 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑈)) → ((LCDual‘𝐾)‘𝑊) ∈ LVec) |
39 | 1, 2, 10 | dvhlmod 39124 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑈)) → 𝑈 ∈ LMod) |
40 | 39, 26 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑈)) → 0 ∈ (Base‘𝑅)) |
41 | 1, 2, 17, 23, 7, 34, 35, 25, 10, 40 | hgmapdcl 39904 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑈)) → (𝐺‘ 0 ) ∈
(Base‘(Scalar‘((LCDual‘𝐾)‘𝑊)))) |
42 | 1, 2, 3, 7, 33, 9,
10, 11 | hdmapcl 39844 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑈)) → (((HDMap‘𝐾)‘𝑊)‘𝑥) ∈ (Base‘((LCDual‘𝐾)‘𝑊))) |
43 | 33, 24, 34, 35, 36, 8, 38, 41, 42 | lvecvs0or 20370 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑈)) → (((𝐺‘ 0 )(
·𝑠 ‘((LCDual‘𝐾)‘𝑊))(((HDMap‘𝐾)‘𝑊)‘𝑥)) =
(0g‘((LCDual‘𝐾)‘𝑊)) ↔ ((𝐺‘ 0 ) =
(0g‘(Scalar‘((LCDual‘𝐾)‘𝑊))) ∨ (((HDMap‘𝐾)‘𝑊)‘𝑥) = (0g‘((LCDual‘𝐾)‘𝑊))))) |
44 | 32, 43 | mpbid 231 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑈)) → ((𝐺‘ 0 ) =
(0g‘(Scalar‘((LCDual‘𝐾)‘𝑊))) ∨ (((HDMap‘𝐾)‘𝑊)‘𝑥) = (0g‘((LCDual‘𝐾)‘𝑊)))) |
45 | 44 | orcomd 868 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑈)) → ((((HDMap‘𝐾)‘𝑊)‘𝑥) = (0g‘((LCDual‘𝐾)‘𝑊)) ∨ (𝐺‘ 0 ) =
(0g‘(Scalar‘((LCDual‘𝐾)‘𝑊))))) |
46 | 45 | ord 861 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑈)) → (¬ (((HDMap‘𝐾)‘𝑊)‘𝑥) = (0g‘((LCDual‘𝐾)‘𝑊)) → (𝐺‘ 0 ) =
(0g‘(Scalar‘((LCDual‘𝐾)‘𝑊))))) |
47 | 46 | 3adant3 1131 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑈) ∧ 𝑥 ≠ (0g‘𝑈)) → (¬ (((HDMap‘𝐾)‘𝑊)‘𝑥) = (0g‘((LCDual‘𝐾)‘𝑊)) → (𝐺‘ 0 ) =
(0g‘(Scalar‘((LCDual‘𝐾)‘𝑊))))) |
48 | 15, 47 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑈) ∧ 𝑥 ≠ (0g‘𝑈)) → (𝐺‘ 0 ) =
(0g‘(Scalar‘((LCDual‘𝐾)‘𝑊)))) |
49 | 48 | rexlimdv3a 3215 |
. . 3
⊢ (𝜑 → (∃𝑥 ∈ (Base‘𝑈)𝑥 ≠ (0g‘𝑈) → (𝐺‘ 0 ) =
(0g‘(Scalar‘((LCDual‘𝐾)‘𝑊))))) |
50 | 6, 49 | mpd 15 |
. 2
⊢ (𝜑 → (𝐺‘ 0 ) =
(0g‘(Scalar‘((LCDual‘𝐾)‘𝑊)))) |
51 | 1, 2, 17, 19, 7, 34, 36, 5 | lcd0 39622 |
. 2
⊢ (𝜑 →
(0g‘(Scalar‘((LCDual‘𝐾)‘𝑊))) = 0 ) |
52 | 50, 51 | eqtrd 2778 |
1
⊢ (𝜑 → (𝐺‘ 0 ) = 0 ) |