Step | Hyp | Ref
| Expression |
1 | | lveclmod 20717 |
. . . 4
β’ (π β LVec β π β LMod) |
2 | 1 | 3ad2ant1 1134 |
. . 3
β’ ((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β π β LMod) |
3 | | simp2 1138 |
. . 3
β’ ((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β πΊ β πΉ) |
4 | | lkrshp.f |
. . . 4
β’ πΉ = (LFnlβπ) |
5 | | lkrshp.k |
. . . 4
β’ πΎ = (LKerβπ) |
6 | | eqid 2733 |
. . . 4
β’
(LSubSpβπ) =
(LSubSpβπ) |
7 | 4, 5, 6 | lkrlss 37965 |
. . 3
β’ ((π β LMod β§ πΊ β πΉ) β (πΎβπΊ) β (LSubSpβπ)) |
8 | 2, 3, 7 | syl2anc 585 |
. 2
β’ ((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β (πΎβπΊ) β (LSubSpβπ)) |
9 | | simp3 1139 |
. . 3
β’ ((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β πΊ β (π Γ { 0 })) |
10 | | lkrshp.d |
. . . . . 6
β’ π· = (Scalarβπ) |
11 | | lkrshp.z |
. . . . . 6
β’ 0 =
(0gβπ·) |
12 | | lkrshp.v |
. . . . . 6
β’ π = (Baseβπ) |
13 | 10, 11, 12, 4, 5 | lkr0f 37964 |
. . . . 5
β’ ((π β LMod β§ πΊ β πΉ) β ((πΎβπΊ) = π β πΊ = (π Γ { 0 }))) |
14 | 2, 3, 13 | syl2anc 585 |
. . . 4
β’ ((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β ((πΎβπΊ) = π β πΊ = (π Γ { 0 }))) |
15 | 14 | necon3bid 2986 |
. . 3
β’ ((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β ((πΎβπΊ) β π β πΊ β (π Γ { 0 }))) |
16 | 9, 15 | mpbird 257 |
. 2
β’ ((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β (πΎβπΊ) β π) |
17 | | eqid 2733 |
. . . 4
β’
(1rβπ·) = (1rβπ·) |
18 | 10, 11, 17, 12, 4 | lfl1 37940 |
. . 3
β’ ((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β βπ£ β π (πΊβπ£) = (1rβπ·)) |
19 | | simp11 1204 |
. . . . . 6
β’ (((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β§ π£ β π β§ (πΊβπ£) = (1rβπ·)) β π β LVec) |
20 | | simp2 1138 |
. . . . . 6
β’ (((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β§ π£ β π β§ (πΊβπ£) = (1rβπ·)) β π£ β π) |
21 | | simp12 1205 |
. . . . . 6
β’ (((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β§ π£ β π β§ (πΊβπ£) = (1rβπ·)) β πΊ β πΉ) |
22 | | simp3 1139 |
. . . . . . . 8
β’ (((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β§ π£ β π β§ (πΊβπ£) = (1rβπ·)) β (πΊβπ£) = (1rβπ·)) |
23 | 10 | lvecdrng 20716 |
. . . . . . . . 9
β’ (π β LVec β π· β
DivRing) |
24 | 11, 17 | drngunz 20376 |
. . . . . . . . 9
β’ (π· β DivRing β
(1rβπ·)
β 0
) |
25 | 19, 23, 24 | 3syl 18 |
. . . . . . . 8
β’ (((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β§ π£ β π β§ (πΊβπ£) = (1rβπ·)) β (1rβπ·) β 0 ) |
26 | 22, 25 | eqnetrd 3009 |
. . . . . . 7
β’ (((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β§ π£ β π β§ (πΊβπ£) = (1rβπ·)) β (πΊβπ£) β 0 ) |
27 | | simpl11 1249 |
. . . . . . . . . 10
β’ ((((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β§ π£ β π β§ (πΊβπ£) = (1rβπ·)) β§ π£ β (πΎβπΊ)) β π β LVec) |
28 | | simpl12 1250 |
. . . . . . . . . 10
β’ ((((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β§ π£ β π β§ (πΊβπ£) = (1rβπ·)) β§ π£ β (πΎβπΊ)) β πΊ β πΉ) |
29 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β§ π£ β π β§ (πΊβπ£) = (1rβπ·)) β§ π£ β (πΎβπΊ)) β π£ β (πΎβπΊ)) |
30 | 10, 11, 4, 5 | lkrf0 37963 |
. . . . . . . . . 10
β’ ((π β LVec β§ πΊ β πΉ β§ π£ β (πΎβπΊ)) β (πΊβπ£) = 0 ) |
31 | 27, 28, 29, 30 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β§ π£ β π β§ (πΊβπ£) = (1rβπ·)) β§ π£ β (πΎβπΊ)) β (πΊβπ£) = 0 ) |
32 | 31 | ex 414 |
. . . . . . . 8
β’ (((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β§ π£ β π β§ (πΊβπ£) = (1rβπ·)) β (π£ β (πΎβπΊ) β (πΊβπ£) = 0 )) |
33 | 32 | necon3ad 2954 |
. . . . . . 7
β’ (((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β§ π£ β π β§ (πΊβπ£) = (1rβπ·)) β ((πΊβπ£) β 0 β Β¬ π£ β (πΎβπΊ))) |
34 | 26, 33 | mpd 15 |
. . . . . 6
β’ (((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β§ π£ β π β§ (πΊβπ£) = (1rβπ·)) β Β¬ π£ β (πΎβπΊ)) |
35 | | eqid 2733 |
. . . . . . 7
β’
(LSpanβπ) =
(LSpanβπ) |
36 | 12, 35, 4, 5 | lkrlsp3 37974 |
. . . . . 6
β’ ((π β LVec β§ (π£ β π β§ πΊ β πΉ) β§ Β¬ π£ β (πΎβπΊ)) β ((LSpanβπ)β((πΎβπΊ) βͺ {π£})) = π) |
37 | 19, 20, 21, 34, 36 | syl121anc 1376 |
. . . . 5
β’ (((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β§ π£ β π β§ (πΊβπ£) = (1rβπ·)) β ((LSpanβπ)β((πΎβπΊ) βͺ {π£})) = π) |
38 | 37 | 3expia 1122 |
. . . 4
β’ (((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β§ π£ β π) β ((πΊβπ£) = (1rβπ·) β ((LSpanβπ)β((πΎβπΊ) βͺ {π£})) = π)) |
39 | 38 | reximdva 3169 |
. . 3
β’ ((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β (βπ£ β π (πΊβπ£) = (1rβπ·) β βπ£ β π ((LSpanβπ)β((πΎβπΊ) βͺ {π£})) = π)) |
40 | 18, 39 | mpd 15 |
. 2
β’ ((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β βπ£ β π ((LSpanβπ)β((πΎβπΊ) βͺ {π£})) = π) |
41 | | lkrshp.h |
. . . 4
β’ π» = (LSHypβπ) |
42 | 12, 35, 6, 41 | islshp 37849 |
. . 3
β’ (π β LVec β ((πΎβπΊ) β π» β ((πΎβπΊ) β (LSubSpβπ) β§ (πΎβπΊ) β π β§ βπ£ β π ((LSpanβπ)β((πΎβπΊ) βͺ {π£})) = π))) |
43 | 42 | 3ad2ant1 1134 |
. 2
β’ ((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β ((πΎβπΊ) β π» β ((πΎβπΊ) β (LSubSpβπ) β§ (πΎβπΊ) β π β§ βπ£ β π ((LSpanβπ)β((πΎβπΊ) βͺ {π£})) = π))) |
44 | 8, 16, 40, 43 | mpbir3and 1343 |
1
β’ ((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β (πΎβπΊ) β π») |