Proof of Theorem hdmapinvlem4
Step | Hyp | Ref
| Expression |
1 | | hdmapinvlem3.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
2 | | hdmapinvlem3.u |
. . . 4
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
3 | | hdmapinvlem3.v |
. . . 4
⊢ 𝑉 = (Base‘𝑈) |
4 | | hdmapinvlem3.m |
. . . 4
⊢ − =
(-g‘𝑈) |
5 | | hdmapinvlem3.r |
. . . 4
⊢ 𝑅 = (Scalar‘𝑈) |
6 | | eqid 2739 |
. . . 4
⊢
(-g‘𝑅) = (-g‘𝑅) |
7 | | hdmapinvlem3.s |
. . . 4
⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) |
8 | | hdmapinvlem3.k |
. . . 4
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
9 | 1, 2, 8 | dvhlmod 38780 |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ LMod) |
10 | | hdmapinvlem3.j |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ 𝐵) |
11 | | eqid 2739 |
. . . . . . 7
⊢
(Base‘𝐾) =
(Base‘𝐾) |
12 | | eqid 2739 |
. . . . . . 7
⊢
((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊) |
13 | | eqid 2739 |
. . . . . . 7
⊢
(0g‘𝑈) = (0g‘𝑈) |
14 | | hdmapinvlem3.e |
. . . . . . 7
⊢ 𝐸 = 〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑊))〉 |
15 | 1, 11, 12, 2, 3, 13, 14, 8 | dvheveccl 38782 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ (𝑉 ∖ {(0g‘𝑈)})) |
16 | 15 | eldifad 3865 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ 𝑉) |
17 | | hdmapinvlem3.q |
. . . . . 6
⊢ · = (
·𝑠 ‘𝑈) |
18 | | hdmapinvlem3.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
19 | 3, 5, 17, 18 | lmodvscl 19783 |
. . . . 5
⊢ ((𝑈 ∈ LMod ∧ 𝐽 ∈ 𝐵 ∧ 𝐸 ∈ 𝑉) → (𝐽 · 𝐸) ∈ 𝑉) |
20 | 9, 10, 16, 19 | syl3anc 1372 |
. . . 4
⊢ (𝜑 → (𝐽 · 𝐸) ∈ 𝑉) |
21 | 16 | snssd 4707 |
. . . . . 6
⊢ (𝜑 → {𝐸} ⊆ 𝑉) |
22 | | hdmapinvlem3.o |
. . . . . . 7
⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) |
23 | 1, 2, 3, 22 | dochssv 39025 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ {𝐸} ⊆ 𝑉) → (𝑂‘{𝐸}) ⊆ 𝑉) |
24 | 8, 21, 23 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝑂‘{𝐸}) ⊆ 𝑉) |
25 | | hdmapinvlem3.d |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ (𝑂‘{𝐸})) |
26 | 24, 25 | sseldd 3888 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
27 | | hdmapinvlem3.i |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ 𝐵) |
28 | 3, 5, 17, 18 | lmodvscl 19783 |
. . . . . 6
⊢ ((𝑈 ∈ LMod ∧ 𝐼 ∈ 𝐵 ∧ 𝐸 ∈ 𝑉) → (𝐼 · 𝐸) ∈ 𝑉) |
29 | 9, 27, 16, 28 | syl3anc 1372 |
. . . . 5
⊢ (𝜑 → (𝐼 · 𝐸) ∈ 𝑉) |
30 | | hdmapinvlem3.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸})) |
31 | 24, 30 | sseldd 3888 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
32 | | hdmapinvlem3.p |
. . . . . 6
⊢ + =
(+g‘𝑈) |
33 | 3, 32 | lmodvacl 19780 |
. . . . 5
⊢ ((𝑈 ∈ LMod ∧ (𝐼 · 𝐸) ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝐼 · 𝐸) + 𝐶) ∈ 𝑉) |
34 | 9, 29, 31, 33 | syl3anc 1372 |
. . . 4
⊢ (𝜑 → ((𝐼 · 𝐸) + 𝐶) ∈ 𝑉) |
35 | 1, 2, 3, 4, 5, 6, 7, 8, 20, 26, 34 | hdmaplns1 39578 |
. . 3
⊢ (𝜑 → ((𝑆‘((𝐼 · 𝐸) + 𝐶))‘((𝐽 · 𝐸) − 𝐷)) = (((𝑆‘((𝐼 · 𝐸) + 𝐶))‘(𝐽 · 𝐸))(-g‘𝑅)((𝑆‘((𝐼 · 𝐸) + 𝐶))‘𝐷))) |
36 | | hdmapinvlem3.t |
. . . . 5
⊢ × =
(.r‘𝑅) |
37 | | hdmapinvlem3.z |
. . . . 5
⊢ 0 =
(0g‘𝑅) |
38 | | hdmapinvlem3.g |
. . . . 5
⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) |
39 | | hdmapinvlem3.ij |
. . . . 5
⊢ (𝜑 → (𝐼 × (𝐺‘𝐽)) = ((𝑆‘𝐷)‘𝐶)) |
40 | 1, 14, 22, 2, 3, 32, 4, 17, 5, 18, 36, 37, 7, 38, 8, 30, 25, 27, 10, 39 | hdmapinvlem3 39590 |
. . . 4
⊢ (𝜑 → ((𝑆‘((𝐽 · 𝐸) − 𝐷))‘((𝐼 · 𝐸) + 𝐶)) = 0 ) |
41 | 3, 4 | lmodvsubcl 19811 |
. . . . . 6
⊢ ((𝑈 ∈ LMod ∧ (𝐽 · 𝐸) ∈ 𝑉 ∧ 𝐷 ∈ 𝑉) → ((𝐽 · 𝐸) − 𝐷) ∈ 𝑉) |
42 | 9, 20, 26, 41 | syl3anc 1372 |
. . . . 5
⊢ (𝜑 → ((𝐽 · 𝐸) − 𝐷) ∈ 𝑉) |
43 | 1, 2, 3, 5, 37, 7,
8, 42, 34 | hdmapip0com 39587 |
. . . 4
⊢ (𝜑 → (((𝑆‘((𝐽 · 𝐸) − 𝐷))‘((𝐼 · 𝐸) + 𝐶)) = 0 ↔ ((𝑆‘((𝐼 · 𝐸) + 𝐶))‘((𝐽 · 𝐸) − 𝐷)) = 0 )) |
44 | 40, 43 | mpbid 235 |
. . 3
⊢ (𝜑 → ((𝑆‘((𝐼 · 𝐸) + 𝐶))‘((𝐽 · 𝐸) − 𝐷)) = 0 ) |
45 | 1, 2, 3, 17, 5, 18, 36, 7, 8, 16, 34, 10 | hdmaplnm1 39579 |
. . . . 5
⊢ (𝜑 → ((𝑆‘((𝐼 · 𝐸) + 𝐶))‘(𝐽 · 𝐸)) = (𝐽 × ((𝑆‘((𝐼 · 𝐸) + 𝐶))‘𝐸))) |
46 | | eqid 2739 |
. . . . . . . 8
⊢
(+g‘𝑅) = (+g‘𝑅) |
47 | 1, 2, 3, 32, 5, 46, 7, 8, 16, 29, 31 | hdmaplna2 39580 |
. . . . . . 7
⊢ (𝜑 → ((𝑆‘((𝐼 · 𝐸) + 𝐶))‘𝐸) = (((𝑆‘(𝐼 · 𝐸))‘𝐸)(+g‘𝑅)((𝑆‘𝐶)‘𝐸))) |
48 | 1, 14, 22, 2, 3, 5,
18, 36, 37, 7, 8, 30 | hdmapinvlem2 39589 |
. . . . . . . 8
⊢ (𝜑 → ((𝑆‘𝐶)‘𝐸) = 0 ) |
49 | 48 | oveq2d 7199 |
. . . . . . 7
⊢ (𝜑 → (((𝑆‘(𝐼 · 𝐸))‘𝐸)(+g‘𝑅)((𝑆‘𝐶)‘𝐸)) = (((𝑆‘(𝐼 · 𝐸))‘𝐸)(+g‘𝑅) 0 )) |
50 | 5 | lmodring 19774 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ LMod → 𝑅 ∈ Ring) |
51 | 9, 50 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Ring) |
52 | | ringgrp 19434 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
53 | 51, 52 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Grp) |
54 | 1, 2, 3, 5, 18, 7,
8, 16, 29 | hdmapipcl 39575 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑆‘(𝐼 · 𝐸))‘𝐸) ∈ 𝐵) |
55 | 18, 46, 37 | grprid 18265 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Grp ∧ ((𝑆‘(𝐼 · 𝐸))‘𝐸) ∈ 𝐵) → (((𝑆‘(𝐼 · 𝐸))‘𝐸)(+g‘𝑅) 0 ) = ((𝑆‘(𝐼 · 𝐸))‘𝐸)) |
56 | 53, 54, 55 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (((𝑆‘(𝐼 · 𝐸))‘𝐸)(+g‘𝑅) 0 ) = ((𝑆‘(𝐼 · 𝐸))‘𝐸)) |
57 | 1, 2, 3, 17, 5, 18, 36, 7, 38, 8, 16, 16, 27 | hdmapglnm2 39581 |
. . . . . . . 8
⊢ (𝜑 → ((𝑆‘(𝐼 · 𝐸))‘𝐸) = (((𝑆‘𝐸)‘𝐸) × (𝐺‘𝐼))) |
58 | | eqid 2739 |
. . . . . . . . . . 11
⊢
((HVMap‘𝐾)‘𝑊) = ((HVMap‘𝐾)‘𝑊) |
59 | | eqid 2739 |
. . . . . . . . . . 11
⊢
(1r‘𝑅) = (1r‘𝑅) |
60 | 1, 14, 58, 7, 8, 2,
5, 59 | hdmapevec2 39506 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑆‘𝐸)‘𝐸) = (1r‘𝑅)) |
61 | 60 | oveq1d 7198 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑆‘𝐸)‘𝐸) × (𝐺‘𝐼)) = ((1r‘𝑅) × (𝐺‘𝐼))) |
62 | 1, 2, 5, 18, 38, 8, 27 | hgmapcl 39559 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘𝐼) ∈ 𝐵) |
63 | 18, 36, 59 | ringlidm 19456 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝐺‘𝐼) ∈ 𝐵) → ((1r‘𝑅) × (𝐺‘𝐼)) = (𝐺‘𝐼)) |
64 | 51, 62, 63 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 →
((1r‘𝑅)
×
(𝐺‘𝐼)) = (𝐺‘𝐼)) |
65 | 61, 64 | eqtrd 2774 |
. . . . . . . 8
⊢ (𝜑 → (((𝑆‘𝐸)‘𝐸) × (𝐺‘𝐼)) = (𝐺‘𝐼)) |
66 | 56, 57, 65 | 3eqtrd 2778 |
. . . . . . 7
⊢ (𝜑 → (((𝑆‘(𝐼 · 𝐸))‘𝐸)(+g‘𝑅) 0 ) = (𝐺‘𝐼)) |
67 | 47, 49, 66 | 3eqtrd 2778 |
. . . . . 6
⊢ (𝜑 → ((𝑆‘((𝐼 · 𝐸) + 𝐶))‘𝐸) = (𝐺‘𝐼)) |
68 | 67 | oveq2d 7199 |
. . . . 5
⊢ (𝜑 → (𝐽 × ((𝑆‘((𝐼 · 𝐸) + 𝐶))‘𝐸)) = (𝐽 × (𝐺‘𝐼))) |
69 | 45, 68 | eqtrd 2774 |
. . . 4
⊢ (𝜑 → ((𝑆‘((𝐼 · 𝐸) + 𝐶))‘(𝐽 · 𝐸)) = (𝐽 × (𝐺‘𝐼))) |
70 | 1, 2, 3, 32, 5, 46, 7, 8, 26, 29, 31 | hdmaplna2 39580 |
. . . . 5
⊢ (𝜑 → ((𝑆‘((𝐼 · 𝐸) + 𝐶))‘𝐷) = (((𝑆‘(𝐼 · 𝐸))‘𝐷)(+g‘𝑅)((𝑆‘𝐶)‘𝐷))) |
71 | 1, 2, 3, 17, 5, 18, 36, 7, 38, 8, 26, 16, 27 | hdmapglnm2 39581 |
. . . . . . 7
⊢ (𝜑 → ((𝑆‘(𝐼 · 𝐸))‘𝐷) = (((𝑆‘𝐸)‘𝐷) × (𝐺‘𝐼))) |
72 | 1, 14, 22, 2, 3, 5,
18, 36, 37, 7, 8, 25 | hdmapinvlem1 39588 |
. . . . . . . 8
⊢ (𝜑 → ((𝑆‘𝐸)‘𝐷) = 0 ) |
73 | 72 | oveq1d 7198 |
. . . . . . 7
⊢ (𝜑 → (((𝑆‘𝐸)‘𝐷) × (𝐺‘𝐼)) = ( 0 × (𝐺‘𝐼))) |
74 | 18, 36, 37 | ringlz 19472 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝐺‘𝐼) ∈ 𝐵) → ( 0 × (𝐺‘𝐼)) = 0 ) |
75 | 51, 62, 74 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → ( 0 × (𝐺‘𝐼)) = 0 ) |
76 | 71, 73, 75 | 3eqtrd 2778 |
. . . . . 6
⊢ (𝜑 → ((𝑆‘(𝐼 · 𝐸))‘𝐷) = 0 ) |
77 | 76 | oveq1d 7198 |
. . . . 5
⊢ (𝜑 → (((𝑆‘(𝐼 · 𝐸))‘𝐷)(+g‘𝑅)((𝑆‘𝐶)‘𝐷)) = ( 0 (+g‘𝑅)((𝑆‘𝐶)‘𝐷))) |
78 | 1, 2, 3, 5, 18, 7,
8, 26, 31 | hdmapipcl 39575 |
. . . . . 6
⊢ (𝜑 → ((𝑆‘𝐶)‘𝐷) ∈ 𝐵) |
79 | 18, 46, 37 | grplid 18264 |
. . . . . 6
⊢ ((𝑅 ∈ Grp ∧ ((𝑆‘𝐶)‘𝐷) ∈ 𝐵) → ( 0 (+g‘𝑅)((𝑆‘𝐶)‘𝐷)) = ((𝑆‘𝐶)‘𝐷)) |
80 | 53, 78, 79 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → ( 0 (+g‘𝑅)((𝑆‘𝐶)‘𝐷)) = ((𝑆‘𝐶)‘𝐷)) |
81 | 70, 77, 80 | 3eqtrd 2778 |
. . . 4
⊢ (𝜑 → ((𝑆‘((𝐼 · 𝐸) + 𝐶))‘𝐷) = ((𝑆‘𝐶)‘𝐷)) |
82 | 69, 81 | oveq12d 7201 |
. . 3
⊢ (𝜑 → (((𝑆‘((𝐼 · 𝐸) + 𝐶))‘(𝐽 · 𝐸))(-g‘𝑅)((𝑆‘((𝐼 · 𝐸) + 𝐶))‘𝐷)) = ((𝐽 × (𝐺‘𝐼))(-g‘𝑅)((𝑆‘𝐶)‘𝐷))) |
83 | 35, 44, 82 | 3eqtr3rd 2783 |
. 2
⊢ (𝜑 → ((𝐽 × (𝐺‘𝐼))(-g‘𝑅)((𝑆‘𝐶)‘𝐷)) = 0 ) |
84 | 5, 18, 36 | lmodmcl 19778 |
. . . 4
⊢ ((𝑈 ∈ LMod ∧ 𝐽 ∈ 𝐵 ∧ (𝐺‘𝐼) ∈ 𝐵) → (𝐽 × (𝐺‘𝐼)) ∈ 𝐵) |
85 | 9, 10, 62, 84 | syl3anc 1372 |
. . 3
⊢ (𝜑 → (𝐽 × (𝐺‘𝐼)) ∈ 𝐵) |
86 | 18, 37, 6 | grpsubeq0 18316 |
. . 3
⊢ ((𝑅 ∈ Grp ∧ (𝐽 × (𝐺‘𝐼)) ∈ 𝐵 ∧ ((𝑆‘𝐶)‘𝐷) ∈ 𝐵) → (((𝐽 × (𝐺‘𝐼))(-g‘𝑅)((𝑆‘𝐶)‘𝐷)) = 0 ↔ (𝐽 × (𝐺‘𝐼)) = ((𝑆‘𝐶)‘𝐷))) |
87 | 53, 85, 78, 86 | syl3anc 1372 |
. 2
⊢ (𝜑 → (((𝐽 × (𝐺‘𝐼))(-g‘𝑅)((𝑆‘𝐶)‘𝐷)) = 0 ↔ (𝐽 × (𝐺‘𝐼)) = ((𝑆‘𝐶)‘𝐷))) |
88 | 83, 87 | mpbid 235 |
1
⊢ (𝜑 → (𝐽 × (𝐺‘𝐼)) = ((𝑆‘𝐶)‘𝐷)) |