| Step | Hyp | Ref
| Expression |
|---|
| 1 | | lindepsnlininds 47631 |
. . . . 5
β’ ((π β π« π΅ β§ π β LMod) β (π linDepS π β Β¬ π linIndS π)) |
| 2 | 1 | ancoms 457 |
. . . 4
β’ ((π β LMod β§ π β π« π΅) β (π linDepS π β Β¬ π linIndS π)) |
| 3 | 2 | 3adant3 1129 |
. . 3
β’ ((π β LMod β§ π β π« π΅ β§ π
β NzRing) β (π linDepS π β Β¬ π linIndS π)) |
| 4 | 3 | con2bid 353 |
. 2
β’ ((π β LMod β§ π β π« π΅ β§ π
β NzRing) β (π linIndS π β Β¬ π linDepS π)) |
| 5 | | notnotb 314 |
. . . . . . . . . 10
β’ (π finSupp 0 β Β¬ Β¬ π finSupp 0 ) |
| 6 | | nne 2934 |
. . . . . . . . . . 11
β’ (Β¬
(π( linC βπ)(π β {π })) β π β (π( linC βπ)(π β {π })) = π ) |
| 7 | 6 | bicomi 223 |
. . . . . . . . . 10
β’ ((π( linC βπ)(π β {π })) = π β Β¬ (π( linC βπ)(π β {π })) β π ) |
| 8 | 5, 7 | anbi12i 626 |
. . . . . . . . 9
β’ ((π finSupp 0 β§ (π( linC βπ)(π β {π })) = π ) β (Β¬ Β¬ π finSupp 0 β§ Β¬ (π( linC βπ)(π β {π })) β π )) |
| 9 | | pm4.56 986 |
. . . . . . . . 9
β’ ((Β¬
Β¬ π finSupp 0 β§ Β¬
(π( linC βπ)(π β {π })) β π ) β Β¬ (Β¬ π finSupp 0 β¨ (π( linC βπ)(π β {π })) β π )) |
| 10 | 8, 9 | bitri 274 |
. . . . . . . 8
β’ ((π finSupp 0 β§ (π( linC βπ)(π β {π })) = π ) β Β¬ (Β¬ π finSupp 0 β¨ (π( linC βπ)(π β {π })) β π )) |
| 11 | 10 | rexbii 3084 |
. . . . . . 7
β’
(βπ β
(πΈ βm
(π β {π }))(π finSupp 0 β§ (π( linC βπ)(π β {π })) = π ) β βπ β (πΈ βm (π β {π })) Β¬ (Β¬ π finSupp 0 β¨ (π( linC βπ)(π β {π })) β π )) |
| 12 | | rexnal 3090 |
. . . . . . 7
β’
(βπ β
(πΈ βm
(π β {π })) Β¬ (Β¬ π finSupp 0 β¨ (π( linC βπ)(π β {π })) β π ) β Β¬ βπ β (πΈ βm (π β {π }))(Β¬ π finSupp 0 β¨ (π( linC βπ)(π β {π })) β π )) |
| 13 | 11, 12 | bitri 274 |
. . . . . 6
β’
(βπ β
(πΈ βm
(π β {π }))(π finSupp 0 β§ (π( linC βπ)(π β {π })) = π ) β Β¬ βπ β (πΈ βm (π β {π }))(Β¬ π finSupp 0 β¨ (π( linC βπ)(π β {π })) β π )) |
| 14 | 13 | rexbii 3084 |
. . . . 5
β’
(βπ β
π βπ β (πΈ βm (π β {π }))(π finSupp 0 β§ (π( linC βπ)(π β {π })) = π ) β βπ β π Β¬ βπ β (πΈ βm (π β {π }))(Β¬ π finSupp 0 β¨ (π( linC βπ)(π β {π })) β π )) |
| 15 | | rexnal 3090 |
. . . . 5
β’
(βπ β
π Β¬ βπ β (πΈ βm (π β {π }))(Β¬ π finSupp 0 β¨ (π( linC βπ)(π β {π })) β π ) β Β¬ βπ β π βπ β (πΈ βm (π β {π }))(Β¬ π finSupp 0 β¨ (π( linC βπ)(π β {π })) β π )) |
| 16 | 14, 15 | bitri 274 |
. . . 4
β’
(βπ β
π βπ β (πΈ βm (π β {π }))(π finSupp 0 β§ (π( linC βπ)(π β {π })) = π ) β Β¬ βπ β π βπ β (πΈ βm (π β {π }))(Β¬ π finSupp 0 β¨ (π( linC βπ)(π β {π })) β π )) |
| 17 | | islindeps2.b |
. . . . 5
β’ π΅ = (Baseβπ) |
| 18 | | islindeps2.z |
. . . . 5
β’ π = (0gβπ) |
| 19 | | islindeps2.r |
. . . . 5
β’ π
= (Scalarβπ) |
| 20 | | islindeps2.e |
. . . . 5
β’ πΈ = (Baseβπ
) |
| 21 | | islindeps2.0 |
. . . . 5
β’ 0 =
(0gβπ
) |
| 22 | 17, 18, 19, 20, 21 | islindeps2 47662 |
. . . 4
β’ ((π β LMod β§ π β π« π΅ β§ π
β NzRing) β (βπ β π βπ β (πΈ βm (π β {π }))(π finSupp 0 β§ (π( linC βπ)(π β {π })) = π ) β π linDepS π)) |
| 23 | 16, 22 | biimtrrid 242 |
. . 3
β’ ((π β LMod β§ π β π« π΅ β§ π
β NzRing) β (Β¬ βπ β π βπ β (πΈ βm (π β {π }))(Β¬ π finSupp 0 β¨ (π( linC βπ)(π β {π })) β π ) β π linDepS π)) |
| 24 | 23 | con1d 145 |
. 2
β’ ((π β LMod β§ π β π« π΅ β§ π
β NzRing) β (Β¬ π linDepS π β βπ β π βπ β (πΈ βm (π β {π }))(Β¬ π finSupp 0 β¨ (π( linC βπ)(π β {π })) β π ))) |
| 25 | 4, 24 | sylbid 239 |
1
β’ ((π β LMod β§ π β π« π΅ β§ π
β NzRing) β (π linIndS π β βπ β π βπ β (πΈ βm (π β {π }))(Β¬ π finSupp 0 β¨ (π( linC βπ)(π β {π })) β π ))) |
