Step | Hyp | Ref
| Expression |
1 | | iscvsi.1 |
. . 3
β’ π β Grp |
2 | | iscvsi.3 |
. . . 4
β’ π β DivRing |
3 | | iscvsi.2 |
. . . 4
β’ π = (βfld
βΎs πΎ) |
4 | 2, 3 | pm3.2i 472 |
. . 3
β’ (π β DivRing β§ π = (βfld
βΎs πΎ)) |
5 | | iscvsi.4 |
. . 3
β’ πΎ β
(SubRingββfld) |
6 | 1, 4, 5 | 3pm3.2i 1340 |
. 2
β’ (π β Grp β§ (π β DivRing β§ π = (βfld
βΎs πΎ))
β§ πΎ β
(SubRingββfld)) |
7 | | iscvsi.5 |
. . . 4
β’ (π₯ β π β (1 Β· π₯) = π₯) |
8 | | iscvsi.6 |
. . . . . . 7
β’ ((π¦ β πΎ β§ π₯ β π) β (π¦ Β· π₯) β π) |
9 | 8 | ancoms 460 |
. . . . . 6
β’ ((π₯ β π β§ π¦ β πΎ) β (π¦ Β· π₯) β π) |
10 | | iscvsi.7 |
. . . . . . . . 9
β’ ((π¦ β πΎ β§ π₯ β π β§ π§ β π) β (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§))) |
11 | 10 | 3com12 1124 |
. . . . . . . 8
β’ ((π₯ β π β§ π¦ β πΎ β§ π§ β π) β (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§))) |
12 | 11 | 3expa 1119 |
. . . . . . 7
β’ (((π₯ β π β§ π¦ β πΎ) β§ π§ β π) β (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§))) |
13 | 12 | ralrimiva 3140 |
. . . . . 6
β’ ((π₯ β π β§ π¦ β πΎ) β βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§))) |
14 | | iscvsi.8 |
. . . . . . . . . 10
β’ ((π¦ β πΎ β§ π§ β πΎ β§ π₯ β π) β ((π§ + π¦) Β· π₯) = ((π§ Β· π₯) + (π¦ Β· π₯))) |
15 | | iscvsi.9 |
. . . . . . . . . 10
β’ ((π¦ β πΎ β§ π§ β πΎ β§ π₯ β π) β ((π§ Β· π¦) Β· π₯) = (π§ Β· (π¦ Β· π₯))) |
16 | 14, 15 | jca 513 |
. . . . . . . . 9
β’ ((π¦ β πΎ β§ π§ β πΎ β§ π₯ β π) β (((π§ + π¦) Β· π₯) = ((π§ Β· π₯) + (π¦ Β· π₯)) β§ ((π§ Β· π¦) Β· π₯) = (π§ Β· (π¦ Β· π₯)))) |
17 | 16 | 3comr 1126 |
. . . . . . . 8
β’ ((π₯ β π β§ π¦ β πΎ β§ π§ β πΎ) β (((π§ + π¦) Β· π₯) = ((π§ Β· π₯) + (π¦ Β· π₯)) β§ ((π§ Β· π¦) Β· π₯) = (π§ Β· (π¦ Β· π₯)))) |
18 | 17 | 3expa 1119 |
. . . . . . 7
β’ (((π₯ β π β§ π¦ β πΎ) β§ π§ β πΎ) β (((π§ + π¦) Β· π₯) = ((π§ Β· π₯) + (π¦ Β· π₯)) β§ ((π§ Β· π¦) Β· π₯) = (π§ Β· (π¦ Β· π₯)))) |
19 | 18 | ralrimiva 3140 |
. . . . . 6
β’ ((π₯ β π β§ π¦ β πΎ) β βπ§ β πΎ (((π§ + π¦) Β· π₯) = ((π§ Β· π₯) + (π¦ Β· π₯)) β§ ((π§ Β· π¦) Β· π₯) = (π§ Β· (π¦ Β· π₯)))) |
20 | 9, 13, 19 | 3jca 1129 |
. . . . 5
β’ ((π₯ β π β§ π¦ β πΎ) β ((π¦ Β· π₯) β π β§ βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§)) β§ βπ§ β πΎ (((π§ + π¦) Β· π₯) = ((π§ Β· π₯) + (π¦ Β· π₯)) β§ ((π§ Β· π¦) Β· π₯) = (π§ Β· (π¦ Β· π₯))))) |
21 | 20 | ralrimiva 3140 |
. . . 4
β’ (π₯ β π β βπ¦ β πΎ ((π¦ Β· π₯) β π β§ βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§)) β§ βπ§ β πΎ (((π§ + π¦) Β· π₯) = ((π§ Β· π₯) + (π¦ Β· π₯)) β§ ((π§ Β· π¦) Β· π₯) = (π§ Β· (π¦ Β· π₯))))) |
22 | 7, 21 | jca 513 |
. . 3
β’ (π₯ β π β ((1 Β· π₯) = π₯ β§ βπ¦ β πΎ ((π¦ Β· π₯) β π β§ βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§)) β§ βπ§ β πΎ (((π§ + π¦) Β· π₯) = ((π§ Β· π₯) + (π¦ Β· π₯)) β§ ((π§ Β· π¦) Β· π₯) = (π§ Β· (π¦ Β· π₯)))))) |
23 | 22 | rgen 3063 |
. 2
β’
βπ₯ β
π ((1 Β· π₯) = π₯ β§ βπ¦ β πΎ ((π¦ Β· π₯) β π β§ βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§)) β§ βπ§ β πΎ (((π§ + π¦) Β· π₯) = ((π§ Β· π₯) + (π¦ Β· π₯)) β§ ((π§ Β· π¦) Β· π₯) = (π§ Β· (π¦ Β· π₯))))) |
24 | | iscvsp.t |
. . 3
β’ Β· = (
Β·π βπ) |
25 | | iscvsp.a |
. . 3
β’ + =
(+gβπ) |
26 | | iscvsp.v |
. . 3
β’ π = (Baseβπ) |
27 | | iscvsp.s |
. . 3
β’ π = (Scalarβπ) |
28 | | iscvsp.k |
. . 3
β’ πΎ = (Baseβπ) |
29 | 24, 25, 26, 27, 28 | iscvsp 24514 |
. 2
β’ (π β βVec β
((π β Grp β§ (π β DivRing β§ π = (βfld
βΎs πΎ))
β§ πΎ β
(SubRingββfld)) β§ βπ₯ β π ((1 Β· π₯) = π₯ β§ βπ¦ β πΎ ((π¦ Β· π₯) β π β§ βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§)) β§ βπ§ β πΎ (((π§ + π¦) Β· π₯) = ((π§ Β· π₯) + (π¦ Β· π₯)) β§ ((π§ Β· π¦) Β· π₯) = (π§ Β· (π¦ Β· π₯))))))) |
30 | 6, 23, 29 | mpbir2an 710 |
1
β’ π β
βVec |