Step | Hyp | Ref
| Expression |
1 | | isofld 32151 |
. . . 4
β’ (π β oField β (π β Field β§ π β oRing)) |
2 | 1 | simprbi 498 |
. . 3
β’ (π β oField β π β oRing) |
3 | | orngogrp 32150 |
. . 3
β’ (π β oRing β π β oGrp) |
4 | | isarchiofld.b |
. . . 4
β’ π΅ = (Baseβπ) |
5 | | eqid 2733 |
. . . 4
β’
(0gβπ) = (0gβπ) |
6 | | isarchiofld.l |
. . . 4
β’ < =
(ltβπ) |
7 | | eqid 2733 |
. . . 4
β’
(.gβπ) = (.gβπ) |
8 | 4, 5, 6, 7 | isarchi3 32079 |
. . 3
β’ (π β oGrp β (π β Archi β
βπ¦ β π΅ βπ₯ β π΅ ((0gβπ) < π¦ β βπ β β π₯ < (π(.gβπ)π¦)))) |
9 | 2, 3, 8 | 3syl 18 |
. 2
β’ (π β oField β (π β Archi β
βπ¦ β π΅ βπ₯ β π΅ ((0gβπ) < π¦ β βπ β β π₯ < (π(.gβπ)π¦)))) |
10 | | orngring 32149 |
. . . . . . 7
β’ (π β oRing β π β Ring) |
11 | | eqid 2733 |
. . . . . . . 8
β’
(1rβπ) = (1rβπ) |
12 | 4, 11 | ringidcl 19997 |
. . . . . . 7
β’ (π β Ring β
(1rβπ)
β π΅) |
13 | 2, 10, 12 | 3syl 18 |
. . . . . 6
β’ (π β oField β
(1rβπ)
β π΅) |
14 | | breq2 5113 |
. . . . . . . . 9
β’ (π¦ = (1rβπ) β
((0gβπ)
<
π¦ β
(0gβπ)
<
(1rβπ))) |
15 | | oveq2 7369 |
. . . . . . . . . . 11
β’ (π¦ = (1rβπ) β (π(.gβπ)π¦) = (π(.gβπ)(1rβπ))) |
16 | 15 | breq2d 5121 |
. . . . . . . . . 10
β’ (π¦ = (1rβπ) β (π₯ < (π(.gβπ)π¦) β π₯ < (π(.gβπ)(1rβπ)))) |
17 | 16 | rexbidv 3172 |
. . . . . . . . 9
β’ (π¦ = (1rβπ) β (βπ β β π₯ < (π(.gβπ)π¦) β βπ β β π₯ < (π(.gβπ)(1rβπ)))) |
18 | 14, 17 | imbi12d 345 |
. . . . . . . 8
β’ (π¦ = (1rβπ) β
(((0gβπ)
<
π¦ β βπ β β π₯ < (π(.gβπ)π¦)) β ((0gβπ) <
(1rβπ)
β βπ β
β π₯ < (π(.gβπ)(1rβπ))))) |
19 | 18 | ralbidv 3171 |
. . . . . . 7
β’ (π¦ = (1rβπ) β (βπ₯ β π΅ ((0gβπ) < π¦ β βπ β β π₯ < (π(.gβπ)π¦)) β βπ₯ β π΅ ((0gβπ) <
(1rβπ)
β βπ β
β π₯ < (π(.gβπ)(1rβπ))))) |
20 | 19 | rspcv 3579 |
. . . . . 6
β’
((1rβπ) β π΅ β (βπ¦ β π΅ βπ₯ β π΅ ((0gβπ) < π¦ β βπ β β π₯ < (π(.gβπ)π¦)) β βπ₯ β π΅ ((0gβπ) <
(1rβπ)
β βπ β
β π₯ < (π(.gβπ)(1rβπ))))) |
21 | 13, 20 | syl 17 |
. . . . 5
β’ (π β oField β
(βπ¦ β π΅ βπ₯ β π΅ ((0gβπ) < π¦ β βπ β β π₯ < (π(.gβπ)π¦)) β βπ₯ β π΅ ((0gβπ) <
(1rβπ)
β βπ β
β π₯ < (π(.gβπ)(1rβπ))))) |
22 | 5, 11, 6 | ofldlt1 32162 |
. . . . . . 7
β’ (π β oField β
(0gβπ)
<
(1rβπ)) |
23 | | pm5.5 362 |
. . . . . . 7
β’
((0gβπ) <
(1rβπ)
β (((0gβπ) <
(1rβπ)
β βπ β
β π₯ < (π(.gβπ)(1rβπ))) β βπ β β π₯ < (π(.gβπ)(1rβπ)))) |
24 | 22, 23 | syl 17 |
. . . . . 6
β’ (π β oField β
(((0gβπ)
<
(1rβπ)
β βπ β
β π₯ < (π(.gβπ)(1rβπ))) β βπ β β π₯ < (π(.gβπ)(1rβπ)))) |
25 | 24 | ralbidv 3171 |
. . . . 5
β’ (π β oField β
(βπ₯ β π΅ ((0gβπ) <
(1rβπ)
β βπ β
β π₯ < (π(.gβπ)(1rβπ))) β βπ₯ β π΅ βπ β β π₯ < (π(.gβπ)(1rβπ)))) |
26 | 21, 25 | sylibd 238 |
. . . 4
β’ (π β oField β
(βπ¦ β π΅ βπ₯ β π΅ ((0gβπ) < π¦ β βπ β β π₯ < (π(.gβπ)π¦)) β βπ₯ β π΅ βπ β β π₯ < (π(.gβπ)(1rβπ)))) |
27 | 2, 10 | syl 17 |
. . . . . . . 8
β’ (π β oField β π β Ring) |
28 | | nnz 12528 |
. . . . . . . 8
β’ (π β β β π β
β€) |
29 | | isarchiofld.h |
. . . . . . . . 9
β’ π» = (β€RHomβπ) |
30 | 29, 7, 11 | zrhmulg 20933 |
. . . . . . . 8
β’ ((π β Ring β§ π β β€) β (π»βπ) = (π(.gβπ)(1rβπ))) |
31 | 27, 28, 30 | syl2an 597 |
. . . . . . 7
β’ ((π β oField β§ π β β) β (π»βπ) = (π(.gβπ)(1rβπ))) |
32 | 31 | breq2d 5121 |
. . . . . 6
β’ ((π β oField β§ π β β) β (π₯ < (π»βπ) β π₯ < (π(.gβπ)(1rβπ)))) |
33 | 32 | rexbidva 3170 |
. . . . 5
β’ (π β oField β
(βπ β β
π₯ < (π»βπ) β βπ β β π₯ < (π(.gβπ)(1rβπ)))) |
34 | 33 | ralbidv 3171 |
. . . 4
β’ (π β oField β
(βπ₯ β π΅ βπ β β π₯ < (π»βπ) β βπ₯ β π΅ βπ β β π₯ < (π(.gβπ)(1rβπ)))) |
35 | 26, 34 | sylibrd 259 |
. . 3
β’ (π β oField β
(βπ¦ β π΅ βπ₯ β π΅ ((0gβπ) < π¦ β βπ β β π₯ < (π(.gβπ)π¦)) β βπ₯ β π΅ βπ β β π₯ < (π»βπ))) |
36 | | nfv 1918 |
. . . . . . . 8
β’
β²π₯ π β oField |
37 | | nfra1 3266 |
. . . . . . . 8
β’
β²π₯βπ₯ β π΅ βπ β β π₯ < (π»βπ) |
38 | 36, 37 | nfan 1903 |
. . . . . . 7
β’
β²π₯(π β oField β§
βπ₯ β π΅ βπ β β π₯ < (π»βπ)) |
39 | | nfv 1918 |
. . . . . . 7
β’
β²π₯ π¦ β π΅ |
40 | 38, 39 | nfan 1903 |
. . . . . 6
β’
β²π₯((π β oField β§
βπ₯ β π΅ βπ β β π₯ < (π»βπ)) β§ π¦ β π΅) |
41 | 27 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β oField β§
βπ₯ β π΅ βπ β β π₯ < (π»βπ)) β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β π β Ring) |
42 | | simplrr 777 |
. . . . . . . . . . 11
β’ ((((π β oField β§
βπ₯ β π΅ βπ β β π₯ < (π»βπ)) β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β π₯ β π΅) |
43 | | simplrl 776 |
. . . . . . . . . . . 12
β’ ((((π β oField β§
βπ₯ β π΅ βπ β β π₯ < (π»βπ)) β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β π¦ β π΅) |
44 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((((π β oField β§
βπ₯ β π΅ βπ β β π₯ < (π»βπ)) β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β (0gβπ) < π¦) |
45 | | simplll 774 |
. . . . . . . . . . . . . . 15
β’ ((((π β oField β§
βπ₯ β π΅ βπ β β π₯ < (π»βπ)) β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β π β oField) |
46 | | ringgrp 19977 |
. . . . . . . . . . . . . . . 16
β’ (π β Ring β π β Grp) |
47 | 4, 5 | grpidcl 18786 |
. . . . . . . . . . . . . . . 16
β’ (π β Grp β
(0gβπ)
β π΅) |
48 | 41, 46, 47 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ ((((π β oField β§
βπ₯ β π΅ βπ β β π₯ < (π»βπ)) β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β (0gβπ) β π΅) |
49 | 6 | pltne 18231 |
. . . . . . . . . . . . . . 15
β’ ((π β oField β§
(0gβπ)
β π΅ β§ π¦ β π΅) β ((0gβπ) < π¦ β (0gβπ) β π¦)) |
50 | 45, 48, 43, 49 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((((π β oField β§
βπ₯ β π΅ βπ β β π₯ < (π»βπ)) β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β ((0gβπ) < π¦ β (0gβπ) β π¦)) |
51 | 44, 50 | mpd 15 |
. . . . . . . . . . . . 13
β’ ((((π β oField β§
βπ₯ β π΅ βπ β β π₯ < (π»βπ)) β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β (0gβπ) β π¦) |
52 | 51 | necomd 2996 |
. . . . . . . . . . . 12
β’ ((((π β oField β§
βπ₯ β π΅ βπ β β π₯ < (π»βπ)) β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β π¦ β (0gβπ)) |
53 | 1 | simplbi 499 |
. . . . . . . . . . . . . 14
β’ (π β oField β π β Field) |
54 | | isfld 20230 |
. . . . . . . . . . . . . . 15
β’ (π β Field β (π β DivRing β§ π β CRing)) |
55 | 54 | simplbi 499 |
. . . . . . . . . . . . . 14
β’ (π β Field β π β
DivRing) |
56 | 53, 55 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β oField β π β
DivRing) |
57 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(Unitβπ) =
(Unitβπ) |
58 | 4, 57, 5 | drngunit 20224 |
. . . . . . . . . . . . 13
β’ (π β DivRing β (π¦ β (Unitβπ) β (π¦ β π΅ β§ π¦ β (0gβπ)))) |
59 | 45, 56, 58 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((((π β oField β§
βπ₯ β π΅ βπ β β π₯ < (π»βπ)) β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β (π¦ β (Unitβπ) β (π¦ β π΅ β§ π¦ β (0gβπ)))) |
60 | 43, 52, 59 | mpbir2and 712 |
. . . . . . . . . . 11
β’ ((((π β oField β§
βπ₯ β π΅ βπ β β π₯ < (π»βπ)) β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β π¦ β (Unitβπ)) |
61 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(/rβπ) = (/rβπ) |
62 | 4, 57, 61 | dvrcl 20123 |
. . . . . . . . . . 11
β’ ((π β Ring β§ π₯ β π΅ β§ π¦ β (Unitβπ)) β (π₯(/rβπ)π¦) β π΅) |
63 | 41, 42, 60, 62 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((π β oField β§
βπ₯ β π΅ βπ β β π₯ < (π»βπ)) β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β (π₯(/rβπ)π¦) β π΅) |
64 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β oField β§
βπ₯ β π΅ βπ β β π₯ < (π»βπ)) β βπ₯ β π΅ βπ β β π₯ < (π»βπ)) |
65 | | breq1 5112 |
. . . . . . . . . . . . . 14
β’ (π₯ = π§ β (π₯ < (π»βπ) β π§ < (π»βπ))) |
66 | 65 | rexbidv 3172 |
. . . . . . . . . . . . 13
β’ (π₯ = π§ β (βπ β β π₯ < (π»βπ) β βπ β β π§ < (π»βπ))) |
67 | 66 | cbvralvw 3224 |
. . . . . . . . . . . 12
β’
(βπ₯ β
π΅ βπ β β π₯ < (π»βπ) β βπ§ β π΅ βπ β β π§ < (π»βπ)) |
68 | 64, 67 | sylib 217 |
. . . . . . . . . . 11
β’ ((π β oField β§
βπ₯ β π΅ βπ β β π₯ < (π»βπ)) β βπ§ β π΅ βπ β β π§ < (π»βπ)) |
69 | 68 | ad2antrr 725 |
. . . . . . . . . 10
β’ ((((π β oField β§
βπ₯ β π΅ βπ β β π₯ < (π»βπ)) β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β βπ§ β π΅ βπ β β π§ < (π»βπ)) |
70 | | breq1 5112 |
. . . . . . . . . . . 12
β’ (π§ = (π₯(/rβπ)π¦) β (π§ < (π»βπ) β (π₯(/rβπ)π¦) < (π»βπ))) |
71 | 70 | rexbidv 3172 |
. . . . . . . . . . 11
β’ (π§ = (π₯(/rβπ)π¦) β (βπ β β π§ < (π»βπ) β βπ β β (π₯(/rβπ)π¦) < (π»βπ))) |
72 | 71 | rspcv 3579 |
. . . . . . . . . 10
β’ ((π₯(/rβπ)π¦) β π΅ β (βπ§ β π΅ βπ β β π§ < (π»βπ) β βπ β β (π₯(/rβπ)π¦) < (π»βπ))) |
73 | 63, 69, 72 | sylc 65 |
. . . . . . . . 9
β’ ((((π β oField β§
βπ₯ β π΅ βπ β β π₯ < (π»βπ)) β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β βπ β β (π₯(/rβπ)π¦) < (π»βπ)) |
74 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(.rβπ) = (.rβπ) |
75 | | simp-4l 782 |
. . . . . . . . . . . . . . 15
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β π β oField) |
76 | 75, 2 | syl 17 |
. . . . . . . . . . . . . 14
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β π β oRing) |
77 | 75, 27 | syl 17 |
. . . . . . . . . . . . . . 15
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β π β Ring) |
78 | | simp-4r 783 |
. . . . . . . . . . . . . . . 16
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β (π¦ β π΅ β§ π₯ β π΅)) |
79 | 78 | simprd 497 |
. . . . . . . . . . . . . . 15
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β π₯ β π΅) |
80 | 78 | simpld 496 |
. . . . . . . . . . . . . . . 16
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β π¦ β π΅) |
81 | | simpllr 775 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β (0gβπ) < π¦) |
82 | 77, 46, 47 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β (0gβπ) β π΅) |
83 | 75, 82, 80, 49 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β ((0gβπ) < π¦ β (0gβπ) β π¦)) |
84 | 81, 83 | mpd 15 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β (0gβπ) β π¦) |
85 | 84 | necomd 2996 |
. . . . . . . . . . . . . . . 16
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β π¦ β (0gβπ)) |
86 | 75, 56, 58 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β (π¦ β (Unitβπ) β (π¦ β π΅ β§ π¦ β (0gβπ)))) |
87 | 80, 85, 86 | mpbir2and 712 |
. . . . . . . . . . . . . . 15
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β π¦ β (Unitβπ)) |
88 | 77, 79, 87, 62 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β (π₯(/rβπ)π¦) β π΅) |
89 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β π β β) |
90 | 75, 89, 31 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β (π»βπ) = (π(.gβπ)(1rβπ))) |
91 | 77, 46 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β π β Grp) |
92 | 89, 28 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β π β β€) |
93 | 77, 12 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β (1rβπ) β π΅) |
94 | 4, 7 | mulgcl 18901 |
. . . . . . . . . . . . . . . 16
β’ ((π β Grp β§ π β β€ β§
(1rβπ)
β π΅) β (π(.gβπ)(1rβπ)) β π΅) |
95 | 91, 92, 93, 94 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β (π(.gβπ)(1rβπ)) β π΅) |
96 | 90, 95 | eqeltrd 2834 |
. . . . . . . . . . . . . 14
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β (π»βπ) β π΅) |
97 | 75, 56 | syl 17 |
. . . . . . . . . . . . . 14
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β π β DivRing) |
98 | | simpr 486 |
. . . . . . . . . . . . . 14
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β (π₯(/rβπ)π¦) < (π»βπ)) |
99 | 4, 74, 5, 76, 88, 96, 80, 6, 97, 98, 81 | orngrmullt 32157 |
. . . . . . . . . . . . 13
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β ((π₯(/rβπ)π¦)(.rβπ)π¦) < ((π»βπ)(.rβπ)π¦)) |
100 | 4, 57, 61, 74 | dvrcan1 20128 |
. . . . . . . . . . . . . 14
β’ ((π β Ring β§ π₯ β π΅ β§ π¦ β (Unitβπ)) β ((π₯(/rβπ)π¦)(.rβπ)π¦) = π₯) |
101 | 77, 79, 87, 100 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β ((π₯(/rβπ)π¦)(.rβπ)π¦) = π₯) |
102 | 90 | oveq1d 7376 |
. . . . . . . . . . . . . 14
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β ((π»βπ)(.rβπ)π¦) = ((π(.gβπ)(1rβπ))(.rβπ)π¦)) |
103 | 4, 7, 74 | mulgass2 20033 |
. . . . . . . . . . . . . . 15
β’ ((π β Ring β§ (π β β€ β§
(1rβπ)
β π΅ β§ π¦ β π΅)) β ((π(.gβπ)(1rβπ))(.rβπ)π¦) = (π(.gβπ)((1rβπ)(.rβπ)π¦))) |
104 | 77, 92, 93, 80, 103 | syl13anc 1373 |
. . . . . . . . . . . . . 14
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β ((π(.gβπ)(1rβπ))(.rβπ)π¦) = (π(.gβπ)((1rβπ)(.rβπ)π¦))) |
105 | 4, 74, 11 | ringlidm 20000 |
. . . . . . . . . . . . . . . 16
β’ ((π β Ring β§ π¦ β π΅) β ((1rβπ)(.rβπ)π¦) = π¦) |
106 | 77, 80, 105 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β ((1rβπ)(.rβπ)π¦) = π¦) |
107 | 106 | oveq2d 7377 |
. . . . . . . . . . . . . 14
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β (π(.gβπ)((1rβπ)(.rβπ)π¦)) = (π(.gβπ)π¦)) |
108 | 102, 104,
107 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β ((π»βπ)(.rβπ)π¦) = (π(.gβπ)π¦)) |
109 | 99, 101, 108 | 3brtr3d 5140 |
. . . . . . . . . . . 12
β’
(((((π β oField
β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β§ (π₯(/rβπ)π¦) < (π»βπ)) β π₯ < (π(.gβπ)π¦)) |
110 | 109 | ex 414 |
. . . . . . . . . . 11
β’ ((((π β oField β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β§ π β β) β ((π₯(/rβπ)π¦) < (π»βπ) β π₯ < (π(.gβπ)π¦))) |
111 | 110 | reximdva 3162 |
. . . . . . . . . 10
β’ (((π β oField β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β (βπ β β (π₯(/rβπ)π¦) < (π»βπ) β βπ β β π₯ < (π(.gβπ)π¦))) |
112 | 111 | adantllr 718 |
. . . . . . . . 9
β’ ((((π β oField β§
βπ₯ β π΅ βπ β β π₯ < (π»βπ)) β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β (βπ β β (π₯(/rβπ)π¦) < (π»βπ) β βπ β β π₯ < (π(.gβπ)π¦))) |
113 | 73, 112 | mpd 15 |
. . . . . . . 8
β’ ((((π β oField β§
βπ₯ β π΅ βπ β β π₯ < (π»βπ)) β§ (π¦ β π΅ β§ π₯ β π΅)) β§ (0gβπ) < π¦) β βπ β β π₯ < (π(.gβπ)π¦)) |
114 | 113 | ex 414 |
. . . . . . 7
β’ (((π β oField β§
βπ₯ β π΅ βπ β β π₯ < (π»βπ)) β§ (π¦ β π΅ β§ π₯ β π΅)) β ((0gβπ) < π¦ β βπ β β π₯ < (π(.gβπ)π¦))) |
115 | 114 | expr 458 |
. . . . . 6
β’ (((π β oField β§
βπ₯ β π΅ βπ β β π₯ < (π»βπ)) β§ π¦ β π΅) β (π₯ β π΅ β ((0gβπ) < π¦ β βπ β β π₯ < (π(.gβπ)π¦)))) |
116 | 40, 115 | ralrimi 3239 |
. . . . 5
β’ (((π β oField β§
βπ₯ β π΅ βπ β β π₯ < (π»βπ)) β§ π¦ β π΅) β βπ₯ β π΅ ((0gβπ) < π¦ β βπ β β π₯ < (π(.gβπ)π¦))) |
117 | 116 | ralrimiva 3140 |
. . . 4
β’ ((π β oField β§
βπ₯ β π΅ βπ β β π₯ < (π»βπ)) β βπ¦ β π΅ βπ₯ β π΅ ((0gβπ) < π¦ β βπ β β π₯ < (π(.gβπ)π¦))) |
118 | 117 | ex 414 |
. . 3
β’ (π β oField β
(βπ₯ β π΅ βπ β β π₯ < (π»βπ) β βπ¦ β π΅ βπ₯ β π΅ ((0gβπ) < π¦ β βπ β β π₯ < (π(.gβπ)π¦)))) |
119 | 35, 118 | impbid 211 |
. 2
β’ (π β oField β
(βπ¦ β π΅ βπ₯ β π΅ ((0gβπ) < π¦ β βπ β β π₯ < (π(.gβπ)π¦)) β βπ₯ β π΅ βπ β β π₯ < (π»βπ))) |
120 | 9, 119 | bitrd 279 |
1
β’ (π β oField β (π β Archi β
βπ₯ β π΅ βπ β β π₯ < (π»βπ))) |