Proof of Theorem mapdh6lem2N
Step | Hyp | Ref
| Expression |
1 | | mapdh.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
2 | | mapdh.m |
. . . 4
⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) |
3 | | mapdh.u |
. . . 4
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
4 | | eqid 2738 |
. . . 4
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
5 | | mapdh.k |
. . . 4
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
6 | 1, 3, 5 | dvhlmod 38736 |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ LMod) |
7 | | mapdhe6.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) |
8 | 7 | eldifad 3853 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
9 | | mapdh.v |
. . . . . . 7
⊢ 𝑉 = (Base‘𝑈) |
10 | | mapdh.n |
. . . . . . 7
⊢ 𝑁 = (LSpan‘𝑈) |
11 | 9, 4, 10 | lspsncl 19861 |
. . . . . 6
⊢ ((𝑈 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈)) |
12 | 6, 8, 11 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈)) |
13 | | mapdhe6.z |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) |
14 | 13 | eldifad 3853 |
. . . . . 6
⊢ (𝜑 → 𝑍 ∈ 𝑉) |
15 | 9, 4, 10 | lspsncl 19861 |
. . . . . 6
⊢ ((𝑈 ∈ LMod ∧ 𝑍 ∈ 𝑉) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑈)) |
16 | 6, 14, 15 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑈)) |
17 | | eqid 2738 |
. . . . . 6
⊢
(LSSum‘𝑈) =
(LSSum‘𝑈) |
18 | 4, 17 | lsmcl 19967 |
. . . . 5
⊢ ((𝑈 ∈ LMod ∧ (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈) ∧ (𝑁‘{𝑍}) ∈ (LSubSp‘𝑈)) → ((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍})) ∈ (LSubSp‘𝑈)) |
19 | 6, 12, 16, 18 | syl3anc 1372 |
. . . 4
⊢ (𝜑 → ((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍})) ∈ (LSubSp‘𝑈)) |
20 | | mapdhcl.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) |
21 | 20 | eldifad 3853 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
22 | | mapdh.p |
. . . . . . . . 9
⊢ + =
(+g‘𝑈) |
23 | 9, 22 | lmodvacl 19760 |
. . . . . . . 8
⊢ ((𝑈 ∈ LMod ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉) → (𝑌 + 𝑍) ∈ 𝑉) |
24 | 6, 8, 14, 23 | syl3anc 1372 |
. . . . . . 7
⊢ (𝜑 → (𝑌 + 𝑍) ∈ 𝑉) |
25 | | mapdh.s |
. . . . . . . 8
⊢ − =
(-g‘𝑈) |
26 | 9, 25 | lmodvsubcl 19791 |
. . . . . . 7
⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ (𝑌 + 𝑍) ∈ 𝑉) → (𝑋 − (𝑌 + 𝑍)) ∈ 𝑉) |
27 | 6, 21, 24, 26 | syl3anc 1372 |
. . . . . 6
⊢ (𝜑 → (𝑋 − (𝑌 + 𝑍)) ∈ 𝑉) |
28 | 9, 4, 10 | lspsncl 19861 |
. . . . . 6
⊢ ((𝑈 ∈ LMod ∧ (𝑋 − (𝑌 + 𝑍)) ∈ 𝑉) → (𝑁‘{(𝑋 − (𝑌 + 𝑍))}) ∈ (LSubSp‘𝑈)) |
29 | 6, 27, 28 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝑁‘{(𝑋 − (𝑌 + 𝑍))}) ∈ (LSubSp‘𝑈)) |
30 | 9, 4, 10 | lspsncl 19861 |
. . . . . 6
⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑈)) |
31 | 6, 21, 30 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑈)) |
32 | 4, 17 | lsmcl 19967 |
. . . . 5
⊢ ((𝑈 ∈ LMod ∧ (𝑁‘{(𝑋 − (𝑌 + 𝑍))}) ∈ (LSubSp‘𝑈) ∧ (𝑁‘{𝑋}) ∈ (LSubSp‘𝑈)) → ((𝑁‘{(𝑋 − (𝑌 + 𝑍))})(LSSum‘𝑈)(𝑁‘{𝑋})) ∈ (LSubSp‘𝑈)) |
33 | 6, 29, 31, 32 | syl3anc 1372 |
. . . 4
⊢ (𝜑 → ((𝑁‘{(𝑋 − (𝑌 + 𝑍))})(LSSum‘𝑈)(𝑁‘{𝑋})) ∈ (LSubSp‘𝑈)) |
34 | 1, 2, 3, 4, 5, 19,
33 | mapdin 39288 |
. . 3
⊢ (𝜑 → (𝑀‘(((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − (𝑌 + 𝑍))})(LSSum‘𝑈)(𝑁‘{𝑋})))) = ((𝑀‘((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍}))) ∩ (𝑀‘((𝑁‘{(𝑋 − (𝑌 + 𝑍))})(LSSum‘𝑈)(𝑁‘{𝑋}))))) |
35 | | mapdh.c |
. . . . . 6
⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) |
36 | | eqid 2738 |
. . . . . 6
⊢
(LSSum‘𝐶) =
(LSSum‘𝐶) |
37 | 1, 2, 3, 4, 17, 35, 36, 5, 12, 16 | mapdlsm 39290 |
. . . . 5
⊢ (𝜑 → (𝑀‘((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍}))) = ((𝑀‘(𝑁‘{𝑌}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑍})))) |
38 | | mapdh6.fg |
. . . . . . . 8
⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑌〉) = 𝐺) |
39 | | mapdh.q |
. . . . . . . . 9
⊢ 𝑄 = (0g‘𝐶) |
40 | | mapdh.i |
. . . . . . . . 9
⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd
‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))))) |
41 | | mapdhc.o |
. . . . . . . . 9
⊢ 0 =
(0g‘𝑈) |
42 | | mapdh.d |
. . . . . . . . 9
⊢ 𝐷 = (Base‘𝐶) |
43 | | mapdh.r |
. . . . . . . . 9
⊢ 𝑅 = (-g‘𝐶) |
44 | | mapdh.j |
. . . . . . . . 9
⊢ 𝐽 = (LSpan‘𝐶) |
45 | | mapdhc.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ 𝐷) |
46 | | mapdh.mn |
. . . . . . . . 9
⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) |
47 | 1, 3, 5 | dvhlvec 38735 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ∈ LVec) |
48 | | mapdh6.yz |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) |
49 | | mapdhe6.xn |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) |
50 | 9, 41, 10, 47, 8, 13, 21, 48, 49 | lspindp2 20019 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}) ∧ ¬ 𝑍 ∈ (𝑁‘{𝑋, 𝑌}))) |
51 | 50 | simpld 498 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) |
52 | 39, 40, 1, 2, 3, 9, 25, 41, 10, 35, 42, 43, 44, 5, 45, 46, 20, 8, 51 | mapdhcl 39353 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑌〉) ∈ 𝐷) |
53 | 38, 52 | eqeltrrd 2834 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ 𝐷) |
54 | 39, 40, 1, 2, 3, 9, 25, 41, 10, 35, 42, 43, 44, 5, 45, 46, 20, 7, 53, 51 | mapdheq 39354 |
. . . . . . . 8
⊢ (𝜑 → ((𝐼‘〈𝑋, 𝐹, 𝑌〉) = 𝐺 ↔ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝐺}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐹𝑅𝐺)})))) |
55 | 38, 54 | mpbid 235 |
. . . . . . 7
⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝐺}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐹𝑅𝐺)}))) |
56 | 55 | simpld 498 |
. . . . . 6
⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝐺})) |
57 | | mapdh6.fe |
. . . . . . . 8
⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑍〉) = 𝐸) |
58 | 9, 41, 10, 47, 7, 14, 21, 48, 49 | lspindp1 20017 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁‘{𝑋}) ≠ (𝑁‘{𝑍}) ∧ ¬ 𝑌 ∈ (𝑁‘{𝑋, 𝑍}))) |
59 | 58 | simpld 498 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍})) |
60 | 39, 40, 1, 2, 3, 9, 25, 41, 10, 35, 42, 43, 44, 5, 45, 46, 20, 14, 59 | mapdhcl 39353 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑍〉) ∈ 𝐷) |
61 | 57, 60 | eqeltrrd 2834 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ 𝐷) |
62 | 39, 40, 1, 2, 3, 9, 25, 41, 10, 35, 42, 43, 44, 5, 45, 46, 20, 13, 61, 59 | mapdheq 39354 |
. . . . . . . 8
⊢ (𝜑 → ((𝐼‘〈𝑋, 𝐹, 𝑍〉) = 𝐸 ↔ ((𝑀‘(𝑁‘{𝑍})) = (𝐽‘{𝐸}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑍)})) = (𝐽‘{(𝐹𝑅𝐸)})))) |
63 | 57, 62 | mpbid 235 |
. . . . . . 7
⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑍})) = (𝐽‘{𝐸}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑍)})) = (𝐽‘{(𝐹𝑅𝐸)}))) |
64 | 63 | simpld 498 |
. . . . . 6
⊢ (𝜑 → (𝑀‘(𝑁‘{𝑍})) = (𝐽‘{𝐸})) |
65 | 56, 64 | oveq12d 7182 |
. . . . 5
⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑌}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑍}))) = ((𝐽‘{𝐺})(LSSum‘𝐶)(𝐽‘{𝐸}))) |
66 | 37, 65 | eqtrd 2773 |
. . . 4
⊢ (𝜑 → (𝑀‘((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍}))) = ((𝐽‘{𝐺})(LSSum‘𝐶)(𝐽‘{𝐸}))) |
67 | 1, 2, 3, 4, 17, 35, 36, 5, 29, 31 | mapdlsm 39290 |
. . . . 5
⊢ (𝜑 → (𝑀‘((𝑁‘{(𝑋 − (𝑌 + 𝑍))})(LSSum‘𝑈)(𝑁‘{𝑋}))) = ((𝑀‘(𝑁‘{(𝑋 − (𝑌 + 𝑍))}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑋})))) |
68 | | mapdh.a |
. . . . . . 7
⊢ ✚ =
(+g‘𝐶) |
69 | 39, 40, 1, 2, 3, 9, 25, 41, 10, 35, 42, 43, 44, 5, 45, 46, 20, 22, 68, 7, 13, 49, 48, 38, 57 | mapdh6lem1N 39359 |
. . . . . 6
⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − (𝑌 + 𝑍))})) = (𝐽‘{(𝐹𝑅(𝐺 ✚ 𝐸))})) |
70 | 69, 46 | oveq12d 7182 |
. . . . 5
⊢ (𝜑 → ((𝑀‘(𝑁‘{(𝑋 − (𝑌 + 𝑍))}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑋}))) = ((𝐽‘{(𝐹𝑅(𝐺 ✚ 𝐸))})(LSSum‘𝐶)(𝐽‘{𝐹}))) |
71 | 67, 70 | eqtrd 2773 |
. . . 4
⊢ (𝜑 → (𝑀‘((𝑁‘{(𝑋 − (𝑌 + 𝑍))})(LSSum‘𝑈)(𝑁‘{𝑋}))) = ((𝐽‘{(𝐹𝑅(𝐺 ✚ 𝐸))})(LSSum‘𝐶)(𝐽‘{𝐹}))) |
72 | 66, 71 | ineq12d 4102 |
. . 3
⊢ (𝜑 → ((𝑀‘((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍}))) ∩ (𝑀‘((𝑁‘{(𝑋 − (𝑌 + 𝑍))})(LSSum‘𝑈)(𝑁‘{𝑋})))) = (((𝐽‘{𝐺})(LSSum‘𝐶)(𝐽‘{𝐸})) ∩ ((𝐽‘{(𝐹𝑅(𝐺 ✚ 𝐸))})(LSSum‘𝐶)(𝐽‘{𝐹})))) |
73 | 34, 72 | eqtrd 2773 |
. 2
⊢ (𝜑 → (𝑀‘(((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − (𝑌 + 𝑍))})(LSSum‘𝑈)(𝑁‘{𝑋})))) = (((𝐽‘{𝐺})(LSSum‘𝐶)(𝐽‘{𝐸})) ∩ ((𝐽‘{(𝐹𝑅(𝐺 ✚ 𝐸))})(LSSum‘𝐶)(𝐽‘{𝐹})))) |
74 | 9, 25, 41, 17, 10, 47, 21, 49, 48, 7, 13, 22 | baerlem5b 39341 |
. . 3
⊢ (𝜑 → (𝑁‘{(𝑌 + 𝑍)}) = (((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − (𝑌 + 𝑍))})(LSSum‘𝑈)(𝑁‘{𝑋})))) |
75 | 74 | fveq2d 6672 |
. 2
⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑌 + 𝑍)})) = (𝑀‘(((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − (𝑌 + 𝑍))})(LSSum‘𝑈)(𝑁‘{𝑋}))))) |
76 | 1, 35, 5 | lcdlvec 39217 |
. . 3
⊢ (𝜑 → 𝐶 ∈ LVec) |
77 | 1, 2, 3, 9, 10, 35, 42, 44, 5, 45, 46, 21, 8, 53, 56, 14, 61, 64, 49 | mapdindp 39297 |
. . 3
⊢ (𝜑 → ¬ 𝐹 ∈ (𝐽‘{𝐺, 𝐸})) |
78 | 1, 2, 3, 9, 10, 35, 42, 44, 5, 53, 56, 8, 14, 61, 64, 48 | mapdncol 39296 |
. . 3
⊢ (𝜑 → (𝐽‘{𝐺}) ≠ (𝐽‘{𝐸})) |
79 | 1, 2, 3, 9, 10, 35, 42, 44, 5, 53, 56, 41, 39, 7 | mapdn0 39295 |
. . 3
⊢ (𝜑 → 𝐺 ∈ (𝐷 ∖ {𝑄})) |
80 | 1, 2, 3, 9, 10, 35, 42, 44, 5, 61, 64, 41, 39, 13 | mapdn0 39295 |
. . 3
⊢ (𝜑 → 𝐸 ∈ (𝐷 ∖ {𝑄})) |
81 | 42, 43, 39, 36, 44, 76, 45, 77, 78, 79, 80, 68 | baerlem5b 39341 |
. 2
⊢ (𝜑 → (𝐽‘{(𝐺 ✚ 𝐸)}) = (((𝐽‘{𝐺})(LSSum‘𝐶)(𝐽‘{𝐸})) ∩ ((𝐽‘{(𝐹𝑅(𝐺 ✚ 𝐸))})(LSSum‘𝐶)(𝐽‘{𝐹})))) |
82 | 73, 75, 81 | 3eqtr4d 2783 |
1
⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑌 + 𝑍)})) = (𝐽‘{(𝐺 ✚ 𝐸)})) |