Proof of Theorem mapdheq4lem
| Step | Hyp | Ref
| Expression |
| 1 | | mapdh.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
| 2 | | mapdh.m |
. . . 4
⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) |
| 3 | | mapdh.u |
. . . 4
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
| 4 | | eqid 2737 |
. . . 4
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
| 5 | | mapdh.k |
. . . 4
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 6 | 1, 3, 5 | dvhlmod 41112 |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ LMod) |
| 7 | | mapdhe4.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) |
| 8 | 7 | eldifad 3963 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
| 9 | | mapdh.v |
. . . . . . 7
⊢ 𝑉 = (Base‘𝑈) |
| 10 | | mapdh.n |
. . . . . . 7
⊢ 𝑁 = (LSpan‘𝑈) |
| 11 | 9, 4, 10 | lspsncl 20975 |
. . . . . 6
⊢ ((𝑈 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈)) |
| 12 | 6, 8, 11 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈)) |
| 13 | | mapdhe.z |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) |
| 14 | 13 | eldifad 3963 |
. . . . . 6
⊢ (𝜑 → 𝑍 ∈ 𝑉) |
| 15 | 9, 4, 10 | lspsncl 20975 |
. . . . . 6
⊢ ((𝑈 ∈ LMod ∧ 𝑍 ∈ 𝑉) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑈)) |
| 16 | 6, 14, 15 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑈)) |
| 17 | | eqid 2737 |
. . . . . 6
⊢
(LSSum‘𝑈) =
(LSSum‘𝑈) |
| 18 | 4, 17 | lsmcl 21082 |
. . . . 5
⊢ ((𝑈 ∈ LMod ∧ (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈) ∧ (𝑁‘{𝑍}) ∈ (LSubSp‘𝑈)) → ((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍})) ∈ (LSubSp‘𝑈)) |
| 19 | 6, 12, 16, 18 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → ((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍})) ∈ (LSubSp‘𝑈)) |
| 20 | | mapdhcl.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) |
| 21 | 20 | eldifad 3963 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
| 22 | | mapdh.s |
. . . . . . . 8
⊢ − =
(-g‘𝑈) |
| 23 | 9, 22 | lmodvsubcl 20905 |
. . . . . . 7
⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 − 𝑌) ∈ 𝑉) |
| 24 | 6, 21, 8, 23 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝑉) |
| 25 | 9, 4, 10 | lspsncl 20975 |
. . . . . 6
⊢ ((𝑈 ∈ LMod ∧ (𝑋 − 𝑌) ∈ 𝑉) → (𝑁‘{(𝑋 − 𝑌)}) ∈ (LSubSp‘𝑈)) |
| 26 | 6, 24, 25 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝑁‘{(𝑋 − 𝑌)}) ∈ (LSubSp‘𝑈)) |
| 27 | 9, 22 | lmodvsubcl 20905 |
. . . . . . 7
⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉) → (𝑋 − 𝑍) ∈ 𝑉) |
| 28 | 6, 21, 14, 27 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → (𝑋 − 𝑍) ∈ 𝑉) |
| 29 | 9, 4, 10 | lspsncl 20975 |
. . . . . 6
⊢ ((𝑈 ∈ LMod ∧ (𝑋 − 𝑍) ∈ 𝑉) → (𝑁‘{(𝑋 − 𝑍)}) ∈ (LSubSp‘𝑈)) |
| 30 | 6, 28, 29 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝑁‘{(𝑋 − 𝑍)}) ∈ (LSubSp‘𝑈)) |
| 31 | 4, 17 | lsmcl 21082 |
. . . . 5
⊢ ((𝑈 ∈ LMod ∧ (𝑁‘{(𝑋 − 𝑌)}) ∈ (LSubSp‘𝑈) ∧ (𝑁‘{(𝑋 − 𝑍)}) ∈ (LSubSp‘𝑈)) → ((𝑁‘{(𝑋 − 𝑌)})(LSSum‘𝑈)(𝑁‘{(𝑋 − 𝑍)})) ∈ (LSubSp‘𝑈)) |
| 32 | 6, 26, 30, 31 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → ((𝑁‘{(𝑋 − 𝑌)})(LSSum‘𝑈)(𝑁‘{(𝑋 − 𝑍)})) ∈ (LSubSp‘𝑈)) |
| 33 | 1, 2, 3, 4, 5, 19,
32 | mapdin 41664 |
. . 3
⊢ (𝜑 → (𝑀‘(((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑌)})(LSSum‘𝑈)(𝑁‘{(𝑋 − 𝑍)})))) = ((𝑀‘((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍}))) ∩ (𝑀‘((𝑁‘{(𝑋 − 𝑌)})(LSSum‘𝑈)(𝑁‘{(𝑋 − 𝑍)}))))) |
| 34 | | mapdh.c |
. . . . . 6
⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) |
| 35 | | eqid 2737 |
. . . . . 6
⊢
(LSSum‘𝐶) =
(LSSum‘𝐶) |
| 36 | 1, 2, 3, 4, 17, 34, 35, 5, 12, 16 | mapdlsm 41666 |
. . . . 5
⊢ (𝜑 → (𝑀‘((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍}))) = ((𝑀‘(𝑁‘{𝑌}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑍})))) |
| 37 | | mapdh.eg |
. . . . . . . 8
⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑌〉) = 𝐺) |
| 38 | | mapdh.q |
. . . . . . . . 9
⊢ 𝑄 = (0g‘𝐶) |
| 39 | | mapdh.i |
. . . . . . . . 9
⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd
‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))))) |
| 40 | | mapdhc.o |
. . . . . . . . 9
⊢ 0 =
(0g‘𝑈) |
| 41 | | mapdh.d |
. . . . . . . . 9
⊢ 𝐷 = (Base‘𝐶) |
| 42 | | mapdh.r |
. . . . . . . . 9
⊢ 𝑅 = (-g‘𝐶) |
| 43 | | mapdh.j |
. . . . . . . . 9
⊢ 𝐽 = (LSpan‘𝐶) |
| 44 | | mapdhc.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ 𝐷) |
| 45 | | mapdh.mn |
. . . . . . . . 9
⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) |
| 46 | 1, 3, 5 | dvhlvec 41111 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ∈ LVec) |
| 47 | | mapdh.yz |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) |
| 48 | | mapdh.xn |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) |
| 49 | 9, 40, 10, 46, 8, 13, 21, 47, 48 | lspindp2 21137 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}) ∧ ¬ 𝑍 ∈ (𝑁‘{𝑋, 𝑌}))) |
| 50 | 49 | simpld 494 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) |
| 51 | 38, 39, 1, 2, 3, 9, 22, 40, 10, 34, 41, 42, 43, 5, 44, 45, 20, 8, 50 | mapdhcl 41729 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑌〉) ∈ 𝐷) |
| 52 | 37, 51 | eqeltrrd 2842 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ 𝐷) |
| 53 | 38, 39, 1, 2, 3, 9, 22, 40, 10, 34, 41, 42, 43, 5, 44, 45, 20, 7, 52, 50 | mapdheq 41730 |
. . . . . . . 8
⊢ (𝜑 → ((𝐼‘〈𝑋, 𝐹, 𝑌〉) = 𝐺 ↔ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝐺}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐹𝑅𝐺)})))) |
| 54 | 37, 53 | mpbid 232 |
. . . . . . 7
⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝐺}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐹𝑅𝐺)}))) |
| 55 | 54 | simpld 494 |
. . . . . 6
⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝐺})) |
| 56 | | mapdh.ee |
. . . . . . . 8
⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑍〉) = 𝐸) |
| 57 | 9, 40, 10, 46, 7, 14, 21, 47, 48 | lspindp1 21135 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁‘{𝑋}) ≠ (𝑁‘{𝑍}) ∧ ¬ 𝑌 ∈ (𝑁‘{𝑋, 𝑍}))) |
| 58 | 57 | simpld 494 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍})) |
| 59 | 38, 39, 1, 2, 3, 9, 22, 40, 10, 34, 41, 42, 43, 5, 44, 45, 20, 14, 58 | mapdhcl 41729 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑍〉) ∈ 𝐷) |
| 60 | 56, 59 | eqeltrrd 2842 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ 𝐷) |
| 61 | 38, 39, 1, 2, 3, 9, 22, 40, 10, 34, 41, 42, 43, 5, 44, 45, 20, 13, 60, 58 | mapdheq 41730 |
. . . . . . . 8
⊢ (𝜑 → ((𝐼‘〈𝑋, 𝐹, 𝑍〉) = 𝐸 ↔ ((𝑀‘(𝑁‘{𝑍})) = (𝐽‘{𝐸}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑍)})) = (𝐽‘{(𝐹𝑅𝐸)})))) |
| 62 | 56, 61 | mpbid 232 |
. . . . . . 7
⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑍})) = (𝐽‘{𝐸}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑍)})) = (𝐽‘{(𝐹𝑅𝐸)}))) |
| 63 | 62 | simpld 494 |
. . . . . 6
⊢ (𝜑 → (𝑀‘(𝑁‘{𝑍})) = (𝐽‘{𝐸})) |
| 64 | 55, 63 | oveq12d 7449 |
. . . . 5
⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑌}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑍}))) = ((𝐽‘{𝐺})(LSSum‘𝐶)(𝐽‘{𝐸}))) |
| 65 | 36, 64 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → (𝑀‘((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍}))) = ((𝐽‘{𝐺})(LSSum‘𝐶)(𝐽‘{𝐸}))) |
| 66 | 1, 2, 3, 4, 17, 34, 35, 5, 26, 30 | mapdlsm 41666 |
. . . . 5
⊢ (𝜑 → (𝑀‘((𝑁‘{(𝑋 − 𝑌)})(LSSum‘𝑈)(𝑁‘{(𝑋 − 𝑍)}))) = ((𝑀‘(𝑁‘{(𝑋 − 𝑌)}))(LSSum‘𝐶)(𝑀‘(𝑁‘{(𝑋 − 𝑍)})))) |
| 67 | 54 | simprd 495 |
. . . . . 6
⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐹𝑅𝐺)})) |
| 68 | 62 | simprd 495 |
. . . . . 6
⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑍)})) = (𝐽‘{(𝐹𝑅𝐸)})) |
| 69 | 67, 68 | oveq12d 7449 |
. . . . 5
⊢ (𝜑 → ((𝑀‘(𝑁‘{(𝑋 − 𝑌)}))(LSSum‘𝐶)(𝑀‘(𝑁‘{(𝑋 − 𝑍)}))) = ((𝐽‘{(𝐹𝑅𝐺)})(LSSum‘𝐶)(𝐽‘{(𝐹𝑅𝐸)}))) |
| 70 | 66, 69 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → (𝑀‘((𝑁‘{(𝑋 − 𝑌)})(LSSum‘𝑈)(𝑁‘{(𝑋 − 𝑍)}))) = ((𝐽‘{(𝐹𝑅𝐺)})(LSSum‘𝐶)(𝐽‘{(𝐹𝑅𝐸)}))) |
| 71 | 65, 70 | ineq12d 4221 |
. . 3
⊢ (𝜑 → ((𝑀‘((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍}))) ∩ (𝑀‘((𝑁‘{(𝑋 − 𝑌)})(LSSum‘𝑈)(𝑁‘{(𝑋 − 𝑍)})))) = (((𝐽‘{𝐺})(LSSum‘𝐶)(𝐽‘{𝐸})) ∩ ((𝐽‘{(𝐹𝑅𝐺)})(LSSum‘𝐶)(𝐽‘{(𝐹𝑅𝐸)})))) |
| 72 | 33, 71 | eqtrd 2777 |
. 2
⊢ (𝜑 → (𝑀‘(((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑌)})(LSSum‘𝑈)(𝑁‘{(𝑋 − 𝑍)})))) = (((𝐽‘{𝐺})(LSSum‘𝐶)(𝐽‘{𝐸})) ∩ ((𝐽‘{(𝐹𝑅𝐺)})(LSSum‘𝐶)(𝐽‘{(𝐹𝑅𝐸)})))) |
| 73 | 9, 22, 40, 17, 10, 46, 21, 48, 47, 7, 13 | baerlem3 41715 |
. . 3
⊢ (𝜑 → (𝑁‘{(𝑌 − 𝑍)}) = (((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑌)})(LSSum‘𝑈)(𝑁‘{(𝑋 − 𝑍)})))) |
| 74 | 73 | fveq2d 6910 |
. 2
⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑌 − 𝑍)})) = (𝑀‘(((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑌)})(LSSum‘𝑈)(𝑁‘{(𝑋 − 𝑍)}))))) |
| 75 | | eqid 2737 |
. . 3
⊢
(0g‘𝐶) = (0g‘𝐶) |
| 76 | 1, 34, 5 | lcdlvec 41593 |
. . 3
⊢ (𝜑 → 𝐶 ∈ LVec) |
| 77 | 1, 2, 3, 9, 10, 34, 41, 43, 5, 44, 45, 21, 8, 52, 55, 14, 60, 63, 48 | mapdindp 41673 |
. . 3
⊢ (𝜑 → ¬ 𝐹 ∈ (𝐽‘{𝐺, 𝐸})) |
| 78 | 1, 2, 3, 9, 10, 34, 41, 43, 5, 52, 55, 8, 14, 60, 63, 47 | mapdncol 41672 |
. . 3
⊢ (𝜑 → (𝐽‘{𝐺}) ≠ (𝐽‘{𝐸})) |
| 79 | 1, 2, 3, 9, 10, 34, 41, 43, 5, 52, 55, 40, 75, 7 | mapdn0 41671 |
. . 3
⊢ (𝜑 → 𝐺 ∈ (𝐷 ∖ {(0g‘𝐶)})) |
| 80 | 1, 2, 3, 9, 10, 34, 41, 43, 5, 60, 63, 40, 75, 13 | mapdn0 41671 |
. . 3
⊢ (𝜑 → 𝐸 ∈ (𝐷 ∖ {(0g‘𝐶)})) |
| 81 | 41, 42, 75, 35, 43, 76, 44, 77, 78, 79, 80 | baerlem3 41715 |
. 2
⊢ (𝜑 → (𝐽‘{(𝐺𝑅𝐸)}) = (((𝐽‘{𝐺})(LSSum‘𝐶)(𝐽‘{𝐸})) ∩ ((𝐽‘{(𝐹𝑅𝐺)})(LSSum‘𝐶)(𝐽‘{(𝐹𝑅𝐸)})))) |
| 82 | 72, 74, 81 | 3eqtr4d 2787 |
1
⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑌 − 𝑍)})) = (𝐽‘{(𝐺𝑅𝐸)})) |