Step | Hyp | Ref
| Expression |
1 | | slmdvsdi.v |
. . . . . . . . 9
β’ π = (Baseβπ) |
2 | | slmdvsdi.a |
. . . . . . . . 9
β’ + =
(+gβπ) |
3 | | slmdvsdi.s |
. . . . . . . . 9
β’ Β· = (
Β·π βπ) |
4 | | eqid 2733 |
. . . . . . . . 9
β’
(0gβπ) = (0gβπ) |
5 | | slmdvsdi.f |
. . . . . . . . 9
β’ πΉ = (Scalarβπ) |
6 | | slmdvsdi.k |
. . . . . . . . 9
β’ πΎ = (BaseβπΉ) |
7 | | eqid 2733 |
. . . . . . . . 9
β’
(+gβπΉ) = (+gβπΉ) |
8 | | eqid 2733 |
. . . . . . . . 9
β’
(.rβπΉ) = (.rβπΉ) |
9 | | eqid 2733 |
. . . . . . . . 9
β’
(1rβπΉ) = (1rβπΉ) |
10 | | eqid 2733 |
. . . . . . . . 9
β’
(0gβπΉ) = (0gβπΉ) |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | slmdlema 32348 |
. . . . . . . 8
β’ ((π β SLMod β§ (π
β πΎ β§ π
β πΎ) β§ (π β π β§ π β π)) β (((π
Β· π) β π β§ (π
Β· (π + π)) = ((π
Β· π) + (π
Β· π)) β§ ((π
(+gβπΉ)π
) Β· π) = ((π
Β· π) + (π
Β· π))) β§ (((π
(.rβπΉ)π
) Β· π) = (π
Β· (π
Β· π)) β§ ((1rβπΉ) Β· π) = π β§ ((0gβπΉ) Β· π) = (0gβπ)))) |
12 | 11 | simpld 496 |
. . . . . . 7
β’ ((π β SLMod β§ (π
β πΎ β§ π
β πΎ) β§ (π β π β§ π β π)) β ((π
Β· π) β π β§ (π
Β· (π + π)) = ((π
Β· π) + (π
Β· π)) β§ ((π
(+gβπΉ)π
) Β· π) = ((π
Β· π) + (π
Β· π)))) |
13 | 12 | simp2d 1144 |
. . . . . 6
β’ ((π β SLMod β§ (π
β πΎ β§ π
β πΎ) β§ (π β π β§ π β π)) β (π
Β· (π + π)) = ((π
Β· π) + (π
Β· π))) |
14 | 13 | 3expia 1122 |
. . . . 5
β’ ((π β SLMod β§ (π
β πΎ β§ π
β πΎ)) β ((π β π β§ π β π) β (π
Β· (π + π)) = ((π
Β· π) + (π
Β· π)))) |
15 | 14 | anabsan2 673 |
. . . 4
β’ ((π β SLMod β§ π
β πΎ) β ((π β π β§ π β π) β (π
Β· (π + π)) = ((π
Β· π) + (π
Β· π)))) |
16 | 15 | exp4b 432 |
. . 3
β’ (π β SLMod β (π
β πΎ β (π β π β (π β π β (π
Β· (π + π)) = ((π
Β· π) + (π
Β· π)))))) |
17 | 16 | com34 91 |
. 2
β’ (π β SLMod β (π
β πΎ β (π β π β (π β π β (π
Β· (π + π)) = ((π
Β· π) + (π
Β· π)))))) |
18 | 17 | 3imp2 1350 |
1
β’ ((π β SLMod β§ (π
β πΎ β§ π β π β§ π β π)) β (π
Β· (π + π)) = ((π
Β· π) + (π
Β· π))) |