Proof of Theorem lspprabs
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | lspprabs.w | . . . . . . 7
⊢ (𝜑 → 𝑊 ∈ LMod) | 
| 2 |  | eqid 2737 | . . . . . . . 8
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) | 
| 3 | 2 | lsssssubg 20956 | . . . . . . 7
⊢ (𝑊 ∈ LMod →
(LSubSp‘𝑊) ⊆
(SubGrp‘𝑊)) | 
| 4 | 1, 3 | syl 17 | . . . . . 6
⊢ (𝜑 → (LSubSp‘𝑊) ⊆ (SubGrp‘𝑊)) | 
| 5 |  | lspprabs.x | . . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝑉) | 
| 6 |  | lspprabs.v | . . . . . . . 8
⊢ 𝑉 = (Base‘𝑊) | 
| 7 |  | lspprabs.n | . . . . . . . 8
⊢ 𝑁 = (LSpan‘𝑊) | 
| 8 | 6, 2, 7 | lspsncl 20975 | . . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑊)) | 
| 9 | 1, 5, 8 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑊)) | 
| 10 | 4, 9 | sseldd 3984 | . . . . 5
⊢ (𝜑 → (𝑁‘{𝑋}) ∈ (SubGrp‘𝑊)) | 
| 11 |  | lspprabs.y | . . . . . . 7
⊢ (𝜑 → 𝑌 ∈ 𝑉) | 
| 12 | 6, 2, 7 | lspsncl 20975 | . . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊)) | 
| 13 | 1, 11, 12 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊)) | 
| 14 | 4, 13 | sseldd 3984 | . . . . 5
⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (SubGrp‘𝑊)) | 
| 15 |  | eqid 2737 | . . . . . 6
⊢
(LSSum‘𝑊) =
(LSSum‘𝑊) | 
| 16 | 15 | lsmub1 19675 | . . . . 5
⊢ (((𝑁‘{𝑋}) ∈ (SubGrp‘𝑊) ∧ (𝑁‘{𝑌}) ∈ (SubGrp‘𝑊)) → (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌}))) | 
| 17 | 10, 14, 16 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌}))) | 
| 18 | 2, 15 | lsmcl 21082 | . . . . . 6
⊢ ((𝑊 ∈ LMod ∧ (𝑁‘{𝑋}) ∈ (LSubSp‘𝑊) ∧ (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊)) → ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})) ∈ (LSubSp‘𝑊)) | 
| 19 | 1, 9, 13, 18 | syl3anc 1373 | . . . . 5
⊢ (𝜑 → ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})) ∈ (LSubSp‘𝑊)) | 
| 20 | 6, 7 | lspsnid 20991 | . . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ (𝑁‘{𝑋})) | 
| 21 | 1, 5, 20 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑋})) | 
| 22 | 6, 7 | lspsnid 20991 | . . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → 𝑌 ∈ (𝑁‘{𝑌})) | 
| 23 | 1, 11, 22 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑌})) | 
| 24 |  | lspprabs.p | . . . . . . 7
⊢  + =
(+g‘𝑊) | 
| 25 | 24, 15 | lsmelvali 19668 | . . . . . 6
⊢ ((((𝑁‘{𝑋}) ∈ (SubGrp‘𝑊) ∧ (𝑁‘{𝑌}) ∈ (SubGrp‘𝑊)) ∧ (𝑋 ∈ (𝑁‘{𝑋}) ∧ 𝑌 ∈ (𝑁‘{𝑌}))) → (𝑋 + 𝑌) ∈ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌}))) | 
| 26 | 10, 14, 21, 23, 25 | syl22anc 839 | . . . . 5
⊢ (𝜑 → (𝑋 + 𝑌) ∈ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌}))) | 
| 27 | 2, 7, 1, 19, 26 | ellspsn5 20994 | . . . 4
⊢ (𝜑 → (𝑁‘{(𝑋 + 𝑌)}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌}))) | 
| 28 | 6, 24 | lmodvacl 20873 | . . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉) | 
| 29 | 1, 5, 11, 28 | syl3anc 1373 | . . . . . . 7
⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝑉) | 
| 30 | 6, 2, 7 | lspsncl 20975 | . . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ (𝑋 + 𝑌) ∈ 𝑉) → (𝑁‘{(𝑋 + 𝑌)}) ∈ (LSubSp‘𝑊)) | 
| 31 | 1, 29, 30 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (𝑁‘{(𝑋 + 𝑌)}) ∈ (LSubSp‘𝑊)) | 
| 32 | 4, 31 | sseldd 3984 | . . . . 5
⊢ (𝜑 → (𝑁‘{(𝑋 + 𝑌)}) ∈ (SubGrp‘𝑊)) | 
| 33 | 4, 19 | sseldd 3984 | . . . . 5
⊢ (𝜑 → ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})) ∈ (SubGrp‘𝑊)) | 
| 34 | 15 | lsmlub 19682 | . . . . 5
⊢ (((𝑁‘{𝑋}) ∈ (SubGrp‘𝑊) ∧ (𝑁‘{(𝑋 + 𝑌)}) ∈ (SubGrp‘𝑊) ∧ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})) ∈ (SubGrp‘𝑊)) → (((𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})) ∧ (𝑁‘{(𝑋 + 𝑌)}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌}))) ↔ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)})) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})))) | 
| 35 | 10, 32, 33, 34 | syl3anc 1373 | . . . 4
⊢ (𝜑 → (((𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})) ∧ (𝑁‘{(𝑋 + 𝑌)}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌}))) ↔ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)})) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})))) | 
| 36 | 17, 27, 35 | mpbi2and 712 | . . 3
⊢ (𝜑 → ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)})) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌}))) | 
| 37 | 15 | lsmub1 19675 | . . . . 5
⊢ (((𝑁‘{𝑋}) ∈ (SubGrp‘𝑊) ∧ (𝑁‘{(𝑋 + 𝑌)}) ∈ (SubGrp‘𝑊)) → (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)}))) | 
| 38 | 10, 32, 37 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)}))) | 
| 39 | 2, 15 | lsmcl 21082 | . . . . . 6
⊢ ((𝑊 ∈ LMod ∧ (𝑁‘{𝑋}) ∈ (LSubSp‘𝑊) ∧ (𝑁‘{(𝑋 + 𝑌)}) ∈ (LSubSp‘𝑊)) → ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)})) ∈ (LSubSp‘𝑊)) | 
| 40 | 1, 9, 31, 39 | syl3anc 1373 | . . . . 5
⊢ (𝜑 → ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)})) ∈ (LSubSp‘𝑊)) | 
| 41 |  | eqid 2737 | . . . . . . 7
⊢
(-g‘𝑊) = (-g‘𝑊) | 
| 42 | 6, 7 | lspsnid 20991 | . . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ (𝑋 + 𝑌) ∈ 𝑉) → (𝑋 + 𝑌) ∈ (𝑁‘{(𝑋 + 𝑌)})) | 
| 43 | 1, 29, 42 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝑁‘{(𝑋 + 𝑌)})) | 
| 44 | 41, 15, 32, 10, 43, 21 | lsmelvalmi 19670 | . . . . . 6
⊢ (𝜑 → ((𝑋 + 𝑌)(-g‘𝑊)𝑋) ∈ ((𝑁‘{(𝑋 + 𝑌)})(LSSum‘𝑊)(𝑁‘{𝑋}))) | 
| 45 |  | lmodabl 20907 | . . . . . . . 8
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Abel) | 
| 46 | 1, 45 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝑊 ∈ Abel) | 
| 47 | 6, 24, 41 | ablpncan2 19833 | . . . . . . 7
⊢ ((𝑊 ∈ Abel ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝑋 + 𝑌)(-g‘𝑊)𝑋) = 𝑌) | 
| 48 | 46, 5, 11, 47 | syl3anc 1373 | . . . . . 6
⊢ (𝜑 → ((𝑋 + 𝑌)(-g‘𝑊)𝑋) = 𝑌) | 
| 49 | 15 | lsmcom 19876 | . . . . . . 7
⊢ ((𝑊 ∈ Abel ∧ (𝑁‘{(𝑋 + 𝑌)}) ∈ (SubGrp‘𝑊) ∧ (𝑁‘{𝑋}) ∈ (SubGrp‘𝑊)) → ((𝑁‘{(𝑋 + 𝑌)})(LSSum‘𝑊)(𝑁‘{𝑋})) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)}))) | 
| 50 | 46, 32, 10, 49 | syl3anc 1373 | . . . . . 6
⊢ (𝜑 → ((𝑁‘{(𝑋 + 𝑌)})(LSSum‘𝑊)(𝑁‘{𝑋})) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)}))) | 
| 51 | 44, 48, 50 | 3eltr3d 2855 | . . . . 5
⊢ (𝜑 → 𝑌 ∈ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)}))) | 
| 52 | 2, 7, 1, 40, 51 | ellspsn5 20994 | . . . 4
⊢ (𝜑 → (𝑁‘{𝑌}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)}))) | 
| 53 | 4, 40 | sseldd 3984 | . . . . 5
⊢ (𝜑 → ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)})) ∈ (SubGrp‘𝑊)) | 
| 54 | 15 | lsmlub 19682 | . . . . 5
⊢ (((𝑁‘{𝑋}) ∈ (SubGrp‘𝑊) ∧ (𝑁‘{𝑌}) ∈ (SubGrp‘𝑊) ∧ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)})) ∈ (SubGrp‘𝑊)) → (((𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)})) ∧ (𝑁‘{𝑌}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)}))) ↔ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)})))) | 
| 55 | 10, 14, 53, 54 | syl3anc 1373 | . . . 4
⊢ (𝜑 → (((𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)})) ∧ (𝑁‘{𝑌}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)}))) ↔ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)})))) | 
| 56 | 38, 52, 55 | mpbi2and 712 | . . 3
⊢ (𝜑 → ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)}))) | 
| 57 | 36, 56 | eqssd 4001 | . 2
⊢ (𝜑 → ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)})) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌}))) | 
| 58 | 6, 7, 15, 1, 5, 29 | lsmpr 21088 | . 2
⊢ (𝜑 → (𝑁‘{𝑋, (𝑋 + 𝑌)}) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)}))) | 
| 59 | 6, 7, 15, 1, 5, 11 | lsmpr 21088 | . 2
⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌}))) | 
| 60 | 57, 58, 59 | 3eqtr4d 2787 | 1
⊢ (𝜑 → (𝑁‘{𝑋, (𝑋 + 𝑌)}) = (𝑁‘{𝑋, 𝑌})) |