Step | Hyp | Ref
| Expression |
1 | | elelpwi 4613 |
. . . . . . 7
β’ ((π£ β π β§ π β π« (Baseβπ)) β π£ β (Baseβπ)) |
2 | 1 | expcom 415 |
. . . . . 6
β’ (π β π«
(Baseβπ) β
(π£ β π β π£ β (Baseβπ))) |
3 | 2 | adantl 483 |
. . . . 5
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
(π£ β π β π£ β (Baseβπ))) |
4 | 3 | imp 408 |
. . . 4
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ π£ β π) β π£ β (Baseβπ)) |
5 | | eqid 2733 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβπ) |
6 | | eqid 2733 |
. . . . . . 7
β’
(Scalarβπ) =
(Scalarβπ) |
7 | | eqid 2733 |
. . . . . . 7
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
8 | | eqid 2733 |
. . . . . . 7
β’
(1rβ(Scalarβπ)) =
(1rβ(Scalarβπ)) |
9 | | equequ1 2029 |
. . . . . . . . 9
β’ (π₯ = π¦ β (π₯ = π£ β π¦ = π£)) |
10 | 9 | ifbid 4552 |
. . . . . . . 8
β’ (π₯ = π¦ β if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ))) = if(π¦ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ)))) |
11 | 10 | cbvmptv 5262 |
. . . . . . 7
β’ (π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ)))) = (π¦ β π β¦ if(π¦ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ)))) |
12 | 5, 6, 7, 8, 11 | mptcfsupp 47056 |
. . . . . 6
β’ ((π β LMod β§ π β π«
(Baseβπ) β§ π£ β π) β (π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ)))) finSupp
(0gβ(Scalarβπ))) |
13 | 12 | 3expa 1119 |
. . . . 5
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ π£ β π) β (π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ)))) finSupp
(0gβ(Scalarβπ))) |
14 | | eqid 2733 |
. . . . . . . 8
β’ (π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ)))) = (π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ)))) |
15 | 5, 6, 7, 8, 14 | linc1 47106 |
. . . . . . 7
β’ ((π β LMod β§ π β π«
(Baseβπ) β§ π£ β π) β ((π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ))))( linC βπ)π) = π£) |
16 | 15 | 3expa 1119 |
. . . . . 6
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ π£ β π) β ((π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ))))( linC βπ)π) = π£) |
17 | 16 | eqcomd 2739 |
. . . . 5
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ π£ β π) β π£ = ((π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ))))( linC βπ)π)) |
18 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
19 | 6, 18, 8 | lmod1cl 20499 |
. . . . . . . . . 10
β’ (π β LMod β
(1rβ(Scalarβπ)) β (Baseβ(Scalarβπ))) |
20 | 6, 18, 7 | lmod0cl 20498 |
. . . . . . . . . 10
β’ (π β LMod β
(0gβ(Scalarβπ)) β (Baseβ(Scalarβπ))) |
21 | 19, 20 | ifcld 4575 |
. . . . . . . . 9
β’ (π β LMod β if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ))) β (Baseβ(Scalarβπ))) |
22 | 21 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§ π£ β π) β§ π₯ β π) β if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ))) β (Baseβ(Scalarβπ))) |
23 | 22 | fmpttd 7115 |
. . . . . . 7
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ π£ β π) β (π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ)))):πβΆ(Baseβ(Scalarβπ))) |
24 | | fvex 6905 |
. . . . . . . 8
β’
(Baseβ(Scalarβπ)) β V |
25 | | simplr 768 |
. . . . . . . 8
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ π£ β π) β π β π« (Baseβπ)) |
26 | | elmapg 8833 |
. . . . . . . 8
β’
(((Baseβ(Scalarβπ)) β V β§ π β π« (Baseβπ)) β ((π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ)))) β ((Baseβ(Scalarβπ)) βm π) β (π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ)))):πβΆ(Baseβ(Scalarβπ)))) |
27 | 24, 25, 26 | sylancr 588 |
. . . . . . 7
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ π£ β π) β ((π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ)))) β ((Baseβ(Scalarβπ)) βm π) β (π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ)))):πβΆ(Baseβ(Scalarβπ)))) |
28 | 23, 27 | mpbird 257 |
. . . . . 6
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ π£ β π) β (π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ)))) β ((Baseβ(Scalarβπ)) βm π)) |
29 | | breq1 5152 |
. . . . . . . 8
β’ (π = (π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ)))) β (π finSupp
(0gβ(Scalarβπ)) β (π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ)))) finSupp
(0gβ(Scalarβπ)))) |
30 | | oveq1 7416 |
. . . . . . . . 9
β’ (π = (π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ)))) β (π( linC βπ)π) = ((π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ))))( linC βπ)π)) |
31 | 30 | eqeq2d 2744 |
. . . . . . . 8
β’ (π = (π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ)))) β (π£ = (π( linC βπ)π) β π£ = ((π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ))))( linC βπ)π))) |
32 | 29, 31 | anbi12d 632 |
. . . . . . 7
β’ (π = (π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ)))) β ((π finSupp
(0gβ(Scalarβπ)) β§ π£ = (π( linC βπ)π)) β ((π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ)))) finSupp
(0gβ(Scalarβπ)) β§ π£ = ((π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ))))( linC βπ)π)))) |
33 | 32 | adantl 483 |
. . . . . 6
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§ π£ β π) β§ π = (π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ))))) β ((π finSupp
(0gβ(Scalarβπ)) β§ π£ = (π( linC βπ)π)) β ((π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ)))) finSupp
(0gβ(Scalarβπ)) β§ π£ = ((π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ))))( linC βπ)π)))) |
34 | 28, 33 | rspcedv 3606 |
. . . . 5
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ π£ β π) β (((π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ)))) finSupp
(0gβ(Scalarβπ)) β§ π£ = ((π₯ β π β¦ if(π₯ = π£, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ))))( linC βπ)π)) β βπ β ((Baseβ(Scalarβπ)) βm π)(π finSupp
(0gβ(Scalarβπ)) β§ π£ = (π( linC βπ)π)))) |
35 | 13, 17, 34 | mp2and 698 |
. . . 4
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ π£ β π) β βπ β ((Baseβ(Scalarβπ)) βm π)(π finSupp
(0gβ(Scalarβπ)) β§ π£ = (π( linC βπ)π))) |
36 | 5, 6, 18 | lcoval 47093 |
. . . . 5
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
(π£ β (π LinCo π) β (π£ β (Baseβπ) β§ βπ β ((Baseβ(Scalarβπ)) βm π)(π finSupp
(0gβ(Scalarβπ)) β§ π£ = (π( linC βπ)π))))) |
37 | 36 | adantr 482 |
. . . 4
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ π£ β π) β (π£ β (π LinCo π) β (π£ β (Baseβπ) β§ βπ β ((Baseβ(Scalarβπ)) βm π)(π finSupp
(0gβ(Scalarβπ)) β§ π£ = (π( linC βπ)π))))) |
38 | 4, 35, 37 | mpbir2and 712 |
. . 3
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ π£ β π) β π£ β (π LinCo π)) |
39 | 38 | ex 414 |
. 2
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
(π£ β π β π£ β (π LinCo π))) |
40 | 39 | ssrdv 3989 |
1
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
π β (π LinCo π)) |