Step | Hyp | Ref
| Expression |
1 | | lshpset2.h |
. . . . . 6
β’ π» = (LSHypβπ) |
2 | | lshpset2.f |
. . . . . 6
β’ πΉ = (LFnlβπ) |
3 | | lshpset2.k |
. . . . . 6
β’ πΎ = (LKerβπ) |
4 | 1, 2, 3 | lshpkrex 38501 |
. . . . 5
β’ ((π β LVec β§ π β π») β βπ β πΉ (πΎβπ) = π ) |
5 | | eleq1 2815 |
. . . . . . . . . . . 12
β’ ((πΎβπ) = π β ((πΎβπ) β π» β π β π»)) |
6 | 5 | biimparc 479 |
. . . . . . . . . . 11
β’ ((π β π» β§ (πΎβπ) = π ) β (πΎβπ) β π») |
7 | 6 | adantll 711 |
. . . . . . . . . 10
β’ (((π β LVec β§ π β π») β§ (πΎβπ) = π ) β (πΎβπ) β π») |
8 | 7 | adantlr 712 |
. . . . . . . . 9
β’ ((((π β LVec β§ π β π») β§ π β πΉ) β§ (πΎβπ) = π ) β (πΎβπ) β π») |
9 | | lshpset2.v |
. . . . . . . . . 10
β’ π = (Baseβπ) |
10 | | lshpset2.d |
. . . . . . . . . 10
β’ π· = (Scalarβπ) |
11 | | lshpset2.z |
. . . . . . . . . 10
β’ 0 =
(0gβπ·) |
12 | | simplll 772 |
. . . . . . . . . 10
β’ ((((π β LVec β§ π β π») β§ π β πΉ) β§ (πΎβπ) = π ) β π β LVec) |
13 | | simplr 766 |
. . . . . . . . . 10
β’ ((((π β LVec β§ π β π») β§ π β πΉ) β§ (πΎβπ) = π ) β π β πΉ) |
14 | 9, 10, 11, 1, 2, 3,
12, 13 | lkrshp3 38489 |
. . . . . . . . 9
β’ ((((π β LVec β§ π β π») β§ π β πΉ) β§ (πΎβπ) = π ) β ((πΎβπ) β π» β π β (π Γ { 0 }))) |
15 | 8, 14 | mpbid 231 |
. . . . . . . 8
β’ ((((π β LVec β§ π β π») β§ π β πΉ) β§ (πΎβπ) = π ) β π β (π Γ { 0 })) |
16 | 15 | ex 412 |
. . . . . . 7
β’ (((π β LVec β§ π β π») β§ π β πΉ) β ((πΎβπ) = π β π β (π Γ { 0 }))) |
17 | | eqimss2 4036 |
. . . . . . . . 9
β’ ((πΎβπ) = π β π β (πΎβπ)) |
18 | | eqimss 4035 |
. . . . . . . . 9
β’ ((πΎβπ) = π β (πΎβπ) β π ) |
19 | 17, 18 | eqssd 3994 |
. . . . . . . 8
β’ ((πΎβπ) = π β π = (πΎβπ)) |
20 | 19 | a1i 11 |
. . . . . . 7
β’ (((π β LVec β§ π β π») β§ π β πΉ) β ((πΎβπ) = π β π = (πΎβπ))) |
21 | 16, 20 | jcad 512 |
. . . . . 6
β’ (((π β LVec β§ π β π») β§ π β πΉ) β ((πΎβπ) = π β (π β (π Γ { 0 }) β§ π = (πΎβπ)))) |
22 | 21 | reximdva 3162 |
. . . . 5
β’ ((π β LVec β§ π β π») β (βπ β πΉ (πΎβπ) = π β βπ β πΉ (π β (π Γ { 0 }) β§ π = (πΎβπ)))) |
23 | 4, 22 | mpd 15 |
. . . 4
β’ ((π β LVec β§ π β π») β βπ β πΉ (π β (π Γ { 0 }) β§ π = (πΎβπ))) |
24 | 23 | ex 412 |
. . 3
β’ (π β LVec β (π β π» β βπ β πΉ (π β (π Γ { 0 }) β§ π = (πΎβπ)))) |
25 | 9, 10, 11, 1, 2, 3 | lkrshp 38488 |
. . . . . . . 8
β’ ((π β LVec β§ π β πΉ β§ π β (π Γ { 0 })) β (πΎβπ) β π») |
26 | 25 | 3adant3r 1178 |
. . . . . . 7
β’ ((π β LVec β§ π β πΉ β§ (π β (π Γ { 0 }) β§ π = (πΎβπ))) β (πΎβπ) β π») |
27 | | eqid 2726 |
. . . . . . . . 9
β’
(LSpanβπ) =
(LSpanβπ) |
28 | | eqid 2726 |
. . . . . . . . 9
β’
(LSubSpβπ) =
(LSubSpβπ) |
29 | 9, 27, 28, 1 | islshp 38362 |
. . . . . . . 8
β’ (π β LVec β ((πΎβπ) β π» β ((πΎβπ) β (LSubSpβπ) β§ (πΎβπ) β π β§ βπ£ β π ((LSpanβπ)β((πΎβπ) βͺ {π£})) = π))) |
30 | 29 | 3ad2ant1 1130 |
. . . . . . 7
β’ ((π β LVec β§ π β πΉ β§ (π β (π Γ { 0 }) β§ π = (πΎβπ))) β ((πΎβπ) β π» β ((πΎβπ) β (LSubSpβπ) β§ (πΎβπ) β π β§ βπ£ β π ((LSpanβπ)β((πΎβπ) βͺ {π£})) = π))) |
31 | 26, 30 | mpbid 231 |
. . . . . 6
β’ ((π β LVec β§ π β πΉ β§ (π β (π Γ { 0 }) β§ π = (πΎβπ))) β ((πΎβπ) β (LSubSpβπ) β§ (πΎβπ) β π β§ βπ£ β π ((LSpanβπ)β((πΎβπ) βͺ {π£})) = π)) |
32 | | eleq1 2815 |
. . . . . . . . 9
β’ (π = (πΎβπ) β (π β (LSubSpβπ) β (πΎβπ) β (LSubSpβπ))) |
33 | | neeq1 2997 |
. . . . . . . . 9
β’ (π = (πΎβπ) β (π β π β (πΎβπ) β π)) |
34 | | uneq1 4151 |
. . . . . . . . . . 11
β’ (π = (πΎβπ) β (π βͺ {π£}) = ((πΎβπ) βͺ {π£})) |
35 | 34 | fveqeq2d 6893 |
. . . . . . . . . 10
β’ (π = (πΎβπ) β (((LSpanβπ)β(π βͺ {π£})) = π β ((LSpanβπ)β((πΎβπ) βͺ {π£})) = π)) |
36 | 35 | rexbidv 3172 |
. . . . . . . . 9
β’ (π = (πΎβπ) β (βπ£ β π ((LSpanβπ)β(π βͺ {π£})) = π β βπ£ β π ((LSpanβπ)β((πΎβπ) βͺ {π£})) = π)) |
37 | 32, 33, 36 | 3anbi123d 1432 |
. . . . . . . 8
β’ (π = (πΎβπ) β ((π β (LSubSpβπ) β§ π β π β§ βπ£ β π ((LSpanβπ)β(π βͺ {π£})) = π) β ((πΎβπ) β (LSubSpβπ) β§ (πΎβπ) β π β§ βπ£ β π ((LSpanβπ)β((πΎβπ) βͺ {π£})) = π))) |
38 | 37 | adantl 481 |
. . . . . . 7
β’ ((π β (π Γ { 0 }) β§ π = (πΎβπ)) β ((π β (LSubSpβπ) β§ π β π β§ βπ£ β π ((LSpanβπ)β(π βͺ {π£})) = π) β ((πΎβπ) β (LSubSpβπ) β§ (πΎβπ) β π β§ βπ£ β π ((LSpanβπ)β((πΎβπ) βͺ {π£})) = π))) |
39 | 38 | 3ad2ant3 1132 |
. . . . . 6
β’ ((π β LVec β§ π β πΉ β§ (π β (π Γ { 0 }) β§ π = (πΎβπ))) β ((π β (LSubSpβπ) β§ π β π β§ βπ£ β π ((LSpanβπ)β(π βͺ {π£})) = π) β ((πΎβπ) β (LSubSpβπ) β§ (πΎβπ) β π β§ βπ£ β π ((LSpanβπ)β((πΎβπ) βͺ {π£})) = π))) |
40 | 31, 39 | mpbird 257 |
. . . . 5
β’ ((π β LVec β§ π β πΉ β§ (π β (π Γ { 0 }) β§ π = (πΎβπ))) β (π β (LSubSpβπ) β§ π β π β§ βπ£ β π ((LSpanβπ)β(π βͺ {π£})) = π)) |
41 | 40 | rexlimdv3a 3153 |
. . . 4
β’ (π β LVec β
(βπ β πΉ (π β (π Γ { 0 }) β§ π = (πΎβπ)) β (π β (LSubSpβπ) β§ π β π β§ βπ£ β π ((LSpanβπ)β(π βͺ {π£})) = π))) |
42 | 9, 27, 28, 1 | islshp 38362 |
. . . 4
β’ (π β LVec β (π β π» β (π β (LSubSpβπ) β§ π β π β§ βπ£ β π ((LSpanβπ)β(π βͺ {π£})) = π))) |
43 | 41, 42 | sylibrd 259 |
. . 3
β’ (π β LVec β
(βπ β πΉ (π β (π Γ { 0 }) β§ π = (πΎβπ)) β π β π»)) |
44 | 24, 43 | impbid 211 |
. 2
β’ (π β LVec β (π β π» β βπ β πΉ (π β (π Γ { 0 }) β§ π = (πΎβπ)))) |
45 | 44 | eqabdv 2861 |
1
β’ (π β LVec β π» = {π β£ βπ β πΉ (π β (π Γ { 0 }) β§ π = (πΎβπ))}) |