Step | Hyp | Ref
| Expression |
1 | | lindepsnlininds 46619 |
. . . . 5
β’ ((π β π« π΅ β§ π β LMod) β (π linDepS π β Β¬ π linIndS π)) |
2 | 1 | ancoms 460 |
. . . 4
β’ ((π β LMod β§ π β π« π΅) β (π linDepS π β Β¬ π linIndS π)) |
3 | 2 | 3adant3 1133 |
. . 3
β’ ((π β LMod β§ π β π« π΅ β§ π
β NzRing) β (π linDepS π β Β¬ π linIndS π)) |
4 | 3 | con2bid 355 |
. 2
β’ ((π β LMod β§ π β π« π΅ β§ π
β NzRing) β (π linIndS π β Β¬ π linDepS π)) |
5 | | notnotb 315 |
. . . . . . . . . 10
β’ (π finSupp 0 β Β¬ Β¬ π finSupp 0 ) |
6 | | nne 2944 |
. . . . . . . . . . 11
β’ (Β¬
(π( linC βπ)(π β {π })) β π β (π( linC βπ)(π β {π })) = π ) |
7 | 6 | bicomi 223 |
. . . . . . . . . 10
β’ ((π( linC βπ)(π β {π })) = π β Β¬ (π( linC βπ)(π β {π })) β π ) |
8 | 5, 7 | anbi12i 628 |
. . . . . . . . 9
β’ ((π finSupp 0 β§ (π( linC βπ)(π β {π })) = π ) β (Β¬ Β¬ π finSupp 0 β§ Β¬ (π( linC βπ)(π β {π })) β π )) |
9 | | pm4.56 988 |
. . . . . . . . 9
β’ ((Β¬
Β¬ π finSupp 0 β§ Β¬
(π( linC βπ)(π β {π })) β π ) β Β¬ (Β¬ π finSupp 0 β¨ (π( linC βπ)(π β {π })) β π )) |
10 | 8, 9 | bitri 275 |
. . . . . . . 8
β’ ((π finSupp 0 β§ (π( linC βπ)(π β {π })) = π ) β Β¬ (Β¬ π finSupp 0 β¨ (π( linC βπ)(π β {π })) β π )) |
11 | 10 | rexbii 3094 |
. . . . . . 7
β’
(βπ β
(πΈ βm
(π β {π }))(π finSupp 0 β§ (π( linC βπ)(π β {π })) = π ) β βπ β (πΈ βm (π β {π })) Β¬ (Β¬ π finSupp 0 β¨ (π( linC βπ)(π β {π })) β π )) |
12 | | rexnal 3100 |
. . . . . . 7
β’
(βπ β
(πΈ βm
(π β {π })) Β¬ (Β¬ π finSupp 0 β¨ (π( linC βπ)(π β {π })) β π ) β Β¬ βπ β (πΈ βm (π β {π }))(Β¬ π finSupp 0 β¨ (π( linC βπ)(π β {π })) β π )) |
13 | 11, 12 | bitri 275 |
. . . . . 6
β’
(βπ β
(πΈ βm
(π β {π }))(π finSupp 0 β§ (π( linC βπ)(π β {π })) = π ) β Β¬ βπ β (πΈ βm (π β {π }))(Β¬ π finSupp 0 β¨ (π( linC βπ)(π β {π })) β π )) |
14 | 13 | rexbii 3094 |
. . . . 5
β’
(βπ β
π βπ β (πΈ βm (π β {π }))(π finSupp 0 β§ (π( linC βπ)(π β {π })) = π ) β βπ β π Β¬ βπ β (πΈ βm (π β {π }))(Β¬ π finSupp 0 β¨ (π( linC βπ)(π β {π })) β π )) |
15 | | rexnal 3100 |
. . . . 5
β’
(βπ β
π Β¬ βπ β (πΈ βm (π β {π }))(Β¬ π finSupp 0 β¨ (π( linC βπ)(π β {π })) β π ) β Β¬ βπ β π βπ β (πΈ βm (π β {π }))(Β¬ π finSupp 0 β¨ (π( linC βπ)(π β {π })) β π )) |
16 | 14, 15 | bitri 275 |
. . . 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 46650 |
. . . 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 βπ)(π β {π })) β π ))) |