Proof of Theorem baerlem5blem1
| Step | Hyp | Ref
| Expression |
| 1 | | baerlem3.v |
. . . . . . . 8
⊢ 𝑉 = (Base‘𝑊) |
| 2 | | baerlem3.p |
. . . . . . . 8
⊢ + =
(+g‘𝑊) |
| 3 | | baerlem3.r |
. . . . . . . 8
⊢ 𝑅 = (Scalar‘𝑊) |
| 4 | | baerlem3.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑅) |
| 5 | | baerlem3.t |
. . . . . . . 8
⊢ · = (
·𝑠 ‘𝑊) |
| 6 | | eqid 2737 |
. . . . . . . 8
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
| 7 | | baerlem3.w |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ LVec) |
| 8 | | baerlem3.n |
. . . . . . . . 9
⊢ 𝑁 = (LSpan‘𝑊) |
| 9 | | lveclmod 21105 |
. . . . . . . . . 10
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
| 10 | 7, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ LMod) |
| 11 | | baerlem3.y |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) |
| 12 | 11 | eldifad 3963 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
| 13 | | baerlem3.z |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) |
| 14 | 13 | eldifad 3963 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ∈ 𝑉) |
| 15 | 1, 6, 8, 10, 12, 14 | lspprcl 20976 |
. . . . . . . 8
⊢ (𝜑 → (𝑁‘{𝑌, 𝑍}) ∈ (LSubSp‘𝑊)) |
| 16 | | baerlem3.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
| 17 | | baerlem3.c |
. . . . . . . 8
⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) |
| 18 | | baerlem5b.a1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑎 ∈ 𝐵) |
| 19 | | baerlem5b.b1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑏 ∈ 𝐵) |
| 20 | 1, 2, 5, 3, 4, 8, 10, 18, 19, 12, 14 | lsppreli 21089 |
. . . . . . . 8
⊢ (𝜑 → ((𝑎 · 𝑌) + (𝑏 · 𝑍)) ∈ (𝑁‘{𝑌, 𝑍})) |
| 21 | 3 | lmodring 20866 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ LMod → 𝑅 ∈ Ring) |
| 22 | 10, 21 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 23 | | ringgrp 20235 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
| 24 | 22, 23 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Grp) |
| 25 | | baerlem5b.d1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑑 ∈ 𝐵) |
| 26 | | baerlem3.i |
. . . . . . . . . . 11
⊢ 𝐼 = (invg‘𝑅) |
| 27 | 4, 26 | grpinvcl 19005 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Grp ∧ 𝑑 ∈ 𝐵) → (𝐼‘𝑑) ∈ 𝐵) |
| 28 | 24, 25, 27 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝐼‘𝑑) ∈ 𝐵) |
| 29 | 1, 2, 5, 3, 4, 8, 10, 28, 28, 12, 14 | lsppreli 21089 |
. . . . . . . 8
⊢ (𝜑 → (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍)) ∈ (𝑁‘{𝑌, 𝑍})) |
| 30 | | baerlem3.q |
. . . . . . . . . 10
⊢ 𝑄 = (0g‘𝑅) |
| 31 | 3, 4, 30 | lmod0cl 20886 |
. . . . . . . . 9
⊢ (𝑊 ∈ LMod → 𝑄 ∈ 𝐵) |
| 32 | 10, 31 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ∈ 𝐵) |
| 33 | | baerlem5b.e1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑒 ∈ 𝐵) |
| 34 | | baerlem3.a |
. . . . . . . . . 10
⊢ ⨣ =
(+g‘𝑅) |
| 35 | 3, 4, 34 | lmodacl 20870 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) → (𝑑 ⨣ 𝑒) ∈ 𝐵) |
| 36 | 10, 25, 33, 35 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (𝑑 ⨣ 𝑒) ∈ 𝐵) |
| 37 | 1, 3, 5, 4 | lmodvscl 20876 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ 𝑎 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) → (𝑎 · 𝑌) ∈ 𝑉) |
| 38 | 10, 18, 12, 37 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑎 · 𝑌) ∈ 𝑉) |
| 39 | 1, 3, 5, 4 | lmodvscl 20876 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ 𝑏 ∈ 𝐵 ∧ 𝑍 ∈ 𝑉) → (𝑏 · 𝑍) ∈ 𝑉) |
| 40 | 10, 19, 14, 39 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑏 · 𝑍) ∈ 𝑉) |
| 41 | 1, 2 | lmodvacl 20873 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ (𝑎 · 𝑌) ∈ 𝑉 ∧ (𝑏 · 𝑍) ∈ 𝑉) → ((𝑎 · 𝑌) + (𝑏 · 𝑍)) ∈ 𝑉) |
| 42 | 10, 38, 40, 41 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑎 · 𝑌) + (𝑏 · 𝑍)) ∈ 𝑉) |
| 43 | | baerlem3.o |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘𝑊) |
| 44 | 1, 2, 43 | lmod0vlid 20890 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ LMod ∧ ((𝑎 · 𝑌) + (𝑏 · 𝑍)) ∈ 𝑉) → ( 0 + ((𝑎 · 𝑌) + (𝑏 · 𝑍))) = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) |
| 45 | 10, 42, 44 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → ( 0 + ((𝑎 · 𝑌) + (𝑏 · 𝑍))) = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) |
| 46 | 1, 3, 5, 30, 43 | lmod0vs 20893 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑄 · 𝑋) = 0 ) |
| 47 | 10, 16, 46 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑄 · 𝑋) = 0 ) |
| 48 | 47 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑄 · 𝑋) + ((𝑎 · 𝑌) + (𝑏 · 𝑍))) = ( 0 + ((𝑎 · 𝑌) + (𝑏 · 𝑍)))) |
| 49 | | baerlem5b.j1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) |
| 50 | 45, 48, 49 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑄 · 𝑋) + ((𝑎 · 𝑌) + (𝑏 · 𝑍))) = 𝑗) |
| 51 | | baerlem3.m |
. . . . . . . . . . . . 13
⊢ − =
(-g‘𝑊) |
| 52 | 1, 2 | lmodvacl 20873 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉) → (𝑌 + 𝑍) ∈ 𝑉) |
| 53 | 10, 12, 14, 52 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑌 + 𝑍) ∈ 𝑉) |
| 54 | 1, 5, 3, 4, 51, 10, 25, 16, 53 | lmodsubdi 20917 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑑 · (𝑋 − (𝑌 + 𝑍))) = ((𝑑 · 𝑋) − (𝑑 · (𝑌 + 𝑍)))) |
| 55 | 1, 3, 5, 4 | lmodvscl 20876 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LMod ∧ 𝑑 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) → (𝑑 · 𝑋) ∈ 𝑉) |
| 56 | 10, 25, 16, 55 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑑 · 𝑋) ∈ 𝑉) |
| 57 | 1, 2, 51, 5, 3, 4,
26, 10, 25, 56, 53 | lmodsubvs 20916 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑑 · 𝑋) − (𝑑 · (𝑌 + 𝑍))) = ((𝑑 · 𝑋) + ((𝐼‘𝑑) · (𝑌 + 𝑍)))) |
| 58 | 1, 2, 3, 5, 4 | lmodvsdi 20883 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LMod ∧ ((𝐼‘𝑑) ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉)) → ((𝐼‘𝑑) · (𝑌 + 𝑍)) = (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍))) |
| 59 | 10, 28, 12, 14, 58 | syl13anc 1374 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐼‘𝑑) · (𝑌 + 𝑍)) = (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍))) |
| 60 | 59 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑑 · 𝑋) + ((𝐼‘𝑑) · (𝑌 + 𝑍))) = ((𝑑 · 𝑋) + (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍)))) |
| 61 | 54, 57, 60 | 3eqtrd 2781 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑑 · (𝑋 − (𝑌 + 𝑍))) = ((𝑑 · 𝑋) + (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍)))) |
| 62 | 61 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑑 · (𝑋 − (𝑌 + 𝑍))) + (𝑒 · 𝑋)) = (((𝑑 · 𝑋) + (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍))) + (𝑒 · 𝑋))) |
| 63 | | baerlem5b.j2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑗 = ((𝑑 · (𝑋 − (𝑌 + 𝑍))) + (𝑒 · 𝑋))) |
| 64 | 1, 2, 3, 5, 4, 34 | lmodvsdir 20884 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉)) → ((𝑑 ⨣ 𝑒) · 𝑋) = ((𝑑 · 𝑋) + (𝑒 · 𝑋))) |
| 65 | 10, 25, 33, 16, 64 | syl13anc 1374 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑑 ⨣ 𝑒) · 𝑋) = ((𝑑 · 𝑋) + (𝑒 · 𝑋))) |
| 66 | 65 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑑 ⨣ 𝑒) · 𝑋) + (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍))) = (((𝑑 · 𝑋) + (𝑒 · 𝑋)) + (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍)))) |
| 67 | | lmodabl 20907 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Abel) |
| 68 | 10, 67 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 ∈ Abel) |
| 69 | 1, 3, 5, 4 | lmodvscl 20876 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ 𝑒 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) → (𝑒 · 𝑋) ∈ 𝑉) |
| 70 | 10, 33, 16, 69 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑒 · 𝑋) ∈ 𝑉) |
| 71 | 1, 3, 5, 4 | lmodvscl 20876 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LMod ∧ (𝐼‘𝑑) ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) → ((𝐼‘𝑑) · 𝑌) ∈ 𝑉) |
| 72 | 10, 28, 12, 71 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐼‘𝑑) · 𝑌) ∈ 𝑉) |
| 73 | 1, 3, 5, 4 | lmodvscl 20876 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LMod ∧ (𝐼‘𝑑) ∈ 𝐵 ∧ 𝑍 ∈ 𝑉) → ((𝐼‘𝑑) · 𝑍) ∈ 𝑉) |
| 74 | 10, 28, 14, 73 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐼‘𝑑) · 𝑍) ∈ 𝑉) |
| 75 | 1, 2 | lmodvacl 20873 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ ((𝐼‘𝑑) · 𝑌) ∈ 𝑉 ∧ ((𝐼‘𝑑) · 𝑍) ∈ 𝑉) → (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍)) ∈ 𝑉) |
| 76 | 10, 72, 74, 75 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍)) ∈ 𝑉) |
| 77 | 1, 2, 68, 56, 70, 76 | abl32 19821 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑑 · 𝑋) + (𝑒 · 𝑋)) + (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍))) = (((𝑑 · 𝑋) + (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍))) + (𝑒 · 𝑋))) |
| 78 | 66, 77 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑑 ⨣ 𝑒) · 𝑋) + (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍))) = (((𝑑 · 𝑋) + (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍))) + (𝑒 · 𝑋))) |
| 79 | 62, 63, 78 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ (𝜑 → 𝑗 = (((𝑑 ⨣ 𝑒) · 𝑋) + (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍)))) |
| 80 | 50, 79 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → ((𝑄 · 𝑋) + ((𝑎 · 𝑌) + (𝑏 · 𝑍))) = (((𝑑 ⨣ 𝑒) · 𝑋) + (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍)))) |
| 81 | 1, 2, 3, 4, 5, 6, 7, 15, 16, 17, 20, 29, 32, 36, 80 | lvecindp 21140 |
. . . . . . 7
⊢ (𝜑 → (𝑄 = (𝑑 ⨣ 𝑒) ∧ ((𝑎 · 𝑌) + (𝑏 · 𝑍)) = (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍)))) |
| 82 | 81 | simpld 494 |
. . . . . 6
⊢ (𝜑 → 𝑄 = (𝑑 ⨣ 𝑒)) |
| 83 | 82 | oveq1d 7446 |
. . . . 5
⊢ (𝜑 → (𝑄 · 𝑋) = ((𝑑 ⨣ 𝑒) · 𝑋)) |
| 84 | 83, 47 | eqtr3d 2779 |
. . . 4
⊢ (𝜑 → ((𝑑 ⨣ 𝑒) · 𝑋) = 0 ) |
| 85 | 84 | oveq1d 7446 |
. . 3
⊢ (𝜑 → (((𝑑 ⨣ 𝑒) · 𝑋) + (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍))) = ( 0 + (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍)))) |
| 86 | 1, 2, 43 | lmod0vlid 20890 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍)) ∈ 𝑉) → ( 0 + (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍))) = (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍))) |
| 87 | 10, 76, 86 | syl2anc 584 |
. . 3
⊢ (𝜑 → ( 0 + (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍))) = (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍))) |
| 88 | 85, 87 | eqtrd 2777 |
. 2
⊢ (𝜑 → (((𝑑 ⨣ 𝑒) · 𝑋) + (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍))) = (((𝐼‘𝑑) · 𝑌) + ((𝐼‘𝑑) · 𝑍))) |
| 89 | 88, 79, 59 | 3eqtr4d 2787 |
1
⊢ (𝜑 → 𝑗 = ((𝐼‘𝑑) · (𝑌 + 𝑍))) |