Step | Hyp | Ref
| Expression |
1 | | elex 3462 |
. . . 4
β’ (π
β DivRing β π
β V) |
2 | 1 | adantr 482 |
. . 3
β’ ((π
β DivRing β§
(chrβπ
) = 0) β
π
β
V) |
3 | | qqhval2.1 |
. . . 4
β’ / =
(/rβπ
) |
4 | | eqid 2733 |
. . . 4
β’
(1rβπ
) = (1rβπ
) |
5 | | qqhval2.2 |
. . . 4
β’ πΏ = (β€RHomβπ
) |
6 | 3, 4, 5 | qqhval 32612 |
. . 3
β’ (π
β V β
(βHomβπ
) = ran
(π₯ β β€, π¦ β (β‘πΏ β (Unitβπ
)) β¦ β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©)) |
7 | 2, 6 | syl 17 |
. 2
β’ ((π
β DivRing β§
(chrβπ
) = 0) β
(βHomβπ
) = ran
(π₯ β β€, π¦ β (β‘πΏ β (Unitβπ
)) β¦ β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©)) |
8 | | eqid 2733 |
. . . 4
β’ β€ =
β€ |
9 | | qqhval2.0 |
. . . . 5
β’ π΅ = (Baseβπ
) |
10 | | eqid 2733 |
. . . . 5
β’
(0gβπ
) = (0gβπ
) |
11 | 9, 5, 10 | zrhunitpreima 32616 |
. . . 4
β’ ((π
β DivRing β§
(chrβπ
) = 0) β
(β‘πΏ β (Unitβπ
)) = (β€ β {0})) |
12 | | mpoeq12 7431 |
. . . 4
β’ ((β€
= β€ β§ (β‘πΏ β (Unitβπ
)) = (β€ β {0})) β (π₯ β β€, π¦ β (β‘πΏ β (Unitβπ
)) β¦ β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) = (π₯ β β€, π¦ β (β€ β {0}) β¦
β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©)) |
13 | 8, 11, 12 | sylancr 588 |
. . 3
β’ ((π
β DivRing β§
(chrβπ
) = 0) β
(π₯ β β€, π¦ β (β‘πΏ β (Unitβπ
)) β¦ β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) = (π₯ β β€, π¦ β (β€ β {0}) β¦
β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©)) |
14 | 13 | rneqd 5894 |
. 2
β’ ((π
β DivRing β§
(chrβπ
) = 0) β
ran (π₯ β β€,
π¦ β (β‘πΏ β (Unitβπ
)) β¦ β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) = ran (π₯ β β€, π¦ β (β€ β {0}) β¦
β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©)) |
15 | | nfv 1918 |
. . . 4
β’
β²π(π
β DivRing β§
(chrβπ
) =
0) |
16 | | nfab1 2906 |
. . . 4
β’
β²π{π β£ βπ₯ β β€ βπ¦ β (β€ β {0})π = β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©} |
17 | | nfcv 2904 |
. . . 4
β’
β²π{β¨π, π β© β£ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ))))} |
18 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π₯ β β€ β§
π¦ β (β€ β
{0}))) β§ π =
β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) β π = β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) |
19 | | zssq 12886 |
. . . . . . . . . . . 12
β’ β€
β β |
20 | | simplrl 776 |
. . . . . . . . . . . 12
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π₯ β β€ β§
π¦ β (β€ β
{0}))) β§ π =
β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) β π₯ β β€) |
21 | 19, 20 | sselid 3943 |
. . . . . . . . . . 11
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π₯ β β€ β§
π¦ β (β€ β
{0}))) β§ π =
β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) β π₯ β β) |
22 | | simplrr 777 |
. . . . . . . . . . . . 13
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π₯ β β€ β§
π¦ β (β€ β
{0}))) β§ π =
β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) β π¦ β (β€ β
{0})) |
23 | 22 | eldifad 3923 |
. . . . . . . . . . . 12
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π₯ β β€ β§
π¦ β (β€ β
{0}))) β§ π =
β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) β π¦ β β€) |
24 | 19, 23 | sselid 3943 |
. . . . . . . . . . 11
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π₯ β β€ β§
π¦ β (β€ β
{0}))) β§ π =
β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) β π¦ β β) |
25 | 22 | eldifbd 3924 |
. . . . . . . . . . . 12
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π₯ β β€ β§
π¦ β (β€ β
{0}))) β§ π =
β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) β Β¬ π¦ β {0}) |
26 | | velsn 4603 |
. . . . . . . . . . . . 13
β’ (π¦ β {0} β π¦ = 0) |
27 | 26 | necon3bbii 2988 |
. . . . . . . . . . . 12
β’ (Β¬
π¦ β {0} β π¦ β 0) |
28 | 25, 27 | sylib 217 |
. . . . . . . . . . 11
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π₯ β β€ β§
π¦ β (β€ β
{0}))) β§ π =
β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) β π¦ β 0) |
29 | | qdivcl 12900 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ π¦ β β β§ π¦ β 0) β (π₯ / π¦) β β) |
30 | 21, 24, 28, 29 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π₯ β β€ β§
π¦ β (β€ β
{0}))) β§ π =
β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) β (π₯ / π¦) β β) |
31 | | simplll 774 |
. . . . . . . . . . 11
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π₯ β β€ β§
π¦ β (β€ β
{0}))) β§ π =
β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) β π
β DivRing) |
32 | | simpllr 775 |
. . . . . . . . . . 11
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π₯ β β€ β§
π¦ β (β€ β
{0}))) β§ π =
β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) β (chrβπ
) = 0) |
33 | 9, 3, 5 | qqhval2lem 32619 |
. . . . . . . . . . . 12
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π₯ β β€ β§
π¦ β β€ β§
π¦ β 0)) β ((πΏβ(numerβ(π₯ / π¦))) / (πΏβ(denomβ(π₯ / π¦)))) = ((πΏβπ₯) / (πΏβπ¦))) |
34 | 33 | eqcomd 2739 |
. . . . . . . . . . 11
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π₯ β β€ β§
π¦ β β€ β§
π¦ β 0)) β ((πΏβπ₯) / (πΏβπ¦)) = ((πΏβ(numerβ(π₯ / π¦))) / (πΏβ(denomβ(π₯ / π¦))))) |
35 | 31, 32, 20, 23, 28, 34 | syl23anc 1378 |
. . . . . . . . . 10
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π₯ β β€ β§
π¦ β (β€ β
{0}))) β§ π =
β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) β ((πΏβπ₯) / (πΏβπ¦)) = ((πΏβ(numerβ(π₯ / π¦))) / (πΏβ(denomβ(π₯ / π¦))))) |
36 | | ovex 7391 |
. . . . . . . . . . 11
β’ (π₯ / π¦) β V |
37 | | ovex 7391 |
. . . . . . . . . . 11
β’ ((πΏβπ₯) / (πΏβπ¦)) β V |
38 | | opeq12 4833 |
. . . . . . . . . . . . 13
β’ ((π = (π₯ / π¦) β§ π = ((πΏβπ₯) / (πΏβπ¦))) β β¨π, π β© = β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) |
39 | 38 | eqeq2d 2744 |
. . . . . . . . . . . 12
β’ ((π = (π₯ / π¦) β§ π = ((πΏβπ₯) / (πΏβπ¦))) β (π = β¨π, π β© β π = β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©)) |
40 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ ((π = (π₯ / π¦) β§ π = ((πΏβπ₯) / (πΏβπ¦))) β π = (π₯ / π¦)) |
41 | 40 | eleq1d 2819 |
. . . . . . . . . . . . 13
β’ ((π = (π₯ / π¦) β§ π = ((πΏβπ₯) / (πΏβπ¦))) β (π β β β (π₯ / π¦) β β)) |
42 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π = (π₯ / π¦) β§ π = ((πΏβπ₯) / (πΏβπ¦))) β π = ((πΏβπ₯) / (πΏβπ¦))) |
43 | 40 | fveq2d 6847 |
. . . . . . . . . . . . . . . 16
β’ ((π = (π₯ / π¦) β§ π = ((πΏβπ₯) / (πΏβπ¦))) β (numerβπ) = (numerβ(π₯ / π¦))) |
44 | 43 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
β’ ((π = (π₯ / π¦) β§ π = ((πΏβπ₯) / (πΏβπ¦))) β (πΏβ(numerβπ)) = (πΏβ(numerβ(π₯ / π¦)))) |
45 | 40 | fveq2d 6847 |
. . . . . . . . . . . . . . . 16
β’ ((π = (π₯ / π¦) β§ π = ((πΏβπ₯) / (πΏβπ¦))) β (denomβπ) = (denomβ(π₯ / π¦))) |
46 | 45 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
β’ ((π = (π₯ / π¦) β§ π = ((πΏβπ₯) / (πΏβπ¦))) β (πΏβ(denomβπ)) = (πΏβ(denomβ(π₯ / π¦)))) |
47 | 44, 46 | oveq12d 7376 |
. . . . . . . . . . . . . 14
β’ ((π = (π₯ / π¦) β§ π = ((πΏβπ₯) / (πΏβπ¦))) β ((πΏβ(numerβπ)) / (πΏβ(denomβπ))) = ((πΏβ(numerβ(π₯ / π¦))) / (πΏβ(denomβ(π₯ / π¦))))) |
48 | 42, 47 | eqeq12d 2749 |
. . . . . . . . . . . . 13
β’ ((π = (π₯ / π¦) β§ π = ((πΏβπ₯) / (πΏβπ¦))) β (π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ))) β ((πΏβπ₯) / (πΏβπ¦)) = ((πΏβ(numerβ(π₯ / π¦))) / (πΏβ(denomβ(π₯ / π¦)))))) |
49 | 41, 48 | anbi12d 632 |
. . . . . . . . . . . 12
β’ ((π = (π₯ / π¦) β§ π = ((πΏβπ₯) / (πΏβπ¦))) β ((π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))) β ((π₯ / π¦) β β β§ ((πΏβπ₯) / (πΏβπ¦)) = ((πΏβ(numerβ(π₯ / π¦))) / (πΏβ(denomβ(π₯ / π¦))))))) |
50 | 39, 49 | anbi12d 632 |
. . . . . . . . . . 11
β’ ((π = (π₯ / π¦) β§ π = ((πΏβπ₯) / (πΏβπ¦))) β ((π = β¨π, π β© β§ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ))))) β (π = β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β© β§ ((π₯ / π¦) β β β§ ((πΏβπ₯) / (πΏβπ¦)) = ((πΏβ(numerβ(π₯ / π¦))) / (πΏβ(denomβ(π₯ / π¦)))))))) |
51 | 36, 37, 50 | spc2ev 3565 |
. . . . . . . . . 10
β’ ((π = β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β© β§ ((π₯ / π¦) β β β§ ((πΏβπ₯) / (πΏβπ¦)) = ((πΏβ(numerβ(π₯ / π¦))) / (πΏβ(denomβ(π₯ / π¦)))))) β βπβπ (π = β¨π, π β© β§ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))))) |
52 | 18, 30, 35, 51 | syl12anc 836 |
. . . . . . . . 9
β’ ((((π
β DivRing β§
(chrβπ
) = 0) β§
(π₯ β β€ β§
π¦ β (β€ β
{0}))) β§ π =
β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) β βπβπ (π = β¨π, π β© β§ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))))) |
53 | 52 | ex 414 |
. . . . . . . 8
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π₯ β β€ β§
π¦ β (β€ β
{0}))) β (π =
β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β© β βπβπ (π = β¨π, π β© β§ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ))))))) |
54 | 53 | rexlimdvva 3202 |
. . . . . . 7
β’ ((π
β DivRing β§
(chrβπ
) = 0) β
(βπ₯ β β€
βπ¦ β (β€
β {0})π =
β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β© β βπβπ (π = β¨π, π β© β§ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ))))))) |
55 | 54 | imp 408 |
. . . . . 6
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
βπ₯ β β€
βπ¦ β (β€
β {0})π =
β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) β βπβπ (π = β¨π, π β© β§ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))))) |
56 | | 19.42vv 1962 |
. . . . . . 7
β’
(βπβπ ((π
β DivRing β§ (chrβπ
) = 0) β§ (π = β¨π, π β© β§ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))))) β ((π
β DivRing β§ (chrβπ
) = 0) β§ βπβπ (π = β¨π, π β© β§ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ))))))) |
57 | | simprrl 780 |
. . . . . . . . . 10
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π = β¨π, π β© β§ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))))) β π β β) |
58 | | qnumcl 16620 |
. . . . . . . . . 10
β’ (π β β β
(numerβπ) β
β€) |
59 | 57, 58 | syl 17 |
. . . . . . . . 9
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π = β¨π, π β© β§ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))))) β (numerβπ) β β€) |
60 | | qdencl 16621 |
. . . . . . . . . . . 12
β’ (π β β β
(denomβπ) β
β) |
61 | 57, 60 | syl 17 |
. . . . . . . . . . 11
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π = β¨π, π β© β§ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))))) β (denomβπ) β β) |
62 | 61 | nnzd 12531 |
. . . . . . . . . 10
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π = β¨π, π β© β§ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))))) β (denomβπ) β β€) |
63 | | nnne0 12192 |
. . . . . . . . . . 11
β’
((denomβπ)
β β β (denomβπ) β 0) |
64 | | nelsn 4627 |
. . . . . . . . . . 11
β’
((denomβπ)
β 0 β Β¬ (denomβπ) β {0}) |
65 | 61, 63, 64 | 3syl 18 |
. . . . . . . . . 10
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π = β¨π, π β© β§ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))))) β Β¬ (denomβπ) β {0}) |
66 | 62, 65 | eldifd 3922 |
. . . . . . . . 9
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π = β¨π, π β© β§ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))))) β (denomβπ) β (β€ β
{0})) |
67 | | simprl 770 |
. . . . . . . . . 10
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π = β¨π, π β© β§ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))))) β π = β¨π, π β©) |
68 | | qeqnumdivden 16626 |
. . . . . . . . . . . 12
β’ (π β β β π = ((numerβπ) / (denomβπ))) |
69 | 57, 68 | syl 17 |
. . . . . . . . . . 11
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π = β¨π, π β© β§ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))))) β π = ((numerβπ) / (denomβπ))) |
70 | | simprrr 781 |
. . . . . . . . . . 11
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π = β¨π, π β© β§ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))))) β π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))) |
71 | 69, 70 | opeq12d 4839 |
. . . . . . . . . 10
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π = β¨π, π β© β§ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))))) β β¨π, π β© = β¨((numerβπ) / (denomβπ)), ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))β©) |
72 | 67, 71 | eqtrd 2773 |
. . . . . . . . 9
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π = β¨π, π β© β§ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))))) β π = β¨((numerβπ) / (denomβπ)), ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))β©) |
73 | | oveq1 7365 |
. . . . . . . . . . . 12
β’ (π₯ = (numerβπ) β (π₯ / π¦) = ((numerβπ) / π¦)) |
74 | | fveq2 6843 |
. . . . . . . . . . . . 13
β’ (π₯ = (numerβπ) β (πΏβπ₯) = (πΏβ(numerβπ))) |
75 | 74 | oveq1d 7373 |
. . . . . . . . . . . 12
β’ (π₯ = (numerβπ) β ((πΏβπ₯) / (πΏβπ¦)) = ((πΏβ(numerβπ)) / (πΏβπ¦))) |
76 | 73, 75 | opeq12d 4839 |
. . . . . . . . . . 11
β’ (π₯ = (numerβπ) β β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β© = β¨((numerβπ) / π¦), ((πΏβ(numerβπ)) / (πΏβπ¦))β©) |
77 | 76 | eqeq2d 2744 |
. . . . . . . . . 10
β’ (π₯ = (numerβπ) β (π = β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β© β π = β¨((numerβπ) / π¦), ((πΏβ(numerβπ)) / (πΏβπ¦))β©)) |
78 | | oveq2 7366 |
. . . . . . . . . . . 12
β’ (π¦ = (denomβπ) β ((numerβπ) / π¦) = ((numerβπ) / (denomβπ))) |
79 | | fveq2 6843 |
. . . . . . . . . . . . 13
β’ (π¦ = (denomβπ) β (πΏβπ¦) = (πΏβ(denomβπ))) |
80 | 79 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (π¦ = (denomβπ) β ((πΏβ(numerβπ)) / (πΏβπ¦)) = ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))) |
81 | 78, 80 | opeq12d 4839 |
. . . . . . . . . . 11
β’ (π¦ = (denomβπ) β
β¨((numerβπ) /
π¦), ((πΏβ(numerβπ)) / (πΏβπ¦))β© = β¨((numerβπ) / (denomβπ)), ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))β©) |
82 | 81 | eqeq2d 2744 |
. . . . . . . . . 10
β’ (π¦ = (denomβπ) β (π = β¨((numerβπ) / π¦), ((πΏβ(numerβπ)) / (πΏβπ¦))β© β π = β¨((numerβπ) / (denomβπ)), ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))β©)) |
83 | 77, 82 | rspc2ev 3591 |
. . . . . . . . 9
β’
(((numerβπ)
β β€ β§ (denomβπ) β (β€ β {0}) β§ π = β¨((numerβπ) / (denomβπ)), ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))β©) β βπ₯ β β€ βπ¦ β (β€ β {0})π = β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) |
84 | 59, 66, 72, 83 | syl3anc 1372 |
. . . . . . . 8
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
(π = β¨π, π β© β§ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))))) β βπ₯ β β€ βπ¦ β (β€ β {0})π = β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) |
85 | 84 | exlimivv 1936 |
. . . . . . 7
β’
(βπβπ ((π
β DivRing β§ (chrβπ
) = 0) β§ (π = β¨π, π β© β§ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))))) β βπ₯ β β€ βπ¦ β (β€ β {0})π = β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) |
86 | 56, 85 | sylbir 234 |
. . . . . 6
β’ (((π
β DivRing β§
(chrβπ
) = 0) β§
βπβπ (π = β¨π, π β© β§ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))))) β βπ₯ β β€ βπ¦ β (β€ β {0})π = β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) |
87 | 55, 86 | impbida 800 |
. . . . 5
β’ ((π
β DivRing β§
(chrβπ
) = 0) β
(βπ₯ β β€
βπ¦ β (β€
β {0})π =
β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β© β βπβπ (π = β¨π, π β© β§ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ))))))) |
88 | | abid 2714 |
. . . . 5
β’ (π β {π β£ βπ₯ β β€ βπ¦ β (β€ β {0})π = β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©} β βπ₯ β β€ βπ¦ β (β€ β {0})π = β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) |
89 | | elopab 5485 |
. . . . 5
β’ (π β {β¨π, π β© β£ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ))))} β βπβπ (π = β¨π, π β© β§ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))))) |
90 | 87, 88, 89 | 3bitr4g 314 |
. . . 4
β’ ((π
β DivRing β§
(chrβπ
) = 0) β
(π β {π β£ βπ₯ β β€ βπ¦ β (β€ β
{0})π = β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©} β π β {β¨π, π β© β£ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ))))})) |
91 | 15, 16, 17, 90 | eqrd 3964 |
. . 3
β’ ((π
β DivRing β§
(chrβπ
) = 0) β
{π β£ βπ₯ β β€ βπ¦ β (β€ β
{0})π = β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©} = {β¨π, π β© β£ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ))))}) |
92 | | eqid 2733 |
. . . 4
β’ (π₯ β β€, π¦ β (β€ β {0})
β¦ β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) = (π₯ β β€, π¦ β (β€ β {0}) β¦
β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) |
93 | 92 | rnmpo 7490 |
. . 3
β’ ran
(π₯ β β€, π¦ β (β€ β {0})
β¦ β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) = {π β£ βπ₯ β β€ βπ¦ β (β€ β {0})π = β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©} |
94 | | df-mpt 5190 |
. . 3
β’ (π β β β¦ ((πΏβ(numerβπ)) / (πΏβ(denomβπ)))) = {β¨π, π β© β£ (π β β β§ π = ((πΏβ(numerβπ)) / (πΏβ(denomβπ))))} |
95 | 91, 93, 94 | 3eqtr4g 2798 |
. 2
β’ ((π
β DivRing β§
(chrβπ
) = 0) β
ran (π₯ β β€,
π¦ β (β€ β
{0}) β¦ β¨(π₯ /
π¦), ((πΏβπ₯) / (πΏβπ¦))β©) = (π β β β¦ ((πΏβ(numerβπ)) / (πΏβ(denomβπ))))) |
96 | 7, 14, 95 | 3eqtrd 2777 |
1
β’ ((π
β DivRing β§
(chrβπ
) = 0) β
(βHomβπ
) =
(π β β β¦
((πΏβ(numerβπ)) / (πΏβ(denomβπ))))) |