Step | Hyp | Ref
| Expression |
1 | | ral0 4513 |
. . . . . 6
β’
βπ₯ β
β
(β
βπ₯) =
(0gβ(Scalarβπ)) |
2 | 1 | 2a1i 12 |
. . . . 5
β’ (π β π β ((β
finSupp
(0gβ(Scalarβπ)) β§ (β
( linC βπ)β
) =
(0gβπ))
β βπ₯ β
β
(β
βπ₯) =
(0gβ(Scalarβπ)))) |
3 | | 0ex 5308 |
. . . . . 6
β’ β
β V |
4 | | breq1 5152 |
. . . . . . . . 9
β’ (π = β
β (π finSupp
(0gβ(Scalarβπ)) β β
finSupp
(0gβ(Scalarβπ)))) |
5 | | oveq1 7416 |
. . . . . . . . . 10
β’ (π = β
β (π( linC βπ)β
) = (β
( linC βπ)β
)) |
6 | 5 | eqeq1d 2735 |
. . . . . . . . 9
β’ (π = β
β ((π( linC βπ)β
) = (0gβπ) β (β
( linC
βπ)β
) =
(0gβπ))) |
7 | 4, 6 | anbi12d 632 |
. . . . . . . 8
β’ (π = β
β ((π finSupp
(0gβ(Scalarβπ)) β§ (π( linC βπ)β
) = (0gβπ)) β (β
finSupp
(0gβ(Scalarβπ)) β§ (β
( linC βπ)β
) =
(0gβπ)))) |
8 | | fveq1 6891 |
. . . . . . . . . 10
β’ (π = β
β (πβπ₯) = (β
βπ₯)) |
9 | 8 | eqeq1d 2735 |
. . . . . . . . 9
β’ (π = β
β ((πβπ₯) = (0gβ(Scalarβπ)) β (β
βπ₯) =
(0gβ(Scalarβπ)))) |
10 | 9 | ralbidv 3178 |
. . . . . . . 8
β’ (π = β
β (βπ₯ β β
(πβπ₯) = (0gβ(Scalarβπ)) β βπ₯ β β
(β
βπ₯) =
(0gβ(Scalarβπ)))) |
11 | 7, 10 | imbi12d 345 |
. . . . . . 7
β’ (π = β
β (((π finSupp
(0gβ(Scalarβπ)) β§ (π( linC βπ)β
) = (0gβπ)) β βπ₯ β β
(πβπ₯) = (0gβ(Scalarβπ))) β ((β
finSupp
(0gβ(Scalarβπ)) β§ (β
( linC βπ)β
) =
(0gβπ))
β βπ₯ β
β
(β
βπ₯) =
(0gβ(Scalarβπ))))) |
12 | 11 | ralsng 4678 |
. . . . . 6
β’ (β
β V β (βπ
β {β
} ((π
finSupp (0gβ(Scalarβπ)) β§ (π( linC βπ)β
) = (0gβπ)) β βπ₯ β β
(πβπ₯) = (0gβ(Scalarβπ))) β ((β
finSupp
(0gβ(Scalarβπ)) β§ (β
( linC βπ)β
) =
(0gβπ))
β βπ₯ β
β
(β
βπ₯) =
(0gβ(Scalarβπ))))) |
13 | 3, 12 | mp1i 13 |
. . . . 5
β’ (π β π β (βπ β {β
} ((π finSupp
(0gβ(Scalarβπ)) β§ (π( linC βπ)β
) = (0gβπ)) β βπ₯ β β
(πβπ₯) = (0gβ(Scalarβπ))) β ((β
finSupp
(0gβ(Scalarβπ)) β§ (β
( linC βπ)β
) =
(0gβπ))
β βπ₯ β
β
(β
βπ₯) =
(0gβ(Scalarβπ))))) |
14 | 2, 13 | mpbird 257 |
. . . 4
β’ (π β π β βπ β {β
} ((π finSupp
(0gβ(Scalarβπ)) β§ (π( linC βπ)β
) = (0gβπ)) β βπ₯ β β
(πβπ₯) = (0gβ(Scalarβπ)))) |
15 | | fvex 6905 |
. . . . . . 7
β’
(Baseβ(Scalarβπ)) β V |
16 | | map0e 8876 |
. . . . . . 7
β’
((Baseβ(Scalarβπ)) β V β
((Baseβ(Scalarβπ)) βm β
) =
1o) |
17 | 15, 16 | mp1i 13 |
. . . . . 6
β’ (π β π β ((Baseβ(Scalarβπ)) βm β
) =
1o) |
18 | | df1o2 8473 |
. . . . . 6
β’
1o = {β
} |
19 | 17, 18 | eqtrdi 2789 |
. . . . 5
β’ (π β π β ((Baseβ(Scalarβπ)) βm β
) =
{β
}) |
20 | 19 | raleqdv 3326 |
. . . 4
β’ (π β π β (βπ β ((Baseβ(Scalarβπ)) βm
β
)((π finSupp
(0gβ(Scalarβπ)) β§ (π( linC βπ)β
) = (0gβπ)) β βπ₯ β β
(πβπ₯) = (0gβ(Scalarβπ))) β βπ β {β
} ((π finSupp
(0gβ(Scalarβπ)) β§ (π( linC βπ)β
) = (0gβπ)) β βπ₯ β β
(πβπ₯) = (0gβ(Scalarβπ))))) |
21 | 14, 20 | mpbird 257 |
. . 3
β’ (π β π β βπ β ((Baseβ(Scalarβπ)) βm
β
)((π finSupp
(0gβ(Scalarβπ)) β§ (π( linC βπ)β
) = (0gβπ)) β βπ₯ β β
(πβπ₯) = (0gβ(Scalarβπ)))) |
22 | | 0elpw 5355 |
. . 3
β’ β
β π« (Baseβπ) |
23 | 21, 22 | jctil 521 |
. 2
β’ (π β π β (β
β π«
(Baseβπ) β§
βπ β
((Baseβ(Scalarβπ)) βm β
)((π finSupp
(0gβ(Scalarβπ)) β§ (π( linC βπ)β
) = (0gβπ)) β βπ₯ β β
(πβπ₯) = (0gβ(Scalarβπ))))) |
24 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
25 | | eqid 2733 |
. . . 4
β’
(0gβπ) = (0gβπ) |
26 | | eqid 2733 |
. . . 4
β’
(Scalarβπ) =
(Scalarβπ) |
27 | | eqid 2733 |
. . . 4
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
28 | | eqid 2733 |
. . . 4
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
29 | 24, 25, 26, 27, 28 | islininds 47127 |
. . 3
β’ ((β
β V β§ π β
π) β (β
linIndS
π β (β
β
π« (Baseβπ)
β§ βπ β
((Baseβ(Scalarβπ)) βm β
)((π finSupp
(0gβ(Scalarβπ)) β§ (π( linC βπ)β
) = (0gβπ)) β βπ₯ β β
(πβπ₯) = (0gβ(Scalarβπ)))))) |
30 | 3, 29 | mpan 689 |
. 2
β’ (π β π β (β
linIndS π β (β
β π«
(Baseβπ) β§
βπ β
((Baseβ(Scalarβπ)) βm β
)((π finSupp
(0gβ(Scalarβπ)) β§ (π( linC βπ)β
) = (0gβπ)) β βπ₯ β β
(πβπ₯) = (0gβ(Scalarβπ)))))) |
31 | 23, 30 | mpbird 257 |
1
β’ (π β π β β
linIndS π) |