Step | Hyp | Ref
| Expression |
1 | | elq 12882 |
. . 3
β’ (π§ β β β
βπ₯ β β€
βπ¦ β β
π§ = (π₯ / π¦)) |
2 | | drngring 20206 |
. . . . . . . 8
β’
((βfld βΎs π
) β DivRing β
(βfld βΎs π
) β Ring) |
3 | 2 | ad2antlr 726 |
. . . . . . 7
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β (βfld βΎs π
) β Ring) |
4 | | zsssubrg 20871 |
. . . . . . . . . 10
β’ (π
β
(SubRingββfld) β β€ β π
) |
5 | 4 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β β€ β π
) |
6 | | eqid 2737 |
. . . . . . . . . . 11
β’
(βfld βΎs π
) = (βfld
βΎs π
) |
7 | 6 | subrgbas 20247 |
. . . . . . . . . 10
β’ (π
β
(SubRingββfld) β π
= (Baseβ(βfld
βΎs π
))) |
8 | 7 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β π
=
(Baseβ(βfld βΎs π
))) |
9 | 5, 8 | sseqtrd 3989 |
. . . . . . . 8
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β β€ β (Baseβ(βfld
βΎs π
))) |
10 | | simprl 770 |
. . . . . . . 8
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β π₯
β β€) |
11 | 9, 10 | sseldd 3950 |
. . . . . . 7
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β π₯
β (Baseβ(βfld βΎs π
))) |
12 | | nnz 12527 |
. . . . . . . . . 10
β’ (π¦ β β β π¦ β
β€) |
13 | 12 | ad2antll 728 |
. . . . . . . . 9
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β π¦
β β€) |
14 | 9, 13 | sseldd 3950 |
. . . . . . . 8
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β π¦
β (Baseβ(βfld βΎs π
))) |
15 | | nnne0 12194 |
. . . . . . . . . 10
β’ (π¦ β β β π¦ β 0) |
16 | 15 | ad2antll 728 |
. . . . . . . . 9
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β π¦
β 0) |
17 | | cnfld0 20837 |
. . . . . . . . . . 11
β’ 0 =
(0gββfld) |
18 | 6, 17 | subrg0 20245 |
. . . . . . . . . 10
β’ (π
β
(SubRingββfld) β 0 =
(0gβ(βfld βΎs π
))) |
19 | 18 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β 0 = (0gβ(βfld
βΎs π
))) |
20 | 16, 19 | neeqtrd 3014 |
. . . . . . . 8
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β π¦
β (0gβ(βfld βΎs π
))) |
21 | | eqid 2737 |
. . . . . . . . . 10
β’
(Baseβ(βfld βΎs π
)) = (Baseβ(βfld
βΎs π
)) |
22 | | eqid 2737 |
. . . . . . . . . 10
β’
(Unitβ(βfld βΎs π
)) = (Unitβ(βfld
βΎs π
)) |
23 | | eqid 2737 |
. . . . . . . . . 10
β’
(0gβ(βfld βΎs π
)) =
(0gβ(βfld βΎs π
)) |
24 | 21, 22, 23 | drngunit 20204 |
. . . . . . . . 9
β’
((βfld βΎs π
) β DivRing β (π¦ β (Unitβ(βfld
βΎs π
))
β (π¦ β
(Baseβ(βfld βΎs π
)) β§ π¦ β
(0gβ(βfld βΎs π
))))) |
25 | 24 | ad2antlr 726 |
. . . . . . . 8
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β (π¦
β (Unitβ(βfld βΎs π
)) β (π¦ β (Baseβ(βfld
βΎs π
))
β§ π¦ β
(0gβ(βfld βΎs π
))))) |
26 | 14, 20, 25 | mpbir2and 712 |
. . . . . . 7
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β π¦
β (Unitβ(βfld βΎs π
))) |
27 | | eqid 2737 |
. . . . . . . 8
β’
(/rβ(βfld βΎs π
)) =
(/rβ(βfld βΎs π
)) |
28 | 21, 22, 27 | dvrcl 20122 |
. . . . . . 7
β’
(((βfld βΎs π
) β Ring β§ π₯ β (Baseβ(βfld
βΎs π
))
β§ π¦ β
(Unitβ(βfld βΎs π
))) β (π₯(/rβ(βfld
βΎs π
))π¦) β (Baseβ(βfld
βΎs π
))) |
29 | 3, 11, 26, 28 | syl3anc 1372 |
. . . . . 6
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β (π₯(/rβ(βfld
βΎs π
))π¦) β (Baseβ(βfld
βΎs π
))) |
30 | | simpll 766 |
. . . . . . 7
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β π
β (SubRingββfld)) |
31 | 5, 10 | sseldd 3950 |
. . . . . . 7
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β π₯
β π
) |
32 | | cnflddiv 20843 |
. . . . . . . 8
β’ / =
(/rββfld) |
33 | 6, 32, 22, 27 | subrgdv 20255 |
. . . . . . 7
β’ ((π
β
(SubRingββfld) β§ π₯ β π
β§ π¦ β (Unitβ(βfld
βΎs π
)))
β (π₯ / π¦) = (π₯(/rβ(βfld
βΎs π
))π¦)) |
34 | 30, 31, 26, 33 | syl3anc 1372 |
. . . . . 6
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β (π₯
/ π¦) = (π₯(/rβ(βfld
βΎs π
))π¦)) |
35 | 29, 34, 8 | 3eltr4d 2853 |
. . . . 5
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β (π₯
/ π¦) β π
) |
36 | | eleq1 2826 |
. . . . 5
β’ (π§ = (π₯ / π¦) β (π§ β π
β (π₯ / π¦) β π
)) |
37 | 35, 36 | syl5ibrcom 247 |
. . . 4
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β (π§
= (π₯ / π¦) β π§ β π
)) |
38 | 37 | rexlimdvva 3206 |
. . 3
β’ ((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β (βπ₯ β β€ βπ¦ β β π§ = (π₯ / π¦) β π§ β π
)) |
39 | 1, 38 | biimtrid 241 |
. 2
β’ ((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β (π§
β β β π§
β π
)) |
40 | 39 | ssrdv 3955 |
1
β’ ((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β β β π
) |