Proof of Theorem lspprabs
Step | Hyp | Ref
| Expression |
1 | | lspprabs.w |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ LMod) |
2 | | eqid 2738 |
. . . . . . . 8
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
3 | 2 | lsssssubg 19849 |
. . . . . . 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 19868 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑊)) |
9 | 1, 5, 8 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑊)) |
10 | 4, 9 | sseldd 3878 |
. . . . 5
⊢ (𝜑 → (𝑁‘{𝑋}) ∈ (SubGrp‘𝑊)) |
11 | | lspprabs.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
12 | 6, 2, 7 | lspsncl 19868 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊)) |
13 | 1, 11, 12 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊)) |
14 | 4, 13 | sseldd 3878 |
. . . . 5
⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (SubGrp‘𝑊)) |
15 | | eqid 2738 |
. . . . . 6
⊢
(LSSum‘𝑊) =
(LSSum‘𝑊) |
16 | 15 | lsmub1 18900 |
. . . . 5
⊢ (((𝑁‘{𝑋}) ∈ (SubGrp‘𝑊) ∧ (𝑁‘{𝑌}) ∈ (SubGrp‘𝑊)) → (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌}))) |
17 | 10, 14, 16 | syl2anc 587 |
. . . 4
⊢ (𝜑 → (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌}))) |
18 | 2, 15 | lsmcl 19974 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ (𝑁‘{𝑋}) ∈ (LSubSp‘𝑊) ∧ (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊)) → ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})) ∈ (LSubSp‘𝑊)) |
19 | 1, 9, 13, 18 | syl3anc 1372 |
. . . . 5
⊢ (𝜑 → ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})) ∈ (LSubSp‘𝑊)) |
20 | 6, 7 | lspsnid 19884 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ (𝑁‘{𝑋})) |
21 | 1, 5, 20 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑋})) |
22 | 6, 7 | lspsnid 19884 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → 𝑌 ∈ (𝑁‘{𝑌})) |
23 | 1, 11, 22 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑌})) |
24 | | lspprabs.p |
. . . . . . 7
⊢ + =
(+g‘𝑊) |
25 | 24, 15 | lsmelvali 18893 |
. . . . . 6
⊢ ((((𝑁‘{𝑋}) ∈ (SubGrp‘𝑊) ∧ (𝑁‘{𝑌}) ∈ (SubGrp‘𝑊)) ∧ (𝑋 ∈ (𝑁‘{𝑋}) ∧ 𝑌 ∈ (𝑁‘{𝑌}))) → (𝑋 + 𝑌) ∈ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌}))) |
26 | 10, 14, 21, 23, 25 | syl22anc 838 |
. . . . 5
⊢ (𝜑 → (𝑋 + 𝑌) ∈ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌}))) |
27 | 2, 7, 1, 19, 26 | lspsnel5a 19887 |
. . . 4
⊢ (𝜑 → (𝑁‘{(𝑋 + 𝑌)}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌}))) |
28 | 6, 24 | lmodvacl 19767 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉) |
29 | 1, 5, 11, 28 | syl3anc 1372 |
. . . . . . 7
⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝑉) |
30 | 6, 2, 7 | lspsncl 19868 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ (𝑋 + 𝑌) ∈ 𝑉) → (𝑁‘{(𝑋 + 𝑌)}) ∈ (LSubSp‘𝑊)) |
31 | 1, 29, 30 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (𝑁‘{(𝑋 + 𝑌)}) ∈ (LSubSp‘𝑊)) |
32 | 4, 31 | sseldd 3878 |
. . . . 5
⊢ (𝜑 → (𝑁‘{(𝑋 + 𝑌)}) ∈ (SubGrp‘𝑊)) |
33 | 4, 19 | sseldd 3878 |
. . . . 5
⊢ (𝜑 → ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})) ∈ (SubGrp‘𝑊)) |
34 | 15 | lsmlub 18908 |
. . . . 5
⊢ (((𝑁‘{𝑋}) ∈ (SubGrp‘𝑊) ∧ (𝑁‘{(𝑋 + 𝑌)}) ∈ (SubGrp‘𝑊) ∧ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})) ∈ (SubGrp‘𝑊)) → (((𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})) ∧ (𝑁‘{(𝑋 + 𝑌)}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌}))) ↔ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)})) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})))) |
35 | 10, 32, 33, 34 | syl3anc 1372 |
. . . 4
⊢ (𝜑 → (((𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})) ∧ (𝑁‘{(𝑋 + 𝑌)}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌}))) ↔ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)})) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})))) |
36 | 17, 27, 35 | mpbi2and 712 |
. . 3
⊢ (𝜑 → ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)})) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌}))) |
37 | 15 | lsmub1 18900 |
. . . . 5
⊢ (((𝑁‘{𝑋}) ∈ (SubGrp‘𝑊) ∧ (𝑁‘{(𝑋 + 𝑌)}) ∈ (SubGrp‘𝑊)) → (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)}))) |
38 | 10, 32, 37 | syl2anc 587 |
. . . 4
⊢ (𝜑 → (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)}))) |
39 | 2, 15 | lsmcl 19974 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ (𝑁‘{𝑋}) ∈ (LSubSp‘𝑊) ∧ (𝑁‘{(𝑋 + 𝑌)}) ∈ (LSubSp‘𝑊)) → ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)})) ∈ (LSubSp‘𝑊)) |
40 | 1, 9, 31, 39 | syl3anc 1372 |
. . . . 5
⊢ (𝜑 → ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)})) ∈ (LSubSp‘𝑊)) |
41 | | eqid 2738 |
. . . . . . 7
⊢
(-g‘𝑊) = (-g‘𝑊) |
42 | 6, 7 | lspsnid 19884 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ (𝑋 + 𝑌) ∈ 𝑉) → (𝑋 + 𝑌) ∈ (𝑁‘{(𝑋 + 𝑌)})) |
43 | 1, 29, 42 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝑁‘{(𝑋 + 𝑌)})) |
44 | 41, 15, 32, 10, 43, 21 | lsmelvalmi 18895 |
. . . . . 6
⊢ (𝜑 → ((𝑋 + 𝑌)(-g‘𝑊)𝑋) ∈ ((𝑁‘{(𝑋 + 𝑌)})(LSSum‘𝑊)(𝑁‘{𝑋}))) |
45 | | lmodabl 19800 |
. . . . . . . 8
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Abel) |
46 | 1, 45 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ Abel) |
47 | 6, 24, 41 | ablpncan2 19055 |
. . . . . . 7
⊢ ((𝑊 ∈ Abel ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝑋 + 𝑌)(-g‘𝑊)𝑋) = 𝑌) |
48 | 46, 5, 11, 47 | syl3anc 1372 |
. . . . . 6
⊢ (𝜑 → ((𝑋 + 𝑌)(-g‘𝑊)𝑋) = 𝑌) |
49 | 15 | lsmcom 19097 |
. . . . . . 7
⊢ ((𝑊 ∈ Abel ∧ (𝑁‘{(𝑋 + 𝑌)}) ∈ (SubGrp‘𝑊) ∧ (𝑁‘{𝑋}) ∈ (SubGrp‘𝑊)) → ((𝑁‘{(𝑋 + 𝑌)})(LSSum‘𝑊)(𝑁‘{𝑋})) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)}))) |
50 | 46, 32, 10, 49 | syl3anc 1372 |
. . . . . 6
⊢ (𝜑 → ((𝑁‘{(𝑋 + 𝑌)})(LSSum‘𝑊)(𝑁‘{𝑋})) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)}))) |
51 | 44, 48, 50 | 3eltr3d 2847 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)}))) |
52 | 2, 7, 1, 40, 51 | lspsnel5a 19887 |
. . . 4
⊢ (𝜑 → (𝑁‘{𝑌}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)}))) |
53 | 4, 40 | sseldd 3878 |
. . . . 5
⊢ (𝜑 → ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)})) ∈ (SubGrp‘𝑊)) |
54 | 15 | lsmlub 18908 |
. . . . 5
⊢ (((𝑁‘{𝑋}) ∈ (SubGrp‘𝑊) ∧ (𝑁‘{𝑌}) ∈ (SubGrp‘𝑊) ∧ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)})) ∈ (SubGrp‘𝑊)) → (((𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)})) ∧ (𝑁‘{𝑌}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)}))) ↔ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)})))) |
55 | 10, 14, 53, 54 | syl3anc 1372 |
. . . 4
⊢ (𝜑 → (((𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)})) ∧ (𝑁‘{𝑌}) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)}))) ↔ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)})))) |
56 | 38, 52, 55 | mpbi2and 712 |
. . 3
⊢ (𝜑 → ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)}))) |
57 | 36, 56 | eqssd 3894 |
. 2
⊢ (𝜑 → ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)})) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌}))) |
58 | 6, 7, 15, 1, 5, 29 | lsmpr 19980 |
. 2
⊢ (𝜑 → (𝑁‘{𝑋, (𝑋 + 𝑌)}) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑋 + 𝑌)}))) |
59 | 6, 7, 15, 1, 5, 11 | lsmpr 19980 |
. 2
⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌}))) |
60 | 57, 58, 59 | 3eqtr4d 2783 |
1
⊢ (𝜑 → (𝑁‘{𝑋, (𝑋 + 𝑌)}) = (𝑁‘{𝑋, 𝑌})) |