Step | Hyp | Ref
| Expression |
1 | | lindepsnlininds 47133 |
. . 3
β’ ((π β π« π΅ β§ π β π) β (π linDepS π β Β¬ π linIndS π)) |
2 | 1 | ancoms 460 |
. 2
β’ ((π β π β§ π β π« π΅) β (π linDepS π β Β¬ π linIndS π)) |
3 | | islindeps.b |
. . . . . 6
β’ π΅ = (Baseβπ) |
4 | | islindeps.z |
. . . . . 6
β’ π = (0gβπ) |
5 | | islindeps.r |
. . . . . 6
β’ π
= (Scalarβπ) |
6 | | islindeps.e |
. . . . . 6
β’ πΈ = (Baseβπ
) |
7 | | islindeps.0 |
. . . . . 6
β’ 0 =
(0gβπ
) |
8 | 3, 4, 5, 6, 7 | islininds 47127 |
. . . . 5
β’ ((π β π« π΅ β§ π β π) β (π linIndS π β (π β π« π΅ β§ βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 )))) |
9 | 8 | ancoms 460 |
. . . 4
β’ ((π β π β§ π β π« π΅) β (π linIndS π β (π β π« π΅ β§ βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 )))) |
10 | | ibar 530 |
. . . . . 6
β’ (π β π« π΅ β (βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ) β (π β π« π΅ β§ βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 )))) |
11 | 10 | bicomd 222 |
. . . . 5
β’ (π β π« π΅ β ((π β π« π΅ β§ βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 )) β βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) |
12 | 11 | adantl 483 |
. . . 4
β’ ((π β π β§ π β π« π΅) β ((π β π« π΅ β§ βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 )) β βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) |
13 | 9, 12 | bitrd 279 |
. . 3
β’ ((π β π β§ π β π« π΅) β (π linIndS π β βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) |
14 | 13 | notbid 318 |
. 2
β’ ((π β π β§ π β π« π΅) β (Β¬ π linIndS π β Β¬ βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) |
15 | | rexnal 3101 |
. . . 4
β’
(βπ β
(πΈ βm π) Β¬ ((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ) β Β¬
βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 )) |
16 | | df-ne 2942 |
. . . . . . . . 9
β’ ((πβπ₯) β 0 β Β¬ (πβπ₯) = 0 ) |
17 | 16 | rexbii 3095 |
. . . . . . . 8
β’
(βπ₯ β
π (πβπ₯) β 0 β βπ₯ β π Β¬ (πβπ₯) = 0 ) |
18 | | rexnal 3101 |
. . . . . . . 8
β’
(βπ₯ β
π Β¬ (πβπ₯) = 0 β Β¬ βπ₯ β π (πβπ₯) = 0 ) |
19 | 17, 18 | bitr2i 276 |
. . . . . . 7
β’ (Β¬
βπ₯ β π (πβπ₯) = 0 β βπ₯ β π (πβπ₯) β 0 ) |
20 | 19 | anbi2i 624 |
. . . . . 6
β’ (((π finSupp 0 β§ (π( linC βπ)π) = π) β§ Β¬ βπ₯ β π (πβπ₯) = 0 ) β ((π finSupp 0 β§ (π( linC βπ)π) = π) β§ βπ₯ β π (πβπ₯) β 0 )) |
21 | | pm4.61 406 |
. . . . . 6
β’ (Β¬
((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ) β ((π finSupp 0 β§ (π( linC βπ)π) = π) β§ Β¬ βπ₯ β π (πβπ₯) = 0 )) |
22 | | df-3an 1090 |
. . . . . 6
β’ ((π finSupp 0 β§ (π( linC βπ)π) = π β§ βπ₯ β π (πβπ₯) β 0 ) β ((π finSupp 0 β§ (π( linC βπ)π) = π) β§ βπ₯ β π (πβπ₯) β 0 )) |
23 | 20, 21, 22 | 3bitr4i 303 |
. . . . 5
β’ (Β¬
((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ) β (π finSupp 0 β§ (π( linC βπ)π) = π β§ βπ₯ β π (πβπ₯) β 0 )) |
24 | 23 | rexbii 3095 |
. . . 4
β’
(βπ β
(πΈ βm π) Β¬ ((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ) β βπ β (πΈ βm π)(π finSupp 0 β§ (π( linC βπ)π) = π β§ βπ₯ β π (πβπ₯) β 0 )) |
25 | 15, 24 | bitr3i 277 |
. . 3
β’ (Β¬
βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ) β βπ β (πΈ βm π)(π finSupp 0 β§ (π( linC βπ)π) = π β§ βπ₯ β π (πβπ₯) β 0 )) |
26 | 25 | a1i 11 |
. 2
β’ ((π β π β§ π β π« π΅) β (Β¬ βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ) β βπ β (πΈ βm π)(π finSupp 0 β§ (π( linC βπ)π) = π β§ βπ₯ β π (πβπ₯) β 0 ))) |
27 | 2, 14, 26 | 3bitrd 305 |
1
β’ ((π β π β§ π β π« π΅) β (π linDepS π β βπ β (πΈ βm π)(π finSupp 0 β§ (π( linC βπ)π) = π β§ βπ₯ β π (πβπ₯) β 0 ))) |