Step | Hyp | Ref
| Expression |
1 | | eqid 2730 |
. . 3
β’
(Baseβπ) =
(Baseβπ) |
2 | | eqid 2730 |
. . 3
β’
(+gβπ) = (+gβπ) |
3 | | eqid 2730 |
. . 3
β’ (
Β·π βπ) = ( Β·π
βπ) |
4 | | eqid 2730 |
. . 3
β’
(0gβπ) = (0gβπ) |
5 | | eqid 2730 |
. . 3
β’
(Scalarβπ) =
(Scalarβπ) |
6 | | eqid 2730 |
. . 3
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
7 | | eqid 2730 |
. . 3
β’
(+gβ(Scalarβπ)) =
(+gβ(Scalarβπ)) |
8 | | eqid 2730 |
. . 3
β’
(.rβ(Scalarβπ)) =
(.rβ(Scalarβπ)) |
9 | | eqid 2730 |
. . 3
β’
(1rβ(Scalarβπ)) =
(1rβ(Scalarβπ)) |
10 | | eqid 2730 |
. . 3
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | isslmd 32617 |
. 2
β’ (π β SLMod β (π β CMnd β§
(Scalarβπ) β
SRing β§ βπ€
β (Baseβ(Scalarβπ))βπ§ β (Baseβ(Scalarβπ))βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(((π§( Β·π
βπ)π¦) β (Baseβπ) β§ (π§( Β·π
βπ)(π¦(+gβπ)π₯)) = ((π§( Β·π
βπ)π¦)(+gβπ)(π§( Β·π
βπ)π₯)) β§ ((π€(+gβ(Scalarβπ))π§)( Β·π
βπ)π¦) = ((π€( Β·π
βπ)π¦)(+gβπ)(π§( Β·π
βπ)π¦))) β§ (((π€(.rβ(Scalarβπ))π§)( Β·π
βπ)π¦) = (π€( Β·π
βπ)(π§(
Β·π βπ)π¦)) β§
((1rβ(Scalarβπ))( Β·π
βπ)π¦) = π¦ β§
((0gβ(Scalarβπ))( Β·π
βπ)π¦) = (0gβπ))))) |
12 | 11 | simp1bi 1143 |
1
β’ (π β SLMod β π β CMnd) |