Step | Hyp | Ref
| Expression |
1 | | simp1 1136 |
. . 3
β’ ((π β π β§ πΌ β π β§ πΉ:πΌβΆπ΅) β π β π) |
2 | | simp3 1138 |
. . . 4
β’ ((π β π β§ πΌ β π β§ πΉ:πΌβΆπ΅) β πΉ:πΌβΆπ΅) |
3 | | simp2 1137 |
. . . 4
β’ ((π β π β§ πΌ β π β§ πΉ:πΌβΆπ΅) β πΌ β π) |
4 | 2, 3 | fexd 7231 |
. . 3
β’ ((π β π β§ πΌ β π β§ πΉ:πΌβΆπ΅) β πΉ β V) |
5 | | islindf.b |
. . . 4
β’ π΅ = (Baseβπ) |
6 | | islindf.v |
. . . 4
β’ Β· = (
Β·π βπ) |
7 | | islindf.k |
. . . 4
β’ πΎ = (LSpanβπ) |
8 | | islindf.s |
. . . 4
β’ π = (Scalarβπ) |
9 | | islindf.n |
. . . 4
β’ π = (Baseβπ) |
10 | | islindf.z |
. . . 4
β’ 0 =
(0gβπ) |
11 | 5, 6, 7, 8, 9, 10 | islindf 21373 |
. . 3
β’ ((π β π β§ πΉ β V) β (πΉ LIndF π β (πΉ:dom πΉβΆπ΅ β§ βπ₯ β dom πΉβπ β (π β { 0 }) Β¬ (π Β· (πΉβπ₯)) β (πΎβ(πΉ β (dom πΉ β {π₯})))))) |
12 | 1, 4, 11 | syl2anc 584 |
. 2
β’ ((π β π β§ πΌ β π β§ πΉ:πΌβΆπ΅) β (πΉ LIndF π β (πΉ:dom πΉβΆπ΅ β§ βπ₯ β dom πΉβπ β (π β { 0 }) Β¬ (π Β· (πΉβπ₯)) β (πΎβ(πΉ β (dom πΉ β {π₯})))))) |
13 | | ffdm 6747 |
. . . . 5
β’ (πΉ:πΌβΆπ΅ β (πΉ:dom πΉβΆπ΅ β§ dom πΉ β πΌ)) |
14 | 13 | simpld 495 |
. . . 4
β’ (πΉ:πΌβΆπ΅ β πΉ:dom πΉβΆπ΅) |
15 | 14 | 3ad2ant3 1135 |
. . 3
β’ ((π β π β§ πΌ β π β§ πΉ:πΌβΆπ΅) β πΉ:dom πΉβΆπ΅) |
16 | 15 | biantrurd 533 |
. 2
β’ ((π β π β§ πΌ β π β§ πΉ:πΌβΆπ΅) β (βπ₯ β dom πΉβπ β (π β { 0 }) Β¬ (π Β· (πΉβπ₯)) β (πΎβ(πΉ β (dom πΉ β {π₯}))) β (πΉ:dom πΉβΆπ΅ β§ βπ₯ β dom πΉβπ β (π β { 0 }) Β¬ (π Β· (πΉβπ₯)) β (πΎβ(πΉ β (dom πΉ β {π₯})))))) |
17 | | fdm 6726 |
. . . 4
β’ (πΉ:πΌβΆπ΅ β dom πΉ = πΌ) |
18 | 17 | 3ad2ant3 1135 |
. . 3
β’ ((π β π β§ πΌ β π β§ πΉ:πΌβΆπ΅) β dom πΉ = πΌ) |
19 | 18 | difeq1d 4121 |
. . . . . . . 8
β’ ((π β π β§ πΌ β π β§ πΉ:πΌβΆπ΅) β (dom πΉ β {π₯}) = (πΌ β {π₯})) |
20 | 19 | imaeq2d 6059 |
. . . . . . 7
β’ ((π β π β§ πΌ β π β§ πΉ:πΌβΆπ΅) β (πΉ β (dom πΉ β {π₯})) = (πΉ β (πΌ β {π₯}))) |
21 | 20 | fveq2d 6895 |
. . . . . 6
β’ ((π β π β§ πΌ β π β§ πΉ:πΌβΆπ΅) β (πΎβ(πΉ β (dom πΉ β {π₯}))) = (πΎβ(πΉ β (πΌ β {π₯})))) |
22 | 21 | eleq2d 2819 |
. . . . 5
β’ ((π β π β§ πΌ β π β§ πΉ:πΌβΆπ΅) β ((π Β· (πΉβπ₯)) β (πΎβ(πΉ β (dom πΉ β {π₯}))) β (π Β· (πΉβπ₯)) β (πΎβ(πΉ β (πΌ β {π₯}))))) |
23 | 22 | notbid 317 |
. . . 4
β’ ((π β π β§ πΌ β π β§ πΉ:πΌβΆπ΅) β (Β¬ (π Β· (πΉβπ₯)) β (πΎβ(πΉ β (dom πΉ β {π₯}))) β Β¬ (π Β· (πΉβπ₯)) β (πΎβ(πΉ β (πΌ β {π₯}))))) |
24 | 23 | ralbidv 3177 |
. . 3
β’ ((π β π β§ πΌ β π β§ πΉ:πΌβΆπ΅) β (βπ β (π β { 0 }) Β¬ (π Β· (πΉβπ₯)) β (πΎβ(πΉ β (dom πΉ β {π₯}))) β βπ β (π β { 0 }) Β¬ (π Β· (πΉβπ₯)) β (πΎβ(πΉ β (πΌ β {π₯}))))) |
25 | 18, 24 | raleqbidv 3342 |
. 2
β’ ((π β π β§ πΌ β π β§ πΉ:πΌβΆπ΅) β (βπ₯ β dom πΉβπ β (π β { 0 }) Β¬ (π Β· (πΉβπ₯)) β (πΎβ(πΉ β (dom πΉ β {π₯}))) β βπ₯ β πΌ βπ β (π β { 0 }) Β¬ (π Β· (πΉβπ₯)) β (πΎβ(πΉ β (πΌ β {π₯}))))) |
26 | 12, 16, 25 | 3bitr2d 306 |
1
β’ ((π β π β§ πΌ β π β§ πΉ:πΌβΆπ΅) β (πΉ LIndF π β βπ₯ β πΌ βπ β (π β { 0 }) Β¬ (π Β· (πΉβπ₯)) β (πΎβ(πΉ β (πΌ β {π₯}))))) |