| Step | Hyp | Ref
| Expression |
|---|
| 1 | | qqhval2.0 |
. . 3
β’ π΅ = (Baseβπ
) |
| 2 | | qqhval2.1 |
. . 3
β’ / =
(/rβπ
) |
| 3 | | qqhval2.2 |
. . 3
β’ πΏ = (β€RHomβπ
) |
| 4 | 1, 2, 3 | qqhval2 33031 |
. 2
β’ ((π
β DivRing β§
(chrβπ
) = 0) β
(βHomβπ
) =
(π β β β¦
((πΏβ(numerβπ)) / (πΏβ(denomβπ))))) |
| 5 | | drngring 20368 |
. . . . 5
β’ (π
β DivRing β π
β Ring) |
| 6 | 5 | adantr 481 |
. . . 4
β’ ((π
β DivRing β§
(chrβπ
) = 0) β
π
β
Ring) |
| 7 | 6 | adantr 481 |
. . 3
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
π β β) β
π
β
Ring) |
| 8 | 3 | zrhrhm 21067 |
. . . . 5
β’ (π
β Ring β πΏ β (β€ring
RingHom π
)) |
| 9 | | zringbas 21029 |
. . . . . 6
β’ β€ =
(Baseββ€ring) |
| 10 | 9, 1 | rhmf 20267 |
. . . . 5
β’ (πΏ β (β€ring
RingHom π
) β πΏ:β€βΆπ΅) |
| 11 | 7, 8, 10 | 3syl 18 |
. . . 4
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
π β β) β
πΏ:β€βΆπ΅) |
| 12 | | qnumcl 16678 |
. . . . 5
β’ (π β β β
(numerβπ) β
β€) |
| 13 | 12 | adantl 482 |
. . . 4
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
π β β) β
(numerβπ) β
β€) |
| 14 | 11, 13 | ffvelcdmd 7087 |
. . 3
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
π β β) β
(πΏβ(numerβπ)) β π΅) |
| 15 | | simpll 765 |
. . . 4
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
π β β) β
π
β
DivRing) |
| 16 | | qdencl 16679 |
. . . . . . 7
β’ (π β β β
(denomβπ) β
β) |
| 17 | 16 | adantl 482 |
. . . . . 6
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
π β β) β
(denomβπ) β
β) |
| 18 | 17 | nnzd 12587 |
. . . . 5
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
π β β) β
(denomβπ) β
β€) |
| 19 | 11, 18 | ffvelcdmd 7087 |
. . . 4
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
π β β) β
(πΏβ(denomβπ)) β π΅) |
| 20 | 17 | nnne0d 12264 |
. . . . . . . . . 10
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
π β β) β
(denomβπ) β
0) |
| 21 | 20 | neneqd 2945 |
. . . . . . . . 9
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
π β β) β
Β¬ (denomβπ) =
0) |
| 22 | | fvex 6904 |
. . . . . . . . . 10
β’
(denomβπ)
β V |
| 23 | 22 | elsn 4643 |
. . . . . . . . 9
β’
((denomβπ)
β {0} β (denomβπ) = 0) |
| 24 | 21, 23 | sylnibr 328 |
. . . . . . . 8
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
π β β) β
Β¬ (denomβπ)
β {0}) |
| 25 | | eqid 2732 |
. . . . . . . . . . . 12
β’
(0gβπ
) = (0gβπ
) |
| 26 | 1, 3, 25 | zrhker 33026 |
. . . . . . . . . . 11
β’ (π
β Ring β
((chrβπ
) = 0 β
(β‘πΏ β {(0gβπ
)}) = {0})) |
| 27 | 26 | biimpa 477 |
. . . . . . . . . 10
β’ ((π
β Ring β§
(chrβπ
) = 0) β
(β‘πΏ β {(0gβπ
)}) = {0}) |
| 28 | 5, 27 | sylan 580 |
. . . . . . . . 9
β’ ((π
β DivRing β§
(chrβπ
) = 0) β
(β‘πΏ β {(0gβπ
)}) = {0}) |
| 29 | 28 | adantr 481 |
. . . . . . . 8
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
π β β) β
(β‘πΏ β {(0gβπ
)}) = {0}) |
| 30 | 24, 29 | neleqtrrd 2856 |
. . . . . . 7
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
π β β) β
Β¬ (denomβπ)
β (β‘πΏ β {(0gβπ
)})) |
| 31 | | ffn 6717 |
. . . . . . . . . . . 12
β’ (πΏ:β€βΆπ΅ β πΏ Fn β€) |
| 32 | 8, 10, 31 | 3syl 18 |
. . . . . . . . . . 11
β’ (π
β Ring β πΏ Fn β€) |
| 33 | | elpreima 7059 |
. . . . . . . . . . 11
β’ (πΏ Fn β€ β
((denomβπ) β
(β‘πΏ β {(0gβπ
)}) β ((denomβπ) β β€ β§ (πΏβ(denomβπ)) β
{(0gβπ
)}))) |
| 34 | 5, 32, 33 | 3syl 18 |
. . . . . . . . . 10
β’ (π
β DivRing β
((denomβπ) β
(β‘πΏ β {(0gβπ
)}) β ((denomβπ) β β€ β§ (πΏβ(denomβπ)) β
{(0gβπ
)}))) |
| 35 | 34 | biimpar 478 |
. . . . . . . . 9
β’ ((π
β DivRing β§
((denomβπ) β
β€ β§ (πΏβ(denomβπ)) β {(0gβπ
)})) β (denomβπ) β (β‘πΏ β {(0gβπ
)})) |
| 36 | 35 | expr 457 |
. . . . . . . 8
β’ ((π
β DivRing β§
(denomβπ) β
β€) β ((πΏβ(denomβπ)) β {(0gβπ
)} β (denomβπ) β (β‘πΏ β {(0gβπ
)}))) |
| 37 | 36 | con3dimp 409 |
. . . . . . 7
β’ (((π
β DivRing β§
(denomβπ) β
β€) β§ Β¬ (denomβπ) β (β‘πΏ β {(0gβπ
)})) β Β¬ (πΏβ(denomβπ)) β
{(0gβπ
)}) |
| 38 | 15, 18, 30, 37 | syl21anc 836 |
. . . . . 6
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
π β β) β
Β¬ (πΏβ(denomβπ)) β {(0gβπ
)}) |
| 39 | | fvex 6904 |
. . . . . . 7
β’ (πΏβ(denomβπ)) β V |
| 40 | 39 | elsn 4643 |
. . . . . 6
β’ ((πΏβ(denomβπ)) β
{(0gβπ
)}
β (πΏβ(denomβπ)) = (0gβπ
)) |
| 41 | 38, 40 | sylnib 327 |
. . . . 5
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
π β β) β
Β¬ (πΏβ(denomβπ)) = (0gβπ
)) |
| 42 | 41 | neqned 2947 |
. . . 4
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
π β β) β
(πΏβ(denomβπ)) β
(0gβπ
)) |
| 43 | | eqid 2732 |
. . . . . 6
β’
(Unitβπ
) =
(Unitβπ
) |
| 44 | 1, 43, 25 | drngunit 20366 |
. . . . 5
β’ (π
β DivRing β ((πΏβ(denomβπ)) β (Unitβπ
) β ((πΏβ(denomβπ)) β π΅ β§ (πΏβ(denomβπ)) β (0gβπ
)))) |
| 45 | 44 | biimpar 478 |
. . . 4
β’ ((π
β DivRing β§ ((πΏβ(denomβπ)) β π΅ β§ (πΏβ(denomβπ)) β (0gβπ
))) β (πΏβ(denomβπ)) β (Unitβπ
)) |
| 46 | 15, 19, 42, 45 | syl12anc 835 |
. . 3
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
π β β) β
(πΏβ(denomβπ)) β (Unitβπ
)) |
| 47 | 1, 43, 2 | dvrcl 20222 |
. . 3
β’ ((π
β Ring β§ (πΏβ(numerβπ)) β π΅ β§ (πΏβ(denomβπ)) β (Unitβπ
)) β ((πΏβ(numerβπ)) / (πΏβ(denomβπ))) β π΅) |
| 48 | 7, 14, 46, 47 | syl3anc 1371 |
. 2
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
π β β) β
((πΏβ(numerβπ)) / (πΏβ(denomβπ))) β π΅) |
| 49 | 4, 48 | fmpt3d 7117 |
1
β’ ((π
β DivRing β§
(chrβπ
) = 0) β
(βHomβπ
):ββΆπ΅) |
