Step | Hyp | Ref
| Expression |
1 | | islindf.b |
. . 3
β’ π΅ = (Baseβπ) |
2 | 1 | islinds 21231 |
. 2
β’ (π β π β (πΉ β (LIndSβπ) β (πΉ β π΅ β§ ( I βΎ πΉ) LIndF π))) |
3 | 1 | fvexi 6857 |
. . . . . . 7
β’ π΅ β V |
4 | 3 | ssex 5279 |
. . . . . 6
β’ (πΉ β π΅ β πΉ β V) |
5 | 4 | adantl 483 |
. . . . 5
β’ ((π β π β§ πΉ β π΅) β πΉ β V) |
6 | | resiexg 7852 |
. . . . 5
β’ (πΉ β V β ( I βΎ
πΉ) β
V) |
7 | 5, 6 | syl 17 |
. . . 4
β’ ((π β π β§ πΉ β π΅) β ( I βΎ πΉ) β V) |
8 | | islindf.v |
. . . . 5
β’ Β· = (
Β·π βπ) |
9 | | islindf.k |
. . . . 5
β’ πΎ = (LSpanβπ) |
10 | | islindf.s |
. . . . 5
β’ π = (Scalarβπ) |
11 | | islindf.n |
. . . . 5
β’ π = (Baseβπ) |
12 | | islindf.z |
. . . . 5
β’ 0 =
(0gβπ) |
13 | 1, 8, 9, 10, 11, 12 | islindf 21234 |
. . . 4
β’ ((π β π β§ ( I βΎ πΉ) β V) β (( I βΎ πΉ) LIndF π β (( I βΎ πΉ):dom ( I βΎ πΉ)βΆπ΅ β§ βπ₯ β dom ( I βΎ πΉ)βπ β (π β { 0 }) Β¬ (π Β· (( I βΎ πΉ)βπ₯)) β (πΎβ(( I βΎ πΉ) β (dom ( I βΎ πΉ) β {π₯})))))) |
14 | 7, 13 | syldan 592 |
. . 3
β’ ((π β π β§ πΉ β π΅) β (( I βΎ πΉ) LIndF π β (( I βΎ πΉ):dom ( I βΎ πΉ)βΆπ΅ β§ βπ₯ β dom ( I βΎ πΉ)βπ β (π β { 0 }) Β¬ (π Β· (( I βΎ πΉ)βπ₯)) β (πΎβ(( I βΎ πΉ) β (dom ( I βΎ πΉ) β {π₯})))))) |
15 | 14 | pm5.32da 580 |
. 2
β’ (π β π β ((πΉ β π΅ β§ ( I βΎ πΉ) LIndF π) β (πΉ β π΅ β§ (( I βΎ πΉ):dom ( I βΎ πΉ)βΆπ΅ β§ βπ₯ β dom ( I βΎ πΉ)βπ β (π β { 0 }) Β¬ (π Β· (( I βΎ πΉ)βπ₯)) β (πΎβ(( I βΎ πΉ) β (dom ( I βΎ πΉ) β {π₯}))))))) |
16 | | dmresi 6006 |
. . . . . . . 8
β’ dom ( I
βΎ πΉ) = πΉ |
17 | 16 | raleqi 3310 |
. . . . . . 7
β’
(βπ₯ β
dom ( I βΎ πΉ)βπ β (π β { 0 }) Β¬ (π Β· (( I βΎ πΉ)βπ₯)) β (πΎβ(( I βΎ πΉ) β (dom ( I βΎ πΉ) β {π₯}))) β βπ₯ β πΉ βπ β (π β { 0 }) Β¬ (π Β· (( I βΎ πΉ)βπ₯)) β (πΎβ(( I βΎ πΉ) β (dom ( I βΎ πΉ) β {π₯})))) |
18 | | fvresi 7120 |
. . . . . . . . . . . 12
β’ (π₯ β πΉ β (( I βΎ πΉ)βπ₯) = π₯) |
19 | 18 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π₯ β πΉ β (π Β· (( I βΎ πΉ)βπ₯)) = (π Β· π₯)) |
20 | 16 | difeq1i 4079 |
. . . . . . . . . . . . . . 15
β’ (dom ( I
βΎ πΉ) β {π₯}) = (πΉ β {π₯}) |
21 | 20 | imaeq2i 6012 |
. . . . . . . . . . . . . 14
β’ (( I
βΎ πΉ) β (dom ( I
βΎ πΉ) β {π₯})) = (( I βΎ πΉ) β (πΉ β {π₯})) |
22 | | difss 4092 |
. . . . . . . . . . . . . . 15
β’ (πΉ β {π₯}) β πΉ |
23 | | resiima 6029 |
. . . . . . . . . . . . . . 15
β’ ((πΉ β {π₯}) β πΉ β (( I βΎ πΉ) β (πΉ β {π₯})) = (πΉ β {π₯})) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ (( I
βΎ πΉ) β (πΉ β {π₯})) = (πΉ β {π₯}) |
25 | 21, 24 | eqtri 2761 |
. . . . . . . . . . . . 13
β’ (( I
βΎ πΉ) β (dom ( I
βΎ πΉ) β {π₯})) = (πΉ β {π₯}) |
26 | 25 | fveq2i 6846 |
. . . . . . . . . . . 12
β’ (πΎβ(( I βΎ πΉ) β (dom ( I βΎ πΉ) β {π₯}))) = (πΎβ(πΉ β {π₯})) |
27 | 26 | a1i 11 |
. . . . . . . . . . 11
β’ (π₯ β πΉ β (πΎβ(( I βΎ πΉ) β (dom ( I βΎ πΉ) β {π₯}))) = (πΎβ(πΉ β {π₯}))) |
28 | 19, 27 | eleq12d 2828 |
. . . . . . . . . 10
β’ (π₯ β πΉ β ((π Β· (( I βΎ πΉ)βπ₯)) β (πΎβ(( I βΎ πΉ) β (dom ( I βΎ πΉ) β {π₯}))) β (π Β· π₯) β (πΎβ(πΉ β {π₯})))) |
29 | 28 | notbid 318 |
. . . . . . . . 9
β’ (π₯ β πΉ β (Β¬ (π Β· (( I βΎ πΉ)βπ₯)) β (πΎβ(( I βΎ πΉ) β (dom ( I βΎ πΉ) β {π₯}))) β Β¬ (π Β· π₯) β (πΎβ(πΉ β {π₯})))) |
30 | 29 | ralbidv 3171 |
. . . . . . . 8
β’ (π₯ β πΉ β (βπ β (π β { 0 }) Β¬ (π Β· (( I βΎ πΉ)βπ₯)) β (πΎβ(( I βΎ πΉ) β (dom ( I βΎ πΉ) β {π₯}))) β βπ β (π β { 0 }) Β¬ (π Β· π₯) β (πΎβ(πΉ β {π₯})))) |
31 | 30 | ralbiia 3091 |
. . . . . . 7
β’
(βπ₯ β
πΉ βπ β (π β { 0 }) Β¬ (π Β· (( I βΎ πΉ)βπ₯)) β (πΎβ(( I βΎ πΉ) β (dom ( I βΎ πΉ) β {π₯}))) β βπ₯ β πΉ βπ β (π β { 0 }) Β¬ (π Β· π₯) β (πΎβ(πΉ β {π₯}))) |
32 | 17, 31 | bitri 275 |
. . . . . 6
β’
(βπ₯ β
dom ( I βΎ πΉ)βπ β (π β { 0 }) Β¬ (π Β· (( I βΎ πΉ)βπ₯)) β (πΎβ(( I βΎ πΉ) β (dom ( I βΎ πΉ) β {π₯}))) β βπ₯ β πΉ βπ β (π β { 0 }) Β¬ (π Β· π₯) β (πΎβ(πΉ β {π₯}))) |
33 | 32 | anbi2i 624 |
. . . . 5
β’ ((( I
βΎ πΉ):dom ( I βΎ
πΉ)βΆπ΅ β§ βπ₯ β dom ( I βΎ πΉ)βπ β (π β { 0 }) Β¬ (π Β· (( I βΎ πΉ)βπ₯)) β (πΎβ(( I βΎ πΉ) β (dom ( I βΎ πΉ) β {π₯})))) β (( I βΎ πΉ):dom ( I βΎ πΉ)βΆπ΅ β§ βπ₯ β πΉ βπ β (π β { 0 }) Β¬ (π Β· π₯) β (πΎβ(πΉ β {π₯})))) |
34 | | f1oi 6823 |
. . . . . . . . 9
β’ ( I
βΎ πΉ):πΉβ1-1-ontoβπΉ |
35 | | f1of 6785 |
. . . . . . . . 9
β’ (( I
βΎ πΉ):πΉβ1-1-ontoβπΉ β ( I βΎ πΉ):πΉβΆπΉ) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . 8
β’ ( I
βΎ πΉ):πΉβΆπΉ |
37 | 16 | feq2i 6661 |
. . . . . . . 8
β’ (( I
βΎ πΉ):dom ( I βΎ
πΉ)βΆπΉ β ( I βΎ πΉ):πΉβΆπΉ) |
38 | 36, 37 | mpbir 230 |
. . . . . . 7
β’ ( I
βΎ πΉ):dom ( I βΎ
πΉ)βΆπΉ |
39 | | fss 6686 |
. . . . . . 7
β’ ((( I
βΎ πΉ):dom ( I βΎ
πΉ)βΆπΉ β§ πΉ β π΅) β ( I βΎ πΉ):dom ( I βΎ πΉ)βΆπ΅) |
40 | 38, 39 | mpan 689 |
. . . . . 6
β’ (πΉ β π΅ β ( I βΎ πΉ):dom ( I βΎ πΉ)βΆπ΅) |
41 | 40 | biantrurd 534 |
. . . . 5
β’ (πΉ β π΅ β (βπ₯ β πΉ βπ β (π β { 0 }) Β¬ (π Β· π₯) β (πΎβ(πΉ β {π₯})) β (( I βΎ πΉ):dom ( I βΎ πΉ)βΆπ΅ β§ βπ₯ β πΉ βπ β (π β { 0 }) Β¬ (π Β· π₯) β (πΎβ(πΉ β {π₯}))))) |
42 | 33, 41 | bitr4id 290 |
. . . 4
β’ (πΉ β π΅ β ((( I βΎ πΉ):dom ( I βΎ πΉ)βΆπ΅ β§ βπ₯ β dom ( I βΎ πΉ)βπ β (π β { 0 }) Β¬ (π Β· (( I βΎ πΉ)βπ₯)) β (πΎβ(( I βΎ πΉ) β (dom ( I βΎ πΉ) β {π₯})))) β βπ₯ β πΉ βπ β (π β { 0 }) Β¬ (π Β· π₯) β (πΎβ(πΉ β {π₯})))) |
43 | 42 | pm5.32i 576 |
. . 3
β’ ((πΉ β π΅ β§ (( I βΎ πΉ):dom ( I βΎ πΉ)βΆπ΅ β§ βπ₯ β dom ( I βΎ πΉ)βπ β (π β { 0 }) Β¬ (π Β· (( I βΎ πΉ)βπ₯)) β (πΎβ(( I βΎ πΉ) β (dom ( I βΎ πΉ) β {π₯}))))) β (πΉ β π΅ β§ βπ₯ β πΉ βπ β (π β { 0 }) Β¬ (π Β· π₯) β (πΎβ(πΉ β {π₯})))) |
44 | 43 | a1i 11 |
. 2
β’ (π β π β ((πΉ β π΅ β§ (( I βΎ πΉ):dom ( I βΎ πΉ)βΆπ΅ β§ βπ₯ β dom ( I βΎ πΉ)βπ β (π β { 0 }) Β¬ (π Β· (( I βΎ πΉ)βπ₯)) β (πΎβ(( I βΎ πΉ) β (dom ( I βΎ πΉ) β {π₯}))))) β (πΉ β π΅ β§ βπ₯ β πΉ βπ β (π β { 0 }) Β¬ (π Β· π₯) β (πΎβ(πΉ β {π₯}))))) |
45 | 2, 15, 44 | 3bitrd 305 |
1
β’ (π β π β (πΉ β (LIndSβπ) β (πΉ β π΅ β§ βπ₯ β πΉ βπ β (π β { 0 }) Β¬ (π Β· π₯) β (πΎβ(πΉ β {π₯}))))) |