Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. . . 4
β’ ((π = π β§ π = π) β π = π) |
2 | | fveq2 6888 |
. . . . . . 7
β’ (π = π β (Baseβπ) = (Baseβπ)) |
3 | | islininds.b |
. . . . . . 7
β’ π΅ = (Baseβπ) |
4 | 2, 3 | eqtr4di 2790 |
. . . . . 6
β’ (π = π β (Baseβπ) = π΅) |
5 | 4 | adantl 482 |
. . . . 5
β’ ((π = π β§ π = π) β (Baseβπ) = π΅) |
6 | 5 | pweqd 4618 |
. . . 4
β’ ((π = π β§ π = π) β π« (Baseβπ) = π« π΅) |
7 | 1, 6 | eleq12d 2827 |
. . 3
β’ ((π = π β§ π = π) β (π β π« (Baseβπ) β π β π« π΅)) |
8 | | fveq2 6888 |
. . . . . . . . 9
β’ (π = π β (Scalarβπ) = (Scalarβπ)) |
9 | | islininds.r |
. . . . . . . . 9
β’ π
= (Scalarβπ) |
10 | 8, 9 | eqtr4di 2790 |
. . . . . . . 8
β’ (π = π β (Scalarβπ) = π
) |
11 | 10 | fveq2d 6892 |
. . . . . . 7
β’ (π = π β (Baseβ(Scalarβπ)) = (Baseβπ
)) |
12 | | islininds.e |
. . . . . . 7
β’ πΈ = (Baseβπ
) |
13 | 11, 12 | eqtr4di 2790 |
. . . . . 6
β’ (π = π β (Baseβ(Scalarβπ)) = πΈ) |
14 | 13 | adantl 482 |
. . . . 5
β’ ((π = π β§ π = π) β (Baseβ(Scalarβπ)) = πΈ) |
15 | 14, 1 | oveq12d 7423 |
. . . 4
β’ ((π = π β§ π = π) β ((Baseβ(Scalarβπ)) βm π ) = (πΈ βm π)) |
16 | 8 | adantl 482 |
. . . . . . . . . 10
β’ ((π = π β§ π = π) β (Scalarβπ) = (Scalarβπ)) |
17 | 16, 9 | eqtr4di 2790 |
. . . . . . . . 9
β’ ((π = π β§ π = π) β (Scalarβπ) = π
) |
18 | 17 | fveq2d 6892 |
. . . . . . . 8
β’ ((π = π β§ π = π) β
(0gβ(Scalarβπ)) = (0gβπ
)) |
19 | | islininds.0 |
. . . . . . . 8
β’ 0 =
(0gβπ
) |
20 | 18, 19 | eqtr4di 2790 |
. . . . . . 7
β’ ((π = π β§ π = π) β
(0gβ(Scalarβπ)) = 0 ) |
21 | 20 | breq2d 5159 |
. . . . . 6
β’ ((π = π β§ π = π) β (π finSupp
(0gβ(Scalarβπ)) β π finSupp 0 )) |
22 | | fveq2 6888 |
. . . . . . . . 9
β’ (π = π β ( linC βπ) = ( linC βπ)) |
23 | 22 | adantl 482 |
. . . . . . . 8
β’ ((π = π β§ π = π) β ( linC βπ) = ( linC βπ)) |
24 | | eqidd 2733 |
. . . . . . . 8
β’ ((π = π β§ π = π) β π = π) |
25 | 23, 24, 1 | oveq123d 7426 |
. . . . . . 7
β’ ((π = π β§ π = π) β (π( linC βπ)π ) = (π( linC βπ)π)) |
26 | | fveq2 6888 |
. . . . . . . . 9
β’ (π = π β (0gβπ) = (0gβπ)) |
27 | 26 | adantl 482 |
. . . . . . . 8
β’ ((π = π β§ π = π) β (0gβπ) = (0gβπ)) |
28 | | islininds.z |
. . . . . . . 8
β’ π = (0gβπ) |
29 | 27, 28 | eqtr4di 2790 |
. . . . . . 7
β’ ((π = π β§ π = π) β (0gβπ) = π) |
30 | 25, 29 | eqeq12d 2748 |
. . . . . 6
β’ ((π = π β§ π = π) β ((π( linC βπ)π ) = (0gβπ) β (π( linC βπ)π) = π)) |
31 | 21, 30 | anbi12d 631 |
. . . . 5
β’ ((π = π β§ π = π) β ((π finSupp
(0gβ(Scalarβπ)) β§ (π( linC βπ)π ) = (0gβπ)) β (π finSupp 0 β§ (π( linC βπ)π) = π))) |
32 | 10 | fveq2d 6892 |
. . . . . . . . 9
β’ (π = π β
(0gβ(Scalarβπ)) = (0gβπ
)) |
33 | 32, 19 | eqtr4di 2790 |
. . . . . . . 8
β’ (π = π β
(0gβ(Scalarβπ)) = 0 ) |
34 | 33 | adantl 482 |
. . . . . . 7
β’ ((π = π β§ π = π) β
(0gβ(Scalarβπ)) = 0 ) |
35 | 34 | eqeq2d 2743 |
. . . . . 6
β’ ((π = π β§ π = π) β ((πβπ₯) = (0gβ(Scalarβπ)) β (πβπ₯) = 0 )) |
36 | 1, 35 | raleqbidv 3342 |
. . . . 5
β’ ((π = π β§ π = π) β (βπ₯ β π (πβπ₯) = (0gβ(Scalarβπ)) β βπ₯ β π (πβπ₯) = 0 )) |
37 | 31, 36 | imbi12d 344 |
. . . 4
β’ ((π = π β§ π = π) β (((π finSupp
(0gβ(Scalarβπ)) β§ (π( linC βπ)π ) = (0gβπ)) β βπ₯ β π (πβπ₯) = (0gβ(Scalarβπ))) β ((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) |
38 | 15, 37 | raleqbidv 3342 |
. . 3
β’ ((π = π β§ π = π) β (βπ β ((Baseβ(Scalarβπ)) βm π )((π finSupp
(0gβ(Scalarβπ)) β§ (π( linC βπ)π ) = (0gβπ)) β βπ₯ β π (πβπ₯) = (0gβ(Scalarβπ))) β βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) |
39 | 7, 38 | anbi12d 631 |
. 2
β’ ((π = π β§ π = π) β ((π β π« (Baseβπ) β§ βπ β
((Baseβ(Scalarβπ)) βm π )((π finSupp
(0gβ(Scalarβπ)) β§ (π( linC βπ)π ) = (0gβπ)) β βπ₯ β π (πβπ₯) = (0gβ(Scalarβπ)))) β (π β π« π΅ β§ βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 )))) |
40 | | df-lininds 47076 |
. 2
β’ linIndS
= {β¨π , πβ© β£ (π β π«
(Baseβπ) β§
βπ β
((Baseβ(Scalarβπ)) βm π )((π finSupp
(0gβ(Scalarβπ)) β§ (π( linC βπ)π ) = (0gβπ)) β βπ₯ β π (πβπ₯) = (0gβ(Scalarβπ))))} |
41 | 39, 40 | brabga 5533 |
1
β’ ((π β π β§ π β π) β (π linIndS π β (π β π« π΅ β§ βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 )))) |