Step | Hyp | Ref
| Expression |
1 | | eqidd 2737 |
. . . . . 6
β’ (((π β LMod β§ π β π΅) β§ π β π) β {β¨π, π β©} = {β¨π, π β©}) |
2 | | fsng 7041 |
. . . . . . 7
β’ ((π β π΅ β§ π β π) β ({β¨π, π β©}:{π}βΆ{π } β {β¨π, π β©} = {β¨π, π β©})) |
3 | 2 | adantll 712 |
. . . . . 6
β’ (((π β LMod β§ π β π΅) β§ π β π) β ({β¨π, π β©}:{π}βΆ{π } β {β¨π, π β©} = {β¨π, π β©})) |
4 | 1, 3 | mpbird 257 |
. . . . 5
β’ (((π β LMod β§ π β π΅) β§ π β π) β {β¨π, π β©}:{π}βΆ{π }) |
5 | | snssi 4747 |
. . . . . 6
β’ (π β π β {π } β π) |
6 | 5 | adantl 483 |
. . . . 5
β’ (((π β LMod β§ π β π΅) β§ π β π) β {π } β π) |
7 | 4, 6 | fssd 6648 |
. . . 4
β’ (((π β LMod β§ π β π΅) β§ π β π) β {β¨π, π β©}:{π}βΆπ) |
8 | | snlindsntor.s |
. . . . . . 7
β’ π = (Baseβπ
) |
9 | 8 | fvexi 6818 |
. . . . . 6
β’ π β V |
10 | | snex 5363 |
. . . . . 6
β’ {π} β V |
11 | 9, 10 | pm3.2i 472 |
. . . . 5
β’ (π β V β§ {π} β V) |
12 | | elmapg 8659 |
. . . . 5
β’ ((π β V β§ {π} β V) β ({β¨π, π β©} β (π βm {π}) β {β¨π, π β©}:{π}βΆπ)) |
13 | 11, 12 | mp1i 13 |
. . . 4
β’ (((π β LMod β§ π β π΅) β§ π β π) β ({β¨π, π β©} β (π βm {π}) β {β¨π, π β©}:{π}βΆπ)) |
14 | 7, 13 | mpbird 257 |
. . 3
β’ (((π β LMod β§ π β π΅) β§ π β π) β {β¨π, π β©} β (π βm {π})) |
15 | | oveq1 7314 |
. . . . . 6
β’ (π = {β¨π, π β©} β (π( linC βπ){π}) = ({β¨π, π β©} ( linC βπ){π})) |
16 | 15 | eqeq1d 2738 |
. . . . 5
β’ (π = {β¨π, π β©} β ((π( linC βπ){π}) = π β ({β¨π, π β©} ( linC βπ){π}) = π)) |
17 | | fveq1 6803 |
. . . . . 6
β’ (π = {β¨π, π β©} β (πβπ) = ({β¨π, π β©}βπ)) |
18 | 17 | eqeq1d 2738 |
. . . . 5
β’ (π = {β¨π, π β©} β ((πβπ) = 0 β ({β¨π, π β©}βπ) = 0 )) |
19 | 16, 18 | imbi12d 345 |
. . . 4
β’ (π = {β¨π, π β©} β (((π( linC βπ){π}) = π β (πβπ) = 0 ) β (({β¨π, π β©} ( linC βπ){π}) = π β ({β¨π, π β©}βπ) = 0 ))) |
20 | | snlindsntor.b |
. . . . . . . 8
β’ π΅ = (Baseβπ) |
21 | | snlindsntor.r |
. . . . . . . 8
β’ π
= (Scalarβπ) |
22 | | snlindsntor.t |
. . . . . . . 8
β’ Β· = (
Β·π βπ) |
23 | 20, 21, 8, 22 | lincvalsng 45815 |
. . . . . . 7
β’ ((π β LMod β§ π β π΅ β§ π β π) β ({β¨π, π β©} ( linC βπ){π}) = (π Β· π)) |
24 | 23 | 3expa 1118 |
. . . . . 6
β’ (((π β LMod β§ π β π΅) β§ π β π) β ({β¨π, π β©} ( linC βπ){π}) = (π Β· π)) |
25 | 24 | eqeq1d 2738 |
. . . . 5
β’ (((π β LMod β§ π β π΅) β§ π β π) β (({β¨π, π β©} ( linC βπ){π}) = π β (π Β· π) = π)) |
26 | | fvsng 7084 |
. . . . . . 7
β’ ((π β π΅ β§ π β π) β ({β¨π, π β©}βπ) = π ) |
27 | 26 | adantll 712 |
. . . . . 6
β’ (((π β LMod β§ π β π΅) β§ π β π) β ({β¨π, π β©}βπ) = π ) |
28 | 27 | eqeq1d 2738 |
. . . . 5
β’ (((π β LMod β§ π β π΅) β§ π β π) β (({β¨π, π β©}βπ) = 0 β π = 0 )) |
29 | 25, 28 | imbi12d 345 |
. . . 4
β’ (((π β LMod β§ π β π΅) β§ π β π) β ((({β¨π, π β©} ( linC βπ){π}) = π β ({β¨π, π β©}βπ) = 0 ) β ((π Β· π) = π β π = 0 ))) |
30 | 19, 29 | sylan9bbr 512 |
. . 3
β’ ((((π β LMod β§ π β π΅) β§ π β π) β§ π = {β¨π, π β©}) β (((π( linC βπ){π}) = π β (πβπ) = 0 ) β ((π Β· π) = π β π = 0 ))) |
31 | 14, 30 | rspcdv 3558 |
. 2
β’ (((π β LMod β§ π β π΅) β§ π β π) β (βπ β (π βm {π})((π( linC βπ){π}) = π β (πβπ) = 0 ) β ((π Β· π) = π β π = 0 ))) |
32 | 31 | ralrimdva 3148 |
1
β’ ((π β LMod β§ π β π΅) β (βπ β (π βm {π})((π( linC βπ){π}) = π β (πβπ) = 0 ) β βπ β π ((π Β· π) = π β π = 0 ))) |