Step | Hyp | Ref
| Expression |
1 | | iscvs 24643 |
. 2
β’ (π β βVec β (π β βMod β§
(Scalarβπ) β
DivRing)) |
2 | | iscvsp.t |
. . . . 5
β’ Β· = (
Β·π βπ) |
3 | | iscvsp.a |
. . . . 5
β’ + =
(+gβπ) |
4 | | iscvsp.v |
. . . . 5
β’ π = (Baseβπ) |
5 | | iscvsp.s |
. . . . 5
β’ π = (Scalarβπ) |
6 | | iscvsp.k |
. . . . 5
β’ πΎ = (Baseβπ) |
7 | 2, 3, 4, 5, 6 | isclmp 24613 |
. . . 4
β’ (π β βMod β
((π β Grp β§ π = (βfld
βΎs πΎ)
β§ πΎ β
(SubRingββfld)) β§ βπ₯ β π ((1 Β· π₯) = π₯ β§ βπ¦ β πΎ ((π¦ Β· π₯) β π β§ βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§)) β§ βπ§ β πΎ (((π§ + π¦) Β· π₯) = ((π§ Β· π₯) + (π¦ Β· π₯)) β§ ((π§ Β· π¦) Β· π₯) = (π§ Β· (π¦ Β· π₯))))))) |
8 | 7 | anbi2ci 626 |
. . 3
β’ ((π β βMod β§
(Scalarβπ) β
DivRing) β ((Scalarβπ) β DivRing β§ ((π β Grp β§ π = (βfld
βΎs πΎ)
β§ πΎ β
(SubRingββfld)) β§ βπ₯ β π ((1 Β· π₯) = π₯ β§ βπ¦ β πΎ ((π¦ Β· π₯) β π β§ βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§)) β§ βπ§ β πΎ (((π§ + π¦) Β· π₯) = ((π§ Β· π₯) + (π¦ Β· π₯)) β§ ((π§ Β· π¦) Β· π₯) = (π§ Β· (π¦ Β· π₯)))))))) |
9 | | anass 470 |
. . 3
β’
((((Scalarβπ)
β DivRing β§ (π
β Grp β§ π =
(βfld βΎs πΎ) β§ πΎ β
(SubRingββfld))) β§ βπ₯ β π ((1 Β· π₯) = π₯ β§ βπ¦ β πΎ ((π¦ Β· π₯) β π β§ βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§)) β§ βπ§ β πΎ (((π§ + π¦) Β· π₯) = ((π§ Β· π₯) + (π¦ Β· π₯)) β§ ((π§ Β· π¦) Β· π₯) = (π§ Β· (π¦ Β· π₯)))))) β ((Scalarβπ) β DivRing β§ ((π β Grp β§ π = (βfld
βΎs πΎ)
β§ πΎ β
(SubRingββfld)) β§ βπ₯ β π ((1 Β· π₯) = π₯ β§ βπ¦ β πΎ ((π¦ Β· π₯) β π β§ βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§)) β§ βπ§ β πΎ (((π§ + π¦) Β· π₯) = ((π§ Β· π₯) + (π¦ Β· π₯)) β§ ((π§ Β· π¦) Β· π₯) = (π§ Β· (π¦ Β· π₯)))))))) |
10 | | 3anan12 1097 |
. . . . . . 7
β’ ((π β Grp β§ π = (βfld
βΎs πΎ)
β§ πΎ β
(SubRingββfld)) β (π = (βfld
βΎs πΎ)
β§ (π β Grp β§
πΎ β
(SubRingββfld)))) |
11 | 10 | anbi2i 624 |
. . . . . 6
β’
(((Scalarβπ)
β DivRing β§ (π
β Grp β§ π =
(βfld βΎs πΎ) β§ πΎ β
(SubRingββfld))) β ((Scalarβπ) β DivRing β§ (π = (βfld
βΎs πΎ)
β§ (π β Grp β§
πΎ β
(SubRingββfld))))) |
12 | | anass 470 |
. . . . . 6
β’
((((Scalarβπ)
β DivRing β§ π =
(βfld βΎs πΎ)) β§ (π β Grp β§ πΎ β
(SubRingββfld))) β ((Scalarβπ) β DivRing β§ (π = (βfld
βΎs πΎ)
β§ (π β Grp β§
πΎ β
(SubRingββfld))))) |
13 | 5 | eqcomi 2742 |
. . . . . . . . 9
β’
(Scalarβπ) =
π |
14 | 13 | eleq1i 2825 |
. . . . . . . 8
β’
((Scalarβπ)
β DivRing β π
β DivRing) |
15 | 14 | anbi1i 625 |
. . . . . . 7
β’
(((Scalarβπ)
β DivRing β§ π =
(βfld βΎs πΎ)) β (π β DivRing β§ π = (βfld
βΎs πΎ))) |
16 | 15 | anbi1i 625 |
. . . . . 6
β’
((((Scalarβπ)
β DivRing β§ π =
(βfld βΎs πΎ)) β§ (π β Grp β§ πΎ β
(SubRingββfld))) β ((π β DivRing β§ π = (βfld
βΎs πΎ))
β§ (π β Grp β§
πΎ β
(SubRingββfld)))) |
17 | 11, 12, 16 | 3bitr2i 299 |
. . . . 5
β’
(((Scalarβπ)
β DivRing β§ (π
β Grp β§ π =
(βfld βΎs πΎ) β§ πΎ β
(SubRingββfld))) β ((π β DivRing β§ π = (βfld
βΎs πΎ))
β§ (π β Grp β§
πΎ β
(SubRingββfld)))) |
18 | | 3anan12 1097 |
. . . . 5
β’ ((π β Grp β§ (π β DivRing β§ π = (βfld
βΎs πΎ))
β§ πΎ β
(SubRingββfld)) β ((π β DivRing β§ π = (βfld
βΎs πΎ))
β§ (π β Grp β§
πΎ β
(SubRingββfld)))) |
19 | 17, 18 | bitr4i 278 |
. . . 4
β’
(((Scalarβπ)
β DivRing β§ (π
β Grp β§ π =
(βfld βΎs πΎ) β§ πΎ β
(SubRingββfld))) β (π β Grp β§ (π β DivRing β§ π = (βfld
βΎs πΎ))
β§ πΎ β
(SubRingββfld))) |
20 | 19 | anbi1i 625 |
. . 3
β’
((((Scalarβπ)
β DivRing β§ (π
β Grp β§ π =
(βfld βΎs πΎ) β§ πΎ β
(SubRingββfld))) β§ βπ₯ β π ((1 Β· π₯) = π₯ β§ βπ¦ β πΎ ((π¦ Β· π₯) β π β§ βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§)) β§ βπ§ β πΎ (((π§ + π¦) Β· π₯) = ((π§ Β· π₯) + (π¦ Β· π₯)) β§ ((π§ Β· π¦) Β· π₯) = (π§ Β· (π¦ Β· π₯)))))) β ((π β Grp β§ (π β DivRing β§ π = (βfld
βΎs πΎ))
β§ πΎ β
(SubRingββfld)) β§ βπ₯ β π ((1 Β· π₯) = π₯ β§ βπ¦ β πΎ ((π¦ Β· π₯) β π β§ βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§)) β§ βπ§ β πΎ (((π§ + π¦) Β· π₯) = ((π§ Β· π₯) + (π¦ Β· π₯)) β§ ((π§ Β· π¦) Β· π₯) = (π§ Β· (π¦ Β· π₯))))))) |
21 | 8, 9, 20 | 3bitr2i 299 |
. 2
β’ ((π β βMod β§
(Scalarβπ) β
DivRing) β ((π β
Grp β§ (π β DivRing
β§ π =
(βfld βΎs πΎ)) β§ πΎ β
(SubRingββfld)) β§ βπ₯ β π ((1 Β· π₯) = π₯ β§ βπ¦ β πΎ ((π¦ Β· π₯) β π β§ βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§)) β§ βπ§ β πΎ (((π§ + π¦) Β· π₯) = ((π§ Β· π₯) + (π¦ Β· π₯)) β§ ((π§ Β· π¦) Β· π₯) = (π§ Β· (π¦ Β· π₯))))))) |
22 | 1, 21 | bitri 275 |
1
β’ (π β βVec β
((π β Grp β§ (π β DivRing β§ π = (βfld
βΎs πΎ))
β§ πΎ β
(SubRingββfld)) β§ βπ₯ β π ((1 Β· π₯) = π₯ β§ βπ¦ β πΎ ((π¦ Β· π₯) β π β§ βπ§ β π (π¦ Β· (π₯ + π§)) = ((π¦ Β· π₯) + (π¦ Β· π§)) β§ βπ§ β πΎ (((π§ + π¦) Β· π₯) = ((π§ Β· π₯) + (π¦ Β· π₯)) β§ ((π§ Β· π¦) Β· π₯) = (π§ Β· (π¦ Β· π₯))))))) |