Proof of Theorem hdmap1l6lem1
Step | Hyp | Ref
| Expression |
1 | | hdmap1l6.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
2 | | hdmap1l6.m |
. . . 4
⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) |
3 | | hdmap1l6.u |
. . . 4
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
4 | | eqid 2738 |
. . . 4
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
5 | | hdmap1l6.k |
. . . 4
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
6 | 1, 3, 5 | dvhlmod 39124 |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ LMod) |
7 | | hdmap1l6cl.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) |
8 | 7 | eldifad 3899 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
9 | | hdmap1l6e.y |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) |
10 | 9 | eldifad 3899 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
11 | | hdmap1l6.v |
. . . . . . . 8
⊢ 𝑉 = (Base‘𝑈) |
12 | | hdmap1l6.s |
. . . . . . . 8
⊢ − =
(-g‘𝑈) |
13 | 11, 12 | lmodvsubcl 20168 |
. . . . . . 7
⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 − 𝑌) ∈ 𝑉) |
14 | 6, 8, 10, 13 | syl3anc 1370 |
. . . . . 6
⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝑉) |
15 | | hdmap1l6.n |
. . . . . . 7
⊢ 𝑁 = (LSpan‘𝑈) |
16 | 11, 4, 15 | lspsncl 20239 |
. . . . . 6
⊢ ((𝑈 ∈ LMod ∧ (𝑋 − 𝑌) ∈ 𝑉) → (𝑁‘{(𝑋 − 𝑌)}) ∈ (LSubSp‘𝑈)) |
17 | 6, 14, 16 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝑁‘{(𝑋 − 𝑌)}) ∈ (LSubSp‘𝑈)) |
18 | | hdmap1l6e.z |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) |
19 | 18 | eldifad 3899 |
. . . . . 6
⊢ (𝜑 → 𝑍 ∈ 𝑉) |
20 | 11, 4, 15 | lspsncl 20239 |
. . . . . 6
⊢ ((𝑈 ∈ LMod ∧ 𝑍 ∈ 𝑉) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑈)) |
21 | 6, 19, 20 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑈)) |
22 | | eqid 2738 |
. . . . . 6
⊢
(LSSum‘𝑈) =
(LSSum‘𝑈) |
23 | 4, 22 | lsmcl 20345 |
. . . . 5
⊢ ((𝑈 ∈ LMod ∧ (𝑁‘{(𝑋 − 𝑌)}) ∈ (LSubSp‘𝑈) ∧ (𝑁‘{𝑍}) ∈ (LSubSp‘𝑈)) → ((𝑁‘{(𝑋 − 𝑌)})(LSSum‘𝑈)(𝑁‘{𝑍})) ∈ (LSubSp‘𝑈)) |
24 | 6, 17, 21, 23 | syl3anc 1370 |
. . . 4
⊢ (𝜑 → ((𝑁‘{(𝑋 − 𝑌)})(LSSum‘𝑈)(𝑁‘{𝑍})) ∈ (LSubSp‘𝑈)) |
25 | 11, 12 | lmodvsubcl 20168 |
. . . . . . 7
⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉) → (𝑋 − 𝑍) ∈ 𝑉) |
26 | 6, 8, 19, 25 | syl3anc 1370 |
. . . . . 6
⊢ (𝜑 → (𝑋 − 𝑍) ∈ 𝑉) |
27 | 11, 4, 15 | lspsncl 20239 |
. . . . . 6
⊢ ((𝑈 ∈ LMod ∧ (𝑋 − 𝑍) ∈ 𝑉) → (𝑁‘{(𝑋 − 𝑍)}) ∈ (LSubSp‘𝑈)) |
28 | 6, 26, 27 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝑁‘{(𝑋 − 𝑍)}) ∈ (LSubSp‘𝑈)) |
29 | 11, 4, 15 | lspsncl 20239 |
. . . . . 6
⊢ ((𝑈 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈)) |
30 | 6, 10, 29 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈)) |
31 | 4, 22 | lsmcl 20345 |
. . . . 5
⊢ ((𝑈 ∈ LMod ∧ (𝑁‘{(𝑋 − 𝑍)}) ∈ (LSubSp‘𝑈) ∧ (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈)) → ((𝑁‘{(𝑋 − 𝑍)})(LSSum‘𝑈)(𝑁‘{𝑌})) ∈ (LSubSp‘𝑈)) |
32 | 6, 28, 30, 31 | syl3anc 1370 |
. . . 4
⊢ (𝜑 → ((𝑁‘{(𝑋 − 𝑍)})(LSSum‘𝑈)(𝑁‘{𝑌})) ∈ (LSubSp‘𝑈)) |
33 | 1, 2, 3, 4, 5, 24,
32 | mapdin 39676 |
. . 3
⊢ (𝜑 → (𝑀‘(((𝑁‘{(𝑋 − 𝑌)})(LSSum‘𝑈)(𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑍)})(LSSum‘𝑈)(𝑁‘{𝑌})))) = ((𝑀‘((𝑁‘{(𝑋 − 𝑌)})(LSSum‘𝑈)(𝑁‘{𝑍}))) ∩ (𝑀‘((𝑁‘{(𝑋 − 𝑍)})(LSSum‘𝑈)(𝑁‘{𝑌}))))) |
34 | | hdmap1l6.c |
. . . . . 6
⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) |
35 | | eqid 2738 |
. . . . . 6
⊢
(LSSum‘𝐶) =
(LSSum‘𝐶) |
36 | 1, 2, 3, 4, 22, 34, 35, 5, 17, 21 | mapdlsm 39678 |
. . . . 5
⊢ (𝜑 → (𝑀‘((𝑁‘{(𝑋 − 𝑌)})(LSSum‘𝑈)(𝑁‘{𝑍}))) = ((𝑀‘(𝑁‘{(𝑋 − 𝑌)}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑍})))) |
37 | 1, 2, 3, 4, 22, 34, 35, 5, 28, 30 | mapdlsm 39678 |
. . . . 5
⊢ (𝜑 → (𝑀‘((𝑁‘{(𝑋 − 𝑍)})(LSSum‘𝑈)(𝑁‘{𝑌}))) = ((𝑀‘(𝑁‘{(𝑋 − 𝑍)}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌})))) |
38 | 36, 37 | ineq12d 4147 |
. . . 4
⊢ (𝜑 → ((𝑀‘((𝑁‘{(𝑋 − 𝑌)})(LSSum‘𝑈)(𝑁‘{𝑍}))) ∩ (𝑀‘((𝑁‘{(𝑋 − 𝑍)})(LSSum‘𝑈)(𝑁‘{𝑌})))) = (((𝑀‘(𝑁‘{(𝑋 − 𝑌)}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑍}))) ∩ ((𝑀‘(𝑁‘{(𝑋 − 𝑍)}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))))) |
39 | | hdmap1l6.fg |
. . . . . . . 8
⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑌〉) = 𝐺) |
40 | | hdmap1l6c.o |
. . . . . . . . 9
⊢ 0 =
(0g‘𝑈) |
41 | | hdmap1l6.d |
. . . . . . . . 9
⊢ 𝐷 = (Base‘𝐶) |
42 | | hdmap1l6.r |
. . . . . . . . 9
⊢ 𝑅 = (-g‘𝐶) |
43 | | hdmap1l6.l |
. . . . . . . . 9
⊢ 𝐿 = (LSpan‘𝐶) |
44 | | hdmap1l6.i |
. . . . . . . . 9
⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) |
45 | | hdmap1l6.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ 𝐷) |
46 | | hdmap1l6.mn |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐿‘{𝐹})) |
47 | 1, 3, 5 | dvhlvec 39123 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ∈ LVec) |
48 | | hdmap1l6.yz |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) |
49 | | hdmap1l6e.xn |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) |
50 | 11, 40, 15, 47, 10, 18, 8, 48, 49 | lspindp2 20397 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}) ∧ ¬ 𝑍 ∈ (𝑁‘{𝑋, 𝑌}))) |
51 | 50 | simpld 495 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) |
52 | 1, 3, 11, 40, 15, 34, 41, 43, 2, 44, 5, 45, 46, 51, 7, 10 | hdmap1cl 39818 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑌〉) ∈ 𝐷) |
53 | 39, 52 | eqeltrrd 2840 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ 𝐷) |
54 | 1, 3, 11, 12, 40, 15, 34, 41, 42, 43, 2, 44, 5, 7, 45, 9, 53, 51, 46 | hdmap1eq 39815 |
. . . . . . . 8
⊢ (𝜑 → ((𝐼‘〈𝑋, 𝐹, 𝑌〉) = 𝐺 ↔ ((𝑀‘(𝑁‘{𝑌})) = (𝐿‘{𝐺}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐿‘{(𝐹𝑅𝐺)})))) |
55 | 39, 54 | mpbid 231 |
. . . . . . 7
⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑌})) = (𝐿‘{𝐺}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐿‘{(𝐹𝑅𝐺)}))) |
56 | 55 | simprd 496 |
. . . . . 6
⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐿‘{(𝐹𝑅𝐺)})) |
57 | | hdmap1l6.fe |
. . . . . . . 8
⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑍〉) = 𝐸) |
58 | 11, 40, 15, 47, 9, 19, 8, 48, 49 | lspindp1 20395 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁‘{𝑋}) ≠ (𝑁‘{𝑍}) ∧ ¬ 𝑌 ∈ (𝑁‘{𝑋, 𝑍}))) |
59 | 58 | simpld 495 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍})) |
60 | 1, 3, 11, 40, 15, 34, 41, 43, 2, 44, 5, 45, 46, 59, 7, 19 | hdmap1cl 39818 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑍〉) ∈ 𝐷) |
61 | 57, 60 | eqeltrrd 2840 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ 𝐷) |
62 | 1, 3, 11, 12, 40, 15, 34, 41, 42, 43, 2, 44, 5, 7, 45, 18, 61, 59, 46 | hdmap1eq 39815 |
. . . . . . . 8
⊢ (𝜑 → ((𝐼‘〈𝑋, 𝐹, 𝑍〉) = 𝐸 ↔ ((𝑀‘(𝑁‘{𝑍})) = (𝐿‘{𝐸}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑍)})) = (𝐿‘{(𝐹𝑅𝐸)})))) |
63 | 57, 62 | mpbid 231 |
. . . . . . 7
⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑍})) = (𝐿‘{𝐸}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑍)})) = (𝐿‘{(𝐹𝑅𝐸)}))) |
64 | 63 | simpld 495 |
. . . . . 6
⊢ (𝜑 → (𝑀‘(𝑁‘{𝑍})) = (𝐿‘{𝐸})) |
65 | 56, 64 | oveq12d 7293 |
. . . . 5
⊢ (𝜑 → ((𝑀‘(𝑁‘{(𝑋 − 𝑌)}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑍}))) = ((𝐿‘{(𝐹𝑅𝐺)})(LSSum‘𝐶)(𝐿‘{𝐸}))) |
66 | 63 | simprd 496 |
. . . . . 6
⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑍)})) = (𝐿‘{(𝐹𝑅𝐸)})) |
67 | 55 | simpld 495 |
. . . . . 6
⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌})) = (𝐿‘{𝐺})) |
68 | 66, 67 | oveq12d 7293 |
. . . . 5
⊢ (𝜑 → ((𝑀‘(𝑁‘{(𝑋 − 𝑍)}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) = ((𝐿‘{(𝐹𝑅𝐸)})(LSSum‘𝐶)(𝐿‘{𝐺}))) |
69 | 65, 68 | ineq12d 4147 |
. . . 4
⊢ (𝜑 → (((𝑀‘(𝑁‘{(𝑋 − 𝑌)}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑍}))) ∩ ((𝑀‘(𝑁‘{(𝑋 − 𝑍)}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌})))) = (((𝐿‘{(𝐹𝑅𝐺)})(LSSum‘𝐶)(𝐿‘{𝐸})) ∩ ((𝐿‘{(𝐹𝑅𝐸)})(LSSum‘𝐶)(𝐿‘{𝐺})))) |
70 | 38, 69 | eqtrd 2778 |
. . 3
⊢ (𝜑 → ((𝑀‘((𝑁‘{(𝑋 − 𝑌)})(LSSum‘𝑈)(𝑁‘{𝑍}))) ∩ (𝑀‘((𝑁‘{(𝑋 − 𝑍)})(LSSum‘𝑈)(𝑁‘{𝑌})))) = (((𝐿‘{(𝐹𝑅𝐺)})(LSSum‘𝐶)(𝐿‘{𝐸})) ∩ ((𝐿‘{(𝐹𝑅𝐸)})(LSSum‘𝐶)(𝐿‘{𝐺})))) |
71 | 33, 70 | eqtrd 2778 |
. 2
⊢ (𝜑 → (𝑀‘(((𝑁‘{(𝑋 − 𝑌)})(LSSum‘𝑈)(𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑍)})(LSSum‘𝑈)(𝑁‘{𝑌})))) = (((𝐿‘{(𝐹𝑅𝐺)})(LSSum‘𝐶)(𝐿‘{𝐸})) ∩ ((𝐿‘{(𝐹𝑅𝐸)})(LSSum‘𝐶)(𝐿‘{𝐺})))) |
72 | | hdmap1l6.p |
. . . 4
⊢ + =
(+g‘𝑈) |
73 | 11, 12, 40, 22, 15, 47, 8, 49, 48, 9, 18, 72 | baerlem5a 39728 |
. . 3
⊢ (𝜑 → (𝑁‘{(𝑋 − (𝑌 + 𝑍))}) = (((𝑁‘{(𝑋 − 𝑌)})(LSSum‘𝑈)(𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑍)})(LSSum‘𝑈)(𝑁‘{𝑌})))) |
74 | 73 | fveq2d 6778 |
. 2
⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − (𝑌 + 𝑍))})) = (𝑀‘(((𝑁‘{(𝑋 − 𝑌)})(LSSum‘𝑈)(𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑍)})(LSSum‘𝑈)(𝑁‘{𝑌}))))) |
75 | | hdmap1l6.q |
. . 3
⊢ 𝑄 = (0g‘𝐶) |
76 | 1, 34, 5 | lcdlvec 39605 |
. . 3
⊢ (𝜑 → 𝐶 ∈ LVec) |
77 | 1, 2, 3, 11, 15, 34, 41, 43, 5, 45, 46, 8, 10, 53, 67, 19, 61, 64, 49 | mapdindp 39685 |
. . 3
⊢ (𝜑 → ¬ 𝐹 ∈ (𝐿‘{𝐺, 𝐸})) |
78 | 1, 2, 3, 11, 15, 34, 41, 43, 5, 53, 67, 10, 19, 61, 64, 48 | mapdncol 39684 |
. . 3
⊢ (𝜑 → (𝐿‘{𝐺}) ≠ (𝐿‘{𝐸})) |
79 | 1, 2, 3, 11, 15, 34, 41, 43, 5, 53, 67, 40, 75, 9 | mapdn0 39683 |
. . 3
⊢ (𝜑 → 𝐺 ∈ (𝐷 ∖ {𝑄})) |
80 | 1, 2, 3, 11, 15, 34, 41, 43, 5, 61, 64, 40, 75, 18 | mapdn0 39683 |
. . 3
⊢ (𝜑 → 𝐸 ∈ (𝐷 ∖ {𝑄})) |
81 | | hdmap1l6.a |
. . 3
⊢ ✚ =
(+g‘𝐶) |
82 | 41, 42, 75, 35, 43, 76, 45, 77, 78, 79, 80, 81 | baerlem5a 39728 |
. 2
⊢ (𝜑 → (𝐿‘{(𝐹𝑅(𝐺 ✚ 𝐸))}) = (((𝐿‘{(𝐹𝑅𝐺)})(LSSum‘𝐶)(𝐿‘{𝐸})) ∩ ((𝐿‘{(𝐹𝑅𝐸)})(LSSum‘𝐶)(𝐿‘{𝐺})))) |
83 | 71, 74, 82 | 3eqtr4d 2788 |
1
⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − (𝑌 + 𝑍))})) = (𝐿‘{(𝐹𝑅(𝐺 ✚ 𝐸))})) |