Step | Hyp | Ref
| Expression |
1 | | elq 12933 |
. . 3
β’ (π§ β β β
βπ₯ β β€
βπ¦ β β
π§ = (π₯ / π¦)) |
2 | | drngring 20363 |
. . . . . . . 8
β’
((βfld βΎs π
) β DivRing β
(βfld βΎs π
) β Ring) |
3 | 2 | ad2antlr 725 |
. . . . . . 7
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β (βfld βΎs π
) β Ring) |
4 | | zsssubrg 21002 |
. . . . . . . . . 10
β’ (π
β
(SubRingββfld) β β€ β π
) |
5 | 4 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β β€ β π
) |
6 | | eqid 2732 |
. . . . . . . . . . 11
β’
(βfld βΎs π
) = (βfld
βΎs π
) |
7 | 6 | subrgbas 20327 |
. . . . . . . . . 10
β’ (π
β
(SubRingββfld) β π
= (Baseβ(βfld
βΎs π
))) |
8 | 7 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β π
=
(Baseβ(βfld βΎs π
))) |
9 | 5, 8 | sseqtrd 4022 |
. . . . . . . 8
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β β€ β (Baseβ(βfld
βΎs π
))) |
10 | | simprl 769 |
. . . . . . . 8
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β π₯
β β€) |
11 | 9, 10 | sseldd 3983 |
. . . . . . 7
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β π₯
β (Baseβ(βfld βΎs π
))) |
12 | | nnz 12578 |
. . . . . . . . . 10
β’ (π¦ β β β π¦ β
β€) |
13 | 12 | ad2antll 727 |
. . . . . . . . 9
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β π¦
β β€) |
14 | 9, 13 | sseldd 3983 |
. . . . . . . 8
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β π¦
β (Baseβ(βfld βΎs π
))) |
15 | | nnne0 12245 |
. . . . . . . . . 10
β’ (π¦ β β β π¦ β 0) |
16 | 15 | ad2antll 727 |
. . . . . . . . 9
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β π¦
β 0) |
17 | | cnfld0 20968 |
. . . . . . . . . . 11
β’ 0 =
(0gββfld) |
18 | 6, 17 | subrg0 20325 |
. . . . . . . . . 10
β’ (π
β
(SubRingββfld) β 0 =
(0gβ(βfld βΎs π
))) |
19 | 18 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β 0 = (0gβ(βfld
βΎs π
))) |
20 | 16, 19 | neeqtrd 3010 |
. . . . . . . 8
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β π¦
β (0gβ(βfld βΎs π
))) |
21 | | eqid 2732 |
. . . . . . . . . 10
β’
(Baseβ(βfld βΎs π
)) = (Baseβ(βfld
βΎs π
)) |
22 | | eqid 2732 |
. . . . . . . . . 10
β’
(Unitβ(βfld βΎs π
)) = (Unitβ(βfld
βΎs π
)) |
23 | | eqid 2732 |
. . . . . . . . . 10
β’
(0gβ(βfld βΎs π
)) =
(0gβ(βfld βΎs π
)) |
24 | 21, 22, 23 | drngunit 20361 |
. . . . . . . . 9
β’
((βfld βΎs π
) β DivRing β (π¦ β (Unitβ(βfld
βΎs π
))
β (π¦ β
(Baseβ(βfld βΎs π
)) β§ π¦ β
(0gβ(βfld βΎs π
))))) |
25 | 24 | ad2antlr 725 |
. . . . . . . 8
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β (π¦
β (Unitβ(βfld βΎs π
)) β (π¦ β (Baseβ(βfld
βΎs π
))
β§ π¦ β
(0gβ(βfld βΎs π
))))) |
26 | 14, 20, 25 | mpbir2and 711 |
. . . . . . 7
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β π¦
β (Unitβ(βfld βΎs π
))) |
27 | | eqid 2732 |
. . . . . . . 8
β’
(/rβ(βfld βΎs π
)) =
(/rβ(βfld βΎs π
)) |
28 | 21, 22, 27 | dvrcl 20217 |
. . . . . . 7
β’
(((βfld βΎs π
) β Ring β§ π₯ β (Baseβ(βfld
βΎs π
))
β§ π¦ β
(Unitβ(βfld βΎs π
))) β (π₯(/rβ(βfld
βΎs π
))π¦) β (Baseβ(βfld
βΎs π
))) |
29 | 3, 11, 26, 28 | syl3anc 1371 |
. . . . . 6
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β (π₯(/rβ(βfld
βΎs π
))π¦) β (Baseβ(βfld
βΎs π
))) |
30 | | simpll 765 |
. . . . . . 7
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β π
β (SubRingββfld)) |
31 | 5, 10 | sseldd 3983 |
. . . . . . 7
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β π₯
β π
) |
32 | | cnflddiv 20974 |
. . . . . . . 8
β’ / =
(/rββfld) |
33 | 6, 32, 22, 27 | subrgdv 20335 |
. . . . . . 7
β’ ((π
β
(SubRingββfld) β§ π₯ β π
β§ π¦ β (Unitβ(βfld
βΎs π
)))
β (π₯ / π¦) = (π₯(/rβ(βfld
βΎs π
))π¦)) |
34 | 30, 31, 26, 33 | syl3anc 1371 |
. . . . . 6
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β (π₯
/ π¦) = (π₯(/rβ(βfld
βΎs π
))π¦)) |
35 | 29, 34, 8 | 3eltr4d 2848 |
. . . . 5
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β (π₯
/ π¦) β π
) |
36 | | eleq1 2821 |
. . . . 5
β’ (π§ = (π₯ / π¦) β (π§ β π
β (π₯ / π¦) β π
)) |
37 | 35, 36 | syl5ibrcom 246 |
. . . 4
β’ (((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β§ (π₯
β β€ β§ π¦
β β)) β (π§
= (π₯ / π¦) β π§ β π
)) |
38 | 37 | rexlimdvva 3211 |
. . 3
β’ ((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β (βπ₯ β β€ βπ¦ β β π§ = (π₯ / π¦) β π§ β π
)) |
39 | 1, 38 | biimtrid 241 |
. 2
β’ ((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β (π§
β β β π§
β π
)) |
40 | 39 | ssrdv 3988 |
1
β’ ((π
β
(SubRingββfld) β§ (βfld
βΎs π
)
β DivRing) β β β π
) |