| Step | Hyp | Ref
| Expression |
|---|
| 1 | | lveclmod 20861 |
. . . . . . 7
β’ (π β LVec β π β LMod) |
| 2 | 1 | 3ad2ant1 1131 |
. . . . . 6
β’ ((π β LVec β§ (π β π β§ πΊ β πΉ) β§ Β¬ π β (πΎβπΊ)) β π β LMod) |
| 3 | | simp2r 1198 |
. . . . . . 7
β’ ((π β LVec β§ (π β π β§ πΊ β πΉ) β§ Β¬ π β (πΎβπΊ)) β πΊ β πΉ) |
| 4 | | lkrlsp3.f |
. . . . . . . 8
β’ πΉ = (LFnlβπ) |
| 5 | | lkrlsp3.k |
. . . . . . . 8
β’ πΎ = (LKerβπ) |
| 6 | | eqid 2730 |
. . . . . . . 8
β’
(LSubSpβπ) =
(LSubSpβπ) |
| 7 | 4, 5, 6 | lkrlss 38268 |
. . . . . . 7
β’ ((π β LMod β§ πΊ β πΉ) β (πΎβπΊ) β (LSubSpβπ)) |
| 8 | 2, 3, 7 | syl2anc 582 |
. . . . . 6
β’ ((π β LVec β§ (π β π β§ πΊ β πΉ) β§ Β¬ π β (πΎβπΊ)) β (πΎβπΊ) β (LSubSpβπ)) |
| 9 | | lkrlsp3.n |
. . . . . . 7
β’ π = (LSpanβπ) |
| 10 | 6, 9 | lspid 20737 |
. . . . . 6
β’ ((π β LMod β§ (πΎβπΊ) β (LSubSpβπ)) β (πβ(πΎβπΊ)) = (πΎβπΊ)) |
| 11 | 2, 8, 10 | syl2anc 582 |
. . . . 5
β’ ((π β LVec β§ (π β π β§ πΊ β πΉ) β§ Β¬ π β (πΎβπΊ)) β (πβ(πΎβπΊ)) = (πΎβπΊ)) |
| 12 | 11 | uneq1d 4161 |
. . . 4
β’ ((π β LVec β§ (π β π β§ πΊ β πΉ) β§ Β¬ π β (πΎβπΊ)) β ((πβ(πΎβπΊ)) βͺ (πβ{π})) = ((πΎβπΊ) βͺ (πβ{π}))) |
| 13 | 12 | fveq2d 6894 |
. . 3
β’ ((π β LVec β§ (π β π β§ πΊ β πΉ) β§ Β¬ π β (πΎβπΊ)) β (πβ((πβ(πΎβπΊ)) βͺ (πβ{π}))) = (πβ((πΎβπΊ) βͺ (πβ{π})))) |
| 14 | | lkrlsp3.v |
. . . . 5
β’ π = (Baseβπ) |
| 15 | 14, 4, 5, 2, 3 | lkrssv 38269 |
. . . 4
β’ ((π β LVec β§ (π β π β§ πΊ β πΉ) β§ Β¬ π β (πΎβπΊ)) β (πΎβπΊ) β π) |
| 16 | | simp2l 1197 |
. . . . 5
β’ ((π β LVec β§ (π β π β§ πΊ β πΉ) β§ Β¬ π β (πΎβπΊ)) β π β π) |
| 17 | 16 | snssd 4811 |
. . . 4
β’ ((π β LVec β§ (π β π β§ πΊ β πΉ) β§ Β¬ π β (πΎβπΊ)) β {π} β π) |
| 18 | 14, 9 | lspun 20742 |
. . . 4
β’ ((π β LMod β§ (πΎβπΊ) β π β§ {π} β π) β (πβ((πΎβπΊ) βͺ {π})) = (πβ((πβ(πΎβπΊ)) βͺ (πβ{π})))) |
| 19 | 2, 15, 17, 18 | syl3anc 1369 |
. . 3
β’ ((π β LVec β§ (π β π β§ πΊ β πΉ) β§ Β¬ π β (πΎβπΊ)) β (πβ((πΎβπΊ) βͺ {π})) = (πβ((πβ(πΎβπΊ)) βͺ (πβ{π})))) |
| 20 | 14, 6, 9 | lspsncl 20732 |
. . . . 5
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
| 21 | 2, 16, 20 | syl2anc 582 |
. . . 4
β’ ((π β LVec β§ (π β π β§ πΊ β πΉ) β§ Β¬ π β (πΎβπΊ)) β (πβ{π}) β (LSubSpβπ)) |
| 22 | | eqid 2730 |
. . . . 5
β’
(LSSumβπ) =
(LSSumβπ) |
| 23 | 6, 9, 22 | lsmsp 20841 |
. . . 4
β’ ((π β LMod β§ (πΎβπΊ) β (LSubSpβπ) β§ (πβ{π}) β (LSubSpβπ)) β ((πΎβπΊ)(LSSumβπ)(πβ{π})) = (πβ((πΎβπΊ) βͺ (πβ{π})))) |
| 24 | 2, 8, 21, 23 | syl3anc 1369 |
. . 3
β’ ((π β LVec β§ (π β π β§ πΊ β πΉ) β§ Β¬ π β (πΎβπΊ)) β ((πΎβπΊ)(LSSumβπ)(πβ{π})) = (πβ((πΎβπΊ) βͺ (πβ{π})))) |
| 25 | 13, 19, 24 | 3eqtr4d 2780 |
. 2
β’ ((π β LVec β§ (π β π β§ πΊ β πΉ) β§ Β¬ π β (πΎβπΊ)) β (πβ((πΎβπΊ) βͺ {π})) = ((πΎβπΊ)(LSSumβπ)(πβ{π}))) |
| 26 | 14, 9, 22, 4, 5 | lkrlsp2 38276 |
. 2
β’ ((π β LVec β§ (π β π β§ πΊ β πΉ) β§ Β¬ π β (πΎβπΊ)) β ((πΎβπΊ)(LSSumβπ)(πβ{π})) = π) |
| 27 | 25, 26 | eqtrd 2770 |
1
β’ ((π β LVec β§ (π β π β§ πΊ β πΉ) β§ Β¬ π β (πΎβπΊ)) β (πβ((πΎβπΊ) βͺ {π})) = π) |
