Step | Hyp | Ref
| Expression |
1 | | lshpset2.h |
. . . . . 6
β’ π» = (LSHypβπ) |
2 | | lshpset2.f |
. . . . . 6
β’ πΉ = (LFnlβπ) |
3 | | lshpset2.k |
. . . . . 6
β’ πΎ = (LKerβπ) |
4 | 1, 2, 3 | lshpkrex 38646 |
. . . . 5
β’ ((π β LVec β§ π β π») β βπ β πΉ (πΎβπ) = π ) |
5 | | eleq1 2813 |
. . . . . . . . . . . 12
β’ ((πΎβπ) = π β ((πΎβπ) β π» β π β π»)) |
6 | 5 | biimparc 478 |
. . . . . . . . . . 11
β’ ((π β π» β§ (πΎβπ) = π ) β (πΎβπ) β π») |
7 | 6 | adantll 712 |
. . . . . . . . . 10
β’ (((π β LVec β§ π β π») β§ (πΎβπ) = π ) β (πΎβπ) β π») |
8 | 7 | adantlr 713 |
. . . . . . . . 9
β’ ((((π β LVec β§ π β π») β§ π β πΉ) β§ (πΎβπ) = π ) β (πΎβπ) β π») |
9 | | lshpset2.v |
. . . . . . . . . 10
β’ π = (Baseβπ) |
10 | | lshpset2.d |
. . . . . . . . . 10
β’ π· = (Scalarβπ) |
11 | | lshpset2.z |
. . . . . . . . . 10
β’ 0 =
(0gβπ·) |
12 | | simplll 773 |
. . . . . . . . . 10
β’ ((((π β LVec β§ π β π») β§ π β πΉ) β§ (πΎβπ) = π ) β π β LVec) |
13 | | simplr 767 |
. . . . . . . . . 10
β’ ((((π β LVec β§ π β π») β§ π β πΉ) β§ (πΎβπ) = π ) β π β πΉ) |
14 | 9, 10, 11, 1, 2, 3,
12, 13 | lkrshp3 38634 |
. . . . . . . . 9
β’ ((((π β LVec β§ π β π») β§ π β πΉ) β§ (πΎβπ) = π ) β ((πΎβπ) β π» β π β (π Γ { 0 }))) |
15 | 8, 14 | mpbid 231 |
. . . . . . . 8
β’ ((((π β LVec β§ π β π») β§ π β πΉ) β§ (πΎβπ) = π ) β π β (π Γ { 0 })) |
16 | 15 | ex 411 |
. . . . . . 7
β’ (((π β LVec β§ π β π») β§ π β πΉ) β ((πΎβπ) = π β π β (π Γ { 0 }))) |
17 | | eqimss2 4032 |
. . . . . . . . 9
β’ ((πΎβπ) = π β π β (πΎβπ)) |
18 | | eqimss 4031 |
. . . . . . . . 9
β’ ((πΎβπ) = π β (πΎβπ) β π ) |
19 | 17, 18 | eqssd 3990 |
. . . . . . . 8
β’ ((πΎβπ) = π β π = (πΎβπ)) |
20 | 19 | a1i 11 |
. . . . . . 7
β’ (((π β LVec β§ π β π») β§ π β πΉ) β ((πΎβπ) = π β π = (πΎβπ))) |
21 | 16, 20 | jcad 511 |
. . . . . 6
β’ (((π β LVec β§ π β π») β§ π β πΉ) β ((πΎβπ) = π β (π β (π Γ { 0 }) β§ π = (πΎβπ)))) |
22 | 21 | reximdva 3158 |
. . . . 5
β’ ((π β LVec β§ π β π») β (βπ β πΉ (πΎβπ) = π β βπ β πΉ (π β (π Γ { 0 }) β§ π = (πΎβπ)))) |
23 | 4, 22 | mpd 15 |
. . . 4
β’ ((π β LVec β§ π β π») β βπ β πΉ (π β (π Γ { 0 }) β§ π = (πΎβπ))) |
24 | 23 | ex 411 |
. . 3
β’ (π β LVec β (π β π» β βπ β πΉ (π β (π Γ { 0 }) β§ π = (πΎβπ)))) |
25 | 9, 10, 11, 1, 2, 3 | lkrshp 38633 |
. . . . . . . 8
β’ ((π β LVec β§ π β πΉ β§ π β (π Γ { 0 })) β (πΎβπ) β π») |
26 | 25 | 3adant3r 1178 |
. . . . . . 7
β’ ((π β LVec β§ π β πΉ β§ (π β (π Γ { 0 }) β§ π = (πΎβπ))) β (πΎβπ) β π») |
27 | | eqid 2725 |
. . . . . . . . 9
β’
(LSpanβπ) =
(LSpanβπ) |
28 | | eqid 2725 |
. . . . . . . . 9
β’
(LSubSpβπ) =
(LSubSpβπ) |
29 | 9, 27, 28, 1 | islshp 38507 |
. . . . . . . 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 2813 |
. . . . . . . . 9
β’ (π = (πΎβπ) β (π β (LSubSpβπ) β (πΎβπ) β (LSubSpβπ))) |
33 | | neeq1 2993 |
. . . . . . . . 9
β’ (π = (πΎβπ) β (π β π β (πΎβπ) β π)) |
34 | | uneq1 4149 |
. . . . . . . . . . 11
β’ (π = (πΎβπ) β (π βͺ {π£}) = ((πΎβπ) βͺ {π£})) |
35 | 34 | fveqeq2d 6900 |
. . . . . . . . . 10
β’ (π = (πΎβπ) β (((LSpanβπ)β(π βͺ {π£})) = π β ((LSpanβπ)β((πΎβπ) βͺ {π£})) = π)) |
36 | 35 | rexbidv 3169 |
. . . . . . . . 9
β’ (π = (πΎβπ) β (βπ£ β π ((LSpanβπ)β(π βͺ {π£})) = π β βπ£ β π ((LSpanβπ)β((πΎβπ) βͺ {π£})) = π)) |
37 | 32, 33, 36 | 3anbi123d 1432 |
. . . . . . . 8
β’ (π = (πΎβπ) β ((π β (LSubSpβπ) β§ π β π β§ βπ£ β π ((LSpanβπ)β(π βͺ {π£})) = π) β ((πΎβπ) β (LSubSpβπ) β§ (πΎβπ) β π β§ βπ£ β π ((LSpanβπ)β((πΎβπ) βͺ {π£})) = π))) |
38 | 37 | adantl 480 |
. . . . . . 7
β’ ((π β (π Γ { 0 }) β§ π = (πΎβπ)) β ((π β (LSubSpβπ) β§ π β π β§ βπ£ β π ((LSpanβπ)β(π βͺ {π£})) = π) β ((πΎβπ) β (LSubSpβπ) β§ (πΎβπ) β π β§ βπ£ β π ((LSpanβπ)β((πΎβπ) βͺ {π£})) = π))) |
39 | 38 | 3ad2ant3 1132 |
. . . . . 6
β’ ((π β LVec β§ π β πΉ β§ (π β (π Γ { 0 }) β§ π = (πΎβπ))) β ((π β (LSubSpβπ) β§ π β π β§ βπ£ β π ((LSpanβπ)β(π βͺ {π£})) = π) β ((πΎβπ) β (LSubSpβπ) β§ (πΎβπ) β π β§ βπ£ β π ((LSpanβπ)β((πΎβπ) βͺ {π£})) = π))) |
40 | 31, 39 | mpbird 256 |
. . . . 5
β’ ((π β LVec β§ π β πΉ β§ (π β (π Γ { 0 }) β§ π = (πΎβπ))) β (π β (LSubSpβπ) β§ π β π β§ βπ£ β π ((LSpanβπ)β(π βͺ {π£})) = π)) |
41 | 40 | rexlimdv3a 3149 |
. . . 4
β’ (π β LVec β
(βπ β πΉ (π β (π Γ { 0 }) β§ π = (πΎβπ)) β (π β (LSubSpβπ) β§ π β π β§ βπ£ β π ((LSpanβπ)β(π βͺ {π£})) = π))) |
42 | 9, 27, 28, 1 | islshp 38507 |
. . . 4
β’ (π β LVec β (π β π» β (π β (LSubSpβπ) β§ π β π β§ βπ£ β π ((LSpanβπ)β(π βͺ {π£})) = π))) |
43 | 41, 42 | sylibrd 258 |
. . 3
β’ (π β LVec β
(βπ β πΉ (π β (π Γ { 0 }) β§ π = (πΎβπ)) β π β π»)) |
44 | 24, 43 | impbid 211 |
. 2
β’ (π β LVec β (π β π» β βπ β πΉ (π β (π Γ { 0 }) β§ π = (πΎβπ)))) |
45 | 44 | eqabdv 2859 |
1
β’ (π β LVec β π» = {π β£ βπ β πΉ (π β (π Γ { 0 }) β§ π = (πΎβπ))}) |