Step | Hyp | Ref
| Expression |
1 | | elex 3465 |
. . 3
β’ (π β π β π β V) |
2 | 1 | adantr 482 |
. 2
β’ ((π β π β§ π β π« π΅) β π β V) |
3 | | lcoop.b |
. . . . . 6
β’ π΅ = (Baseβπ) |
4 | 3 | pweqi 4580 |
. . . . 5
β’ π«
π΅ = π«
(Baseβπ) |
5 | 4 | eleq2i 2826 |
. . . 4
β’ (π β π« π΅ β π β π« (Baseβπ)) |
6 | 5 | biimpi 215 |
. . 3
β’ (π β π« π΅ β π β π« (Baseβπ)) |
7 | 6 | adantl 483 |
. 2
β’ ((π β π β§ π β π« π΅) β π β π« (Baseβπ)) |
8 | 3 | fvexi 6860 |
. . 3
β’ π΅ β V |
9 | | rabexg 5292 |
. . 3
β’ (π΅ β V β {π β π΅ β£ βπ β (π
βm π)(π finSupp (0gβπ) β§ π = (π ( linC βπ)π))} β V) |
10 | 8, 9 | mp1i 13 |
. 2
β’ ((π β π β§ π β π« π΅) β {π β π΅ β£ βπ β (π
βm π)(π finSupp (0gβπ) β§ π = (π ( linC βπ)π))} β V) |
11 | | fveq2 6846 |
. . . . . 6
β’ (π = π β (Baseβπ) = (Baseβπ)) |
12 | 11, 3 | eqtr4di 2791 |
. . . . 5
β’ (π = π β (Baseβπ) = π΅) |
13 | 12 | adantr 482 |
. . . 4
β’ ((π = π β§ π£ = π) β (Baseβπ) = π΅) |
14 | | 2fveq3 6851 |
. . . . . . . 8
β’ (π = π β (Baseβ(Scalarβπ)) =
(Baseβ(Scalarβπ))) |
15 | 14 | adantr 482 |
. . . . . . 7
β’ ((π = π β§ π£ = π) β (Baseβ(Scalarβπ)) =
(Baseβ(Scalarβπ))) |
16 | | lcoop.r |
. . . . . . . 8
β’ π
= (Baseβπ) |
17 | | lcoop.s |
. . . . . . . . 9
β’ π = (Scalarβπ) |
18 | 17 | fveq2i 6849 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβ(Scalarβπ)) |
19 | 16, 18 | eqtri 2761 |
. . . . . . 7
β’ π
=
(Baseβ(Scalarβπ)) |
20 | 15, 19 | eqtr4di 2791 |
. . . . . 6
β’ ((π = π β§ π£ = π) β (Baseβ(Scalarβπ)) = π
) |
21 | | simpr 486 |
. . . . . 6
β’ ((π = π β§ π£ = π) β π£ = π) |
22 | 20, 21 | oveq12d 7379 |
. . . . 5
β’ ((π = π β§ π£ = π) β ((Baseβ(Scalarβπ)) βm π£) = (π
βm π)) |
23 | | 2fveq3 6851 |
. . . . . . . . 9
β’ (π = π β
(0gβ(Scalarβπ)) = (0gβ(Scalarβπ))) |
24 | 17 | a1i 11 |
. . . . . . . . . . 11
β’ (π = π β π = (Scalarβπ)) |
25 | 24 | eqcomd 2739 |
. . . . . . . . . 10
β’ (π = π β (Scalarβπ) = π) |
26 | 25 | fveq2d 6850 |
. . . . . . . . 9
β’ (π = π β
(0gβ(Scalarβπ)) = (0gβπ)) |
27 | 23, 26 | eqtrd 2773 |
. . . . . . . 8
β’ (π = π β
(0gβ(Scalarβπ)) = (0gβπ)) |
28 | 27 | adantr 482 |
. . . . . . 7
β’ ((π = π β§ π£ = π) β
(0gβ(Scalarβπ)) = (0gβπ)) |
29 | 28 | breq2d 5121 |
. . . . . 6
β’ ((π = π β§ π£ = π) β (π finSupp
(0gβ(Scalarβπ)) β π finSupp (0gβπ))) |
30 | | fveq2 6846 |
. . . . . . . . 9
β’ (π = π β ( linC βπ) = ( linC βπ)) |
31 | 30 | adantr 482 |
. . . . . . . 8
β’ ((π = π β§ π£ = π) β ( linC βπ) = ( linC βπ)) |
32 | | eqidd 2734 |
. . . . . . . 8
β’ ((π = π β§ π£ = π) β π = π ) |
33 | 31, 32, 21 | oveq123d 7382 |
. . . . . . 7
β’ ((π = π β§ π£ = π) β (π ( linC βπ)π£) = (π ( linC βπ)π)) |
34 | 33 | eqeq2d 2744 |
. . . . . 6
β’ ((π = π β§ π£ = π) β (π = (π ( linC βπ)π£) β π = (π ( linC βπ)π))) |
35 | 29, 34 | anbi12d 632 |
. . . . 5
β’ ((π = π β§ π£ = π) β ((π finSupp
(0gβ(Scalarβπ)) β§ π = (π ( linC βπ)π£)) β (π finSupp (0gβπ) β§ π = (π ( linC βπ)π)))) |
36 | 22, 35 | rexeqbidv 3319 |
. . . 4
β’ ((π = π β§ π£ = π) β (βπ β ((Baseβ(Scalarβπ)) βm π£)(π finSupp
(0gβ(Scalarβπ)) β§ π = (π ( linC βπ)π£)) β βπ β (π
βm π)(π finSupp (0gβπ) β§ π = (π ( linC βπ)π)))) |
37 | 13, 36 | rabeqbidv 3423 |
. . 3
β’ ((π = π β§ π£ = π) β {π β (Baseβπ) β£ βπ β ((Baseβ(Scalarβπ)) βm π£)(π finSupp
(0gβ(Scalarβπ)) β§ π = (π ( linC βπ)π£))} = {π β π΅ β£ βπ β (π
βm π)(π finSupp (0gβπ) β§ π = (π ( linC βπ)π))}) |
38 | 11 | pweqd 4581 |
. . 3
β’ (π = π β π« (Baseβπ) = π« (Baseβπ)) |
39 | | df-lco 46578 |
. . 3
β’ LinCo =
(π β V, π£ β π«
(Baseβπ) β¦
{π β (Baseβπ) β£ βπ β
((Baseβ(Scalarβπ)) βm π£)(π finSupp
(0gβ(Scalarβπ)) β§ π = (π ( linC βπ)π£))}) |
40 | 37, 38, 39 | ovmpox 7512 |
. 2
β’ ((π β V β§ π β π«
(Baseβπ) β§ {π β π΅ β£ βπ β (π
βm π)(π finSupp (0gβπ) β§ π = (π ( linC βπ)π))} β V) β (π LinCo π) = {π β π΅ β£ βπ β (π
βm π)(π finSupp (0gβπ) β§ π = (π ( linC βπ)π))}) |
41 | 2, 7, 10, 40 | syl3anc 1372 |
1
β’ ((π β π β§ π β π« π΅) β (π LinCo π) = {π β π΅ β£ βπ β (π
βm π)(π finSupp (0gβπ) β§ π = (π ( linC βπ)π))}) |