| Step | Hyp | Ref
| Expression |
|---|
| 1 | | lveclmod 20973 |
. . . 4
β’ (π β LVec β π β LMod) |
| 2 | 1 | 3anim2i 1151 |
. . 3
β’ ((π β π« π΅ β§ π β LVec β§ π β π) β (π β π« π΅ β§ π β LMod β§ π β π)) |
| 3 | 2 | 3ad2ant1 1131 |
. 2
β’ (((π β π« π΅ β§ π β LVec β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β 0 β§ πΉ finSupp 0 ) β§ (πΉ( linC βπ)π) = π) β (π β π« π΅ β§ π β LMod β§ π β π)) |
| 4 | | simp21 1204 |
. 2
β’ (((π β π« π΅ β§ π β LVec β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β 0 β§ πΉ finSupp 0 ) β§ (πΉ( linC βπ)π) = π) β πΉ β (πΈ βm π)) |
| 5 | | elmapi 8857 |
. . . . . 6
β’ (πΉ β (πΈ βm π) β πΉ:πβΆπΈ) |
| 6 | 5 | 3ad2ant1 1131 |
. . . . 5
β’ ((πΉ β (πΈ βm π) β§ (πΉβπ) β 0 β§ πΉ finSupp 0 ) β πΉ:πβΆπΈ) |
| 7 | | simp3 1136 |
. . . . 5
β’ ((π β π« π΅ β§ π β LVec β§ π β π) β π β π) |
| 8 | | ffvelcdm 7085 |
. . . . 5
β’ ((πΉ:πβΆπΈ β§ π β π) β (πΉβπ) β πΈ) |
| 9 | 6, 7, 8 | syl2anr 596 |
. . . 4
β’ (((π β π« π΅ β§ π β LVec β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β 0 β§ πΉ finSupp 0 )) β (πΉβπ) β πΈ) |
| 10 | | simpr2 1193 |
. . . 4
β’ (((π β π« π΅ β§ π β LVec β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β 0 β§ πΉ finSupp 0 )) β (πΉβπ) β 0 ) |
| 11 | | lincresunit.r |
. . . . . . . 8
β’ π
= (Scalarβπ) |
| 12 | 11 | lvecdrng 20972 |
. . . . . . 7
β’ (π β LVec β π
β
DivRing) |
| 13 | 12 | 3ad2ant2 1132 |
. . . . . 6
β’ ((π β π« π΅ β§ π β LVec β§ π β π) β π
β DivRing) |
| 14 | 13 | adantr 480 |
. . . . 5
β’ (((π β π« π΅ β§ π β LVec β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β 0 β§ πΉ finSupp 0 )) β π
β
DivRing) |
| 15 | | lincresunit.e |
. . . . . 6
β’ πΈ = (Baseβπ
) |
| 16 | | lincresunit.u |
. . . . . 6
β’ π = (Unitβπ
) |
| 17 | | lincresunit.0 |
. . . . . 6
β’ 0 =
(0gβπ
) |
| 18 | 15, 16, 17 | drngunit 20611 |
. . . . 5
β’ (π
β DivRing β ((πΉβπ) β π β ((πΉβπ) β πΈ β§ (πΉβπ) β 0 ))) |
| 19 | 14, 18 | syl 17 |
. . . 4
β’ (((π β π« π΅ β§ π β LVec β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β 0 β§ πΉ finSupp 0 )) β ((πΉβπ) β π β ((πΉβπ) β πΈ β§ (πΉβπ) β 0 ))) |
| 20 | 9, 10, 19 | mpbir2and 712 |
. . 3
β’ (((π β π« π΅ β§ π β LVec β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β 0 β§ πΉ finSupp 0 )) β (πΉβπ) β π) |
| 21 | 20 | 3adant3 1130 |
. 2
β’ (((π β π« π΅ β§ π β LVec β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β 0 β§ πΉ finSupp 0 ) β§ (πΉ( linC βπ)π) = π) β (πΉβπ) β π) |
| 22 | | simp3 1136 |
. . 3
β’ ((πΉ β (πΈ βm π) β§ (πΉβπ) β 0 β§ πΉ finSupp 0 ) β πΉ finSupp 0 ) |
| 23 | 22 | 3ad2ant2 1132 |
. 2
β’ (((π β π« π΅ β§ π β LVec β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β 0 β§ πΉ finSupp 0 ) β§ (πΉ( linC βπ)π) = π) β πΉ finSupp 0 ) |
| 24 | | simp3 1136 |
. 2
β’ (((π β π« π΅ β§ π β LVec β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β 0 β§ πΉ finSupp 0 ) β§ (πΉ( linC βπ)π) = π) β (πΉ( linC βπ)π) = π) |
| 25 | | lincresunit.b |
. . 3
β’ π΅ = (Baseβπ) |
| 26 | | lincresunit.z |
. . 3
β’ π = (0gβπ) |
| 27 | | lincresunit.n |
. . 3
β’ π = (invgβπ
) |
| 28 | | lincresunit.i |
. . 3
β’ πΌ = (invrβπ
) |
| 29 | | lincresunit.t |
. . 3
β’ Β· =
(.rβπ
) |
| 30 | | lincresunit.g |
. . 3
β’ πΊ = (π β (π β {π}) β¦ ((πΌβ(πβ(πΉβπ))) Β· (πΉβπ ))) |
| 31 | 25, 11, 15, 16, 17, 26, 27, 28, 29, 30 | lincresunit3 47462 |
. 2
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 ) β§ (πΉ( linC βπ)π) = π) β (πΊ( linC βπ)(π β {π})) = π) |
| 32 | 3, 4, 21, 23, 24, 31 | syl131anc 1381 |
1
β’ (((π β π« π΅ β§ π β LVec β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β 0 β§ πΉ finSupp 0 ) β§ (πΉ( linC βπ)π) = π) β (πΊ( linC βπ)(π β {π})) = π) |
