Proof of Theorem mapdpglem30
Step | Hyp | Ref
| Expression |
1 | | mapdpg.f |
. . 3
⊢ 𝐹 = (Base‘𝐶) |
2 | | eqid 2738 |
. . 3
⊢
(+g‘𝐶) = (+g‘𝐶) |
3 | | eqid 2738 |
. . 3
⊢
(Scalar‘𝐶) =
(Scalar‘𝐶) |
4 | | eqid 2738 |
. . 3
⊢
(Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶)) |
5 | | mapdpglem26.t |
. . 3
⊢ · = (
·𝑠 ‘𝐶) |
6 | | eqid 2738 |
. . 3
⊢
(0g‘𝐶) = (0g‘𝐶) |
7 | | mapdpg.j |
. . 3
⊢ 𝐽 = (LSpan‘𝐶) |
8 | | mapdpg.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
9 | | mapdpg.c |
. . . 4
⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) |
10 | | mapdpg.k |
. . . 4
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
11 | 8, 9, 10 | lcdlvec 39532 |
. . 3
⊢ (𝜑 → 𝐶 ∈ LVec) |
12 | | mapdpg.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ 𝐹) |
13 | | mapdpg.m |
. . . . 5
⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) |
14 | | mapdpg.u |
. . . . 5
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
15 | | mapdpg.v |
. . . . 5
⊢ 𝑉 = (Base‘𝑈) |
16 | | mapdpg.s |
. . . . 5
⊢ − =
(-g‘𝑈) |
17 | | mapdpg.z |
. . . . 5
⊢ 0 =
(0g‘𝑈) |
18 | | mapdpg.n |
. . . . 5
⊢ 𝑁 = (LSpan‘𝑈) |
19 | | mapdpg.r |
. . . . 5
⊢ 𝑅 = (-g‘𝐶) |
20 | | mapdpg.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) |
21 | | mapdpg.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) |
22 | | mapdpg.ne |
. . . . 5
⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) |
23 | | mapdpg.e |
. . . . 5
⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) |
24 | 8, 13, 14, 15, 16, 17, 18, 9, 1, 19, 7, 10, 20, 21, 12, 22, 23 | mapdpglem30a 39636 |
. . . 4
⊢ (𝜑 → 𝐺 ≠ (0g‘𝐶)) |
25 | | eldifsn 4717 |
. . . 4
⊢ (𝐺 ∈ (𝐹 ∖ {(0g‘𝐶)}) ↔ (𝐺 ∈ 𝐹 ∧ 𝐺 ≠ (0g‘𝐶))) |
26 | 12, 24, 25 | sylanbrc 582 |
. . 3
⊢ (𝜑 → 𝐺 ∈ (𝐹 ∖ {(0g‘𝐶)})) |
27 | | mapdpgem25.i1 |
. . . . 5
⊢ (𝜑 → (𝑖 ∈ 𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅𝑖)})))) |
28 | 27 | simpld 494 |
. . . 4
⊢ (𝜑 → 𝑖 ∈ 𝐹) |
29 | | mapdpgem25.h1 |
. . . . 5
⊢ (𝜑 → (ℎ ∈ 𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)})))) |
30 | 8, 13, 14, 15, 16, 17, 18, 9, 1, 19, 7, 10, 20, 21, 12, 22, 23, 29, 27 | mapdpglem30b 39637 |
. . . 4
⊢ (𝜑 → 𝑖 ≠ (0g‘𝐶)) |
31 | | eldifsn 4717 |
. . . 4
⊢ (𝑖 ∈ (𝐹 ∖ {(0g‘𝐶)}) ↔ (𝑖 ∈ 𝐹 ∧ 𝑖 ≠ (0g‘𝐶))) |
32 | 28, 30, 31 | sylanbrc 582 |
. . 3
⊢ (𝜑 → 𝑖 ∈ (𝐹 ∖ {(0g‘𝐶)})) |
33 | | mapdpglem28.ve |
. . . 4
⊢ (𝜑 → 𝑣 ∈ 𝐵) |
34 | | mapdpglem26.a |
. . . . 5
⊢ 𝐴 = (Scalar‘𝑈) |
35 | | mapdpglem26.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐴) |
36 | 8, 14, 34, 35, 9, 3, 4, 10 | lcdsbase 39541 |
. . . 4
⊢ (𝜑 →
(Base‘(Scalar‘𝐶)) = 𝐵) |
37 | 33, 36 | eleqtrrd 2842 |
. . 3
⊢ (𝜑 → 𝑣 ∈ (Base‘(Scalar‘𝐶))) |
38 | 8, 14, 10 | dvhlmod 39051 |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ LMod) |
39 | 34 | lmodring 20046 |
. . . . . 6
⊢ (𝑈 ∈ LMod → 𝐴 ∈ Ring) |
40 | 38, 39 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ Ring) |
41 | | ringgrp 19703 |
. . . . . . 7
⊢ (𝐴 ∈ Ring → 𝐴 ∈ Grp) |
42 | 40, 41 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ Grp) |
43 | | eqid 2738 |
. . . . . . . 8
⊢
(1r‘𝐴) = (1r‘𝐴) |
44 | 35, 43 | ringidcl 19722 |
. . . . . . 7
⊢ (𝐴 ∈ Ring →
(1r‘𝐴)
∈ 𝐵) |
45 | 40, 44 | syl 17 |
. . . . . 6
⊢ (𝜑 → (1r‘𝐴) ∈ 𝐵) |
46 | | eqid 2738 |
. . . . . . 7
⊢
(invg‘𝐴) = (invg‘𝐴) |
47 | 35, 46 | grpinvcl 18542 |
. . . . . 6
⊢ ((𝐴 ∈ Grp ∧
(1r‘𝐴)
∈ 𝐵) →
((invg‘𝐴)‘(1r‘𝐴)) ∈ 𝐵) |
48 | 42, 45, 47 | syl2anc 583 |
. . . . 5
⊢ (𝜑 →
((invg‘𝐴)‘(1r‘𝐴)) ∈ 𝐵) |
49 | | eqid 2738 |
. . . . . 6
⊢
(.r‘𝐴) = (.r‘𝐴) |
50 | 35, 49 | ringcl 19715 |
. . . . 5
⊢ ((𝐴 ∈ Ring ∧ 𝑣 ∈ 𝐵 ∧ ((invg‘𝐴)‘(1r‘𝐴)) ∈ 𝐵) → (𝑣(.r‘𝐴)((invg‘𝐴)‘(1r‘𝐴))) ∈ 𝐵) |
51 | 40, 33, 48, 50 | syl3anc 1369 |
. . . 4
⊢ (𝜑 → (𝑣(.r‘𝐴)((invg‘𝐴)‘(1r‘𝐴))) ∈ 𝐵) |
52 | 51, 36 | eleqtrrd 2842 |
. . 3
⊢ (𝜑 → (𝑣(.r‘𝐴)((invg‘𝐴)‘(1r‘𝐴))) ∈
(Base‘(Scalar‘𝐶))) |
53 | 45, 36 | eleqtrrd 2842 |
. . 3
⊢ (𝜑 → (1r‘𝐴) ∈
(Base‘(Scalar‘𝐶))) |
54 | | mapdpglem28.ue |
. . . . 5
⊢ (𝜑 → 𝑢 ∈ 𝐵) |
55 | 35, 49 | ringcl 19715 |
. . . . 5
⊢ ((𝐴 ∈ Ring ∧ 𝑢 ∈ 𝐵 ∧ ((invg‘𝐴)‘(1r‘𝐴)) ∈ 𝐵) → (𝑢(.r‘𝐴)((invg‘𝐴)‘(1r‘𝐴))) ∈ 𝐵) |
56 | 40, 54, 48, 55 | syl3anc 1369 |
. . . 4
⊢ (𝜑 → (𝑢(.r‘𝐴)((invg‘𝐴)‘(1r‘𝐴))) ∈ 𝐵) |
57 | 56, 36 | eleqtrrd 2842 |
. . 3
⊢ (𝜑 → (𝑢(.r‘𝐴)((invg‘𝐴)‘(1r‘𝐴))) ∈
(Base‘(Scalar‘𝐶))) |
58 | | mapdpglem26.o |
. . . 4
⊢ 𝑂 = (0g‘𝐴) |
59 | | mapdpglem28.u1 |
. . . 4
⊢ (𝜑 → ℎ = (𝑢 · 𝑖)) |
60 | | mapdpglem28.u2 |
. . . 4
⊢ (𝜑 → (𝐺𝑅ℎ) = (𝑣 · (𝐺𝑅𝑖))) |
61 | 8, 13, 14, 15, 16, 17, 18, 9, 1, 19, 7, 10, 20, 21, 12, 22, 23, 29, 27, 34, 35, 5, 58, 33, 59, 60 | mapdpglem29 39641 |
. . 3
⊢ (𝜑 → (𝐽‘{𝐺}) ≠ (𝐽‘{𝑖})) |
62 | 8, 14, 34, 35, 49, 9, 1, 5, 10,
48, 54, 28 | lcdvsass 39548 |
. . . . 5
⊢ (𝜑 → ((𝑢(.r‘𝐴)((invg‘𝐴)‘(1r‘𝐴))) · 𝑖) = (((invg‘𝐴)‘(1r‘𝐴)) · (𝑢 · 𝑖))) |
63 | 62 | oveq2d 7271 |
. . . 4
⊢ (𝜑 →
(((1r‘𝐴)
·
𝐺)(+g‘𝐶)((𝑢(.r‘𝐴)((invg‘𝐴)‘(1r‘𝐴))) · 𝑖)) = (((1r‘𝐴) · 𝐺)(+g‘𝐶)(((invg‘𝐴)‘(1r‘𝐴)) · (𝑢 · 𝑖)))) |
64 | 8, 14, 34, 35, 9, 1, 5, 10, 45, 12 | lcdvscl 39546 |
. . . . 5
⊢ (𝜑 →
((1r‘𝐴)
·
𝐺) ∈ 𝐹) |
65 | 8, 14, 34, 35, 9, 1, 5, 10, 54, 28 | lcdvscl 39546 |
. . . . 5
⊢ (𝜑 → (𝑢 · 𝑖) ∈ 𝐹) |
66 | 8, 14, 34, 46, 43, 9, 1, 2, 5, 19, 10, 64, 65 | lcdvsub 39558 |
. . . 4
⊢ (𝜑 →
(((1r‘𝐴)
·
𝐺)𝑅(𝑢 · 𝑖)) = (((1r‘𝐴) · 𝐺)(+g‘𝐶)(((invg‘𝐴)‘(1r‘𝐴)) · (𝑢 · 𝑖)))) |
67 | 8, 14, 34, 35, 49, 9, 1, 5, 10,
48, 33, 28 | lcdvsass 39548 |
. . . . . 6
⊢ (𝜑 → ((𝑣(.r‘𝐴)((invg‘𝐴)‘(1r‘𝐴))) · 𝑖) = (((invg‘𝐴)‘(1r‘𝐴)) · (𝑣 · 𝑖))) |
68 | 67 | oveq2d 7271 |
. . . . 5
⊢ (𝜑 → ((𝑣 · 𝐺)(+g‘𝐶)((𝑣(.r‘𝐴)((invg‘𝐴)‘(1r‘𝐴))) · 𝑖)) = ((𝑣 · 𝐺)(+g‘𝐶)(((invg‘𝐴)‘(1r‘𝐴)) · (𝑣 · 𝑖)))) |
69 | 8, 14, 34, 35, 9, 1, 5, 10, 33, 12 | lcdvscl 39546 |
. . . . . 6
⊢ (𝜑 → (𝑣 · 𝐺) ∈ 𝐹) |
70 | 8, 14, 34, 35, 9, 1, 5, 10, 33, 28 | lcdvscl 39546 |
. . . . . 6
⊢ (𝜑 → (𝑣 · 𝑖) ∈ 𝐹) |
71 | 8, 14, 34, 46, 43, 9, 1, 2, 5, 19, 10, 69, 70 | lcdvsub 39558 |
. . . . 5
⊢ (𝜑 → ((𝑣 · 𝐺)𝑅(𝑣 · 𝑖)) = ((𝑣 · 𝐺)(+g‘𝐶)(((invg‘𝐴)‘(1r‘𝐴)) · (𝑣 · 𝑖)))) |
72 | 8, 13, 14, 15, 16, 17, 18, 9, 1, 19, 7, 10, 20, 21, 12, 22, 23, 29, 27, 34, 35, 5, 58, 33, 59, 60 | mapdpglem28 39642 |
. . . . . 6
⊢ (𝜑 → ((𝑣 · 𝐺)𝑅(𝑣 · 𝑖)) = (𝐺𝑅(𝑢 · 𝑖))) |
73 | | eqid 2738 |
. . . . . . . . . 10
⊢
(1r‘(Scalar‘𝐶)) =
(1r‘(Scalar‘𝐶)) |
74 | 8, 14, 34, 43, 9, 3, 73, 10 | lcd1 39550 |
. . . . . . . . 9
⊢ (𝜑 →
(1r‘(Scalar‘𝐶)) = (1r‘𝐴)) |
75 | 74 | oveq1d 7270 |
. . . . . . . 8
⊢ (𝜑 →
((1r‘(Scalar‘𝐶)) · 𝐺) = ((1r‘𝐴) · 𝐺)) |
76 | 8, 9, 10 | lcdlmod 39533 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ LMod) |
77 | 1, 3, 5, 73 | lmodvs1 20066 |
. . . . . . . . 9
⊢ ((𝐶 ∈ LMod ∧ 𝐺 ∈ 𝐹) →
((1r‘(Scalar‘𝐶)) · 𝐺) = 𝐺) |
78 | 76, 12, 77 | syl2anc 583 |
. . . . . . . 8
⊢ (𝜑 →
((1r‘(Scalar‘𝐶)) · 𝐺) = 𝐺) |
79 | 75, 78 | eqtr3d 2780 |
. . . . . . 7
⊢ (𝜑 →
((1r‘𝐴)
·
𝐺) = 𝐺) |
80 | 79 | oveq1d 7270 |
. . . . . 6
⊢ (𝜑 →
(((1r‘𝐴)
·
𝐺)𝑅(𝑢 · 𝑖)) = (𝐺𝑅(𝑢 · 𝑖))) |
81 | 72, 80 | eqtr4d 2781 |
. . . . 5
⊢ (𝜑 → ((𝑣 · 𝐺)𝑅(𝑣 · 𝑖)) = (((1r‘𝐴) · 𝐺)𝑅(𝑢 · 𝑖))) |
82 | 68, 71, 81 | 3eqtr2rd 2785 |
. . . 4
⊢ (𝜑 →
(((1r‘𝐴)
·
𝐺)𝑅(𝑢 · 𝑖)) = ((𝑣 · 𝐺)(+g‘𝐶)((𝑣(.r‘𝐴)((invg‘𝐴)‘(1r‘𝐴))) · 𝑖))) |
83 | 63, 66, 82 | 3eqtr2rd 2785 |
. . 3
⊢ (𝜑 → ((𝑣 · 𝐺)(+g‘𝐶)((𝑣(.r‘𝐴)((invg‘𝐴)‘(1r‘𝐴))) · 𝑖)) = (((1r‘𝐴) · 𝐺)(+g‘𝐶)((𝑢(.r‘𝐴)((invg‘𝐴)‘(1r‘𝐴))) · 𝑖))) |
84 | 1, 2, 3, 4, 5, 6, 7, 11, 26, 32, 37, 52, 53, 57, 61, 83 | lvecindp2 20316 |
. 2
⊢ (𝜑 → (𝑣 = (1r‘𝐴) ∧ (𝑣(.r‘𝐴)((invg‘𝐴)‘(1r‘𝐴))) = (𝑢(.r‘𝐴)((invg‘𝐴)‘(1r‘𝐴))))) |
85 | 35, 49, 43, 46, 40, 33 | rngnegr 19749 |
. . . . 5
⊢ (𝜑 → (𝑣(.r‘𝐴)((invg‘𝐴)‘(1r‘𝐴))) =
((invg‘𝐴)‘𝑣)) |
86 | 35, 49, 43, 46, 40, 54 | rngnegr 19749 |
. . . . 5
⊢ (𝜑 → (𝑢(.r‘𝐴)((invg‘𝐴)‘(1r‘𝐴))) =
((invg‘𝐴)‘𝑢)) |
87 | 85, 86 | eqeq12d 2754 |
. . . 4
⊢ (𝜑 → ((𝑣(.r‘𝐴)((invg‘𝐴)‘(1r‘𝐴))) = (𝑢(.r‘𝐴)((invg‘𝐴)‘(1r‘𝐴))) ↔
((invg‘𝐴)‘𝑣) = ((invg‘𝐴)‘𝑢))) |
88 | 35, 46, 42, 33, 54 | grpinv11 18559 |
. . . 4
⊢ (𝜑 →
(((invg‘𝐴)‘𝑣) = ((invg‘𝐴)‘𝑢) ↔ 𝑣 = 𝑢)) |
89 | 87, 88 | bitrd 278 |
. . 3
⊢ (𝜑 → ((𝑣(.r‘𝐴)((invg‘𝐴)‘(1r‘𝐴))) = (𝑢(.r‘𝐴)((invg‘𝐴)‘(1r‘𝐴))) ↔ 𝑣 = 𝑢)) |
90 | 89 | anbi2d 628 |
. 2
⊢ (𝜑 → ((𝑣 = (1r‘𝐴) ∧ (𝑣(.r‘𝐴)((invg‘𝐴)‘(1r‘𝐴))) = (𝑢(.r‘𝐴)((invg‘𝐴)‘(1r‘𝐴)))) ↔ (𝑣 = (1r‘𝐴) ∧ 𝑣 = 𝑢))) |
91 | 84, 90 | mpbid 231 |
1
⊢ (𝜑 → (𝑣 = (1r‘𝐴) ∧ 𝑣 = 𝑢)) |