Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’
(odβπΉ) =
(odβπΉ) |
2 | | eqid 2733 |
. . 3
β’
(1rβπΉ) = (1rβπΉ) |
3 | | eqid 2733 |
. . 3
β’
(chrβπΉ) =
(chrβπΉ) |
4 | 1, 2, 3 | chrval 20951 |
. 2
β’
((odβπΉ)β(1rβπΉ)) = (chrβπΉ) |
5 | | ofldfld 32159 |
. . . . 5
β’ (πΉ β oField β πΉ β Field) |
6 | | isfld 20230 |
. . . . . 6
β’ (πΉ β Field β (πΉ β DivRing β§ πΉ β CRing)) |
7 | 6 | simplbi 499 |
. . . . 5
β’ (πΉ β Field β πΉ β
DivRing) |
8 | | drngring 20226 |
. . . . 5
β’ (πΉ β DivRing β πΉ β Ring) |
9 | 5, 7, 8 | 3syl 18 |
. . . 4
β’ (πΉ β oField β πΉ β Ring) |
10 | | eqid 2733 |
. . . . 5
β’
(BaseβπΉ) =
(BaseβπΉ) |
11 | 10, 2 | ringidcl 19997 |
. . . 4
β’ (πΉ β Ring β
(1rβπΉ)
β (BaseβπΉ)) |
12 | | eqid 2733 |
. . . . 5
β’
(.gβπΉ) = (.gβπΉ) |
13 | | eqid 2733 |
. . . . 5
β’
(0gβπΉ) = (0gβπΉ) |
14 | | eqid 2733 |
. . . . 5
β’ {π¦ β β β£ (π¦(.gβπΉ)(1rβπΉ)) = (0gβπΉ)} = {π¦ β β β£ (π¦(.gβπΉ)(1rβπΉ)) = (0gβπΉ)} |
15 | 10, 12, 13, 1, 14 | odval 19324 |
. . . 4
β’
((1rβπΉ) β (BaseβπΉ) β ((odβπΉ)β(1rβπΉ)) = if({π¦ β β β£ (π¦(.gβπΉ)(1rβπΉ)) = (0gβπΉ)} = β
, 0, inf({π¦ β β β£ (π¦(.gβπΉ)(1rβπΉ)) = (0gβπΉ)}, β, < ))) |
16 | 9, 11, 15 | 3syl 18 |
. . 3
β’ (πΉ β oField β
((odβπΉ)β(1rβπΉ)) = if({π¦ β β β£ (π¦(.gβπΉ)(1rβπΉ)) = (0gβπΉ)} = β
, 0, inf({π¦ β β β£ (π¦(.gβπΉ)(1rβπΉ)) = (0gβπΉ)}, β, < ))) |
17 | | oveq1 7368 |
. . . . . . . . . . . . 13
β’ (π = 1 β (π(.gβπΉ)(1rβπΉ)) = (1(.gβπΉ)(1rβπΉ))) |
18 | 17 | breq2d 5121 |
. . . . . . . . . . . 12
β’ (π = 1 β
((0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ)) β (0gβπΉ)(ltβπΉ)(1(.gβπΉ)(1rβπΉ)))) |
19 | 18 | imbi2d 341 |
. . . . . . . . . . 11
β’ (π = 1 β ((πΉ β oField β
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β (πΉ β oField β
(0gβπΉ)(ltβπΉ)(1(.gβπΉ)(1rβπΉ))))) |
20 | | oveq1 7368 |
. . . . . . . . . . . . 13
β’ (π = π β (π(.gβπΉ)(1rβπΉ)) = (π(.gβπΉ)(1rβπΉ))) |
21 | 20 | breq2d 5121 |
. . . . . . . . . . . 12
β’ (π = π β ((0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ)) β (0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ)))) |
22 | 21 | imbi2d 341 |
. . . . . . . . . . 11
β’ (π = π β ((πΉ β oField β
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β (πΉ β oField β
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))))) |
23 | | oveq1 7368 |
. . . . . . . . . . . . 13
β’ (π = (π + 1) β (π(.gβπΉ)(1rβπΉ)) = ((π + 1)(.gβπΉ)(1rβπΉ))) |
24 | 23 | breq2d 5121 |
. . . . . . . . . . . 12
β’ (π = (π + 1) β ((0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ)) β (0gβπΉ)(ltβπΉ)((π + 1)(.gβπΉ)(1rβπΉ)))) |
25 | 24 | imbi2d 341 |
. . . . . . . . . . 11
β’ (π = (π + 1) β ((πΉ β oField β
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β (πΉ β oField β
(0gβπΉ)(ltβπΉ)((π + 1)(.gβπΉ)(1rβπΉ))))) |
26 | | oveq1 7368 |
. . . . . . . . . . . . 13
β’ (π = π¦ β (π(.gβπΉ)(1rβπΉ)) = (π¦(.gβπΉ)(1rβπΉ))) |
27 | 26 | breq2d 5121 |
. . . . . . . . . . . 12
β’ (π = π¦ β ((0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ)) β (0gβπΉ)(ltβπΉ)(π¦(.gβπΉ)(1rβπΉ)))) |
28 | 27 | imbi2d 341 |
. . . . . . . . . . 11
β’ (π = π¦ β ((πΉ β oField β
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β (πΉ β oField β
(0gβπΉ)(ltβπΉ)(π¦(.gβπΉ)(1rβπΉ))))) |
29 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(ltβπΉ) =
(ltβπΉ) |
30 | 13, 2, 29 | ofldlt1 32162 |
. . . . . . . . . . . 12
β’ (πΉ β oField β
(0gβπΉ)(ltβπΉ)(1rβπΉ)) |
31 | 9, 11 | syl 17 |
. . . . . . . . . . . . 13
β’ (πΉ β oField β
(1rβπΉ)
β (BaseβπΉ)) |
32 | 10, 12 | mulg1 18891 |
. . . . . . . . . . . . 13
β’
((1rβπΉ) β (BaseβπΉ) β (1(.gβπΉ)(1rβπΉ)) = (1rβπΉ)) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . 12
β’ (πΉ β oField β
(1(.gβπΉ)(1rβπΉ)) = (1rβπΉ)) |
34 | 30, 33 | breqtrrd 5137 |
. . . . . . . . . . 11
β’ (πΉ β oField β
(0gβπΉ)(ltβπΉ)(1(.gβπΉ)(1rβπΉ))) |
35 | | ofldtos 32160 |
. . . . . . . . . . . . . . . 16
β’ (πΉ β oField β πΉ β Toset) |
36 | | tospos 18317 |
. . . . . . . . . . . . . . . 16
β’ (πΉ β Toset β πΉ β Poset) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (πΉ β oField β πΉ β Poset) |
38 | 37 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ πΉ β oField) β§
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β πΉ β Poset) |
39 | | ringgrp 19977 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉ β Ring β πΉ β Grp) |
40 | 9, 39 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ β oField β πΉ β Grp) |
41 | 40 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ πΉ β oField) β§
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β πΉ β Grp) |
42 | 10, 13 | grpidcl 18786 |
. . . . . . . . . . . . . . . 16
β’ (πΉ β Grp β
(0gβπΉ)
β (BaseβπΉ)) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ πΉ β oField) β§
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β (0gβπΉ) β (BaseβπΉ)) |
44 | | grpmnd 18763 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉ β Grp β πΉ β Mnd) |
45 | | mndmgm 18571 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉ β Mnd β πΉ β Mgm) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ β Grp β πΉ β Mgm) |
47 | 41, 46 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ πΉ β oField) β§
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β πΉ β Mgm) |
48 | | simpll 766 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ πΉ β oField) β§
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β π β β) |
49 | 31 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ πΉ β oField) β§
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β (1rβπΉ) β (BaseβπΉ)) |
50 | 10, 12 | mulgnncl 18899 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ β Mgm β§ π β β β§
(1rβπΉ)
β (BaseβπΉ))
β (π(.gβπΉ)(1rβπΉ)) β (BaseβπΉ)) |
51 | 47, 48, 49, 50 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ πΉ β oField) β§
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β (π(.gβπΉ)(1rβπΉ)) β (BaseβπΉ)) |
52 | 48 | peano2nnd 12178 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ πΉ β oField) β§
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β (π + 1) β β) |
53 | 10, 12 | mulgnncl 18899 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ β Mgm β§ (π + 1) β β β§
(1rβπΉ)
β (BaseβπΉ))
β ((π +
1)(.gβπΉ)(1rβπΉ)) β (BaseβπΉ)) |
54 | 47, 52, 49, 53 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ πΉ β oField) β§
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β ((π + 1)(.gβπΉ)(1rβπΉ)) β (BaseβπΉ)) |
55 | 43, 51, 54 | 3jca 1129 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ πΉ β oField) β§
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β ((0gβπΉ) β (BaseβπΉ) β§ (π(.gβπΉ)(1rβπΉ)) β (BaseβπΉ) β§ ((π + 1)(.gβπΉ)(1rβπΉ)) β (BaseβπΉ))) |
56 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ πΉ β oField) β§
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β (0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) |
57 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ πΉ β oField) β§
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β πΉ β oField) |
58 | | isofld 32151 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉ β oField β (πΉ β Field β§ πΉ β oRing)) |
59 | 58 | simprbi 498 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ β oField β πΉ β oRing) |
60 | | orngogrp 32150 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ β oRing β πΉ β oGrp) |
61 | 57, 59, 60 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ πΉ β oField) β§
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β πΉ β oGrp) |
62 | 30 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ πΉ β oField) β§
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β (0gβπΉ)(ltβπΉ)(1rβπΉ)) |
63 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
(+gβπΉ) = (+gβπΉ) |
64 | 10, 29, 63 | ogrpaddlt 31981 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ β oGrp β§
((0gβπΉ)
β (BaseβπΉ) β§
(1rβπΉ)
β (BaseβπΉ) β§
(π(.gβπΉ)(1rβπΉ)) β (BaseβπΉ)) β§ (0gβπΉ)(ltβπΉ)(1rβπΉ)) β ((0gβπΉ)(+gβπΉ)(π(.gβπΉ)(1rβπΉ)))(ltβπΉ)((1rβπΉ)(+gβπΉ)(π(.gβπΉ)(1rβπΉ)))) |
65 | 61, 43, 49, 51, 62, 64 | syl131anc 1384 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ πΉ β oField) β§
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β ((0gβπΉ)(+gβπΉ)(π(.gβπΉ)(1rβπΉ)))(ltβπΉ)((1rβπΉ)(+gβπΉ)(π(.gβπΉ)(1rβπΉ)))) |
66 | 10, 63, 13 | grplid 18788 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ β Grp β§ (π(.gβπΉ)(1rβπΉ)) β (BaseβπΉ)) β
((0gβπΉ)(+gβπΉ)(π(.gβπΉ)(1rβπΉ))) = (π(.gβπΉ)(1rβπΉ))) |
67 | 41, 51, 66 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ πΉ β oField) β§
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β ((0gβπΉ)(+gβπΉ)(π(.gβπΉ)(1rβπΉ))) = (π(.gβπΉ)(1rβπΉ))) |
68 | 67 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ πΉ β oField) β§
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β (π(.gβπΉ)(1rβπΉ)) = ((0gβπΉ)(+gβπΉ)(π(.gβπΉ)(1rβπΉ)))) |
69 | 10, 12, 63 | mulgnnp1 18892 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§
(1rβπΉ)
β (BaseβπΉ))
β ((π +
1)(.gβπΉ)(1rβπΉ)) = ((π(.gβπΉ)(1rβπΉ))(+gβπΉ)(1rβπΉ))) |
70 | 48, 49, 69 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ πΉ β oField) β§
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β ((π + 1)(.gβπΉ)(1rβπΉ)) = ((π(.gβπΉ)(1rβπΉ))(+gβπΉ)(1rβπΉ))) |
71 | | ringcmn 20011 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉ β Ring β πΉ β CMnd) |
72 | 57, 9, 71 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ πΉ β oField) β§
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β πΉ β CMnd) |
73 | 10, 63 | cmncom 19588 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ β CMnd β§ (π(.gβπΉ)(1rβπΉ)) β (BaseβπΉ) β§
(1rβπΉ)
β (BaseβπΉ))
β ((π(.gβπΉ)(1rβπΉ))(+gβπΉ)(1rβπΉ)) = ((1rβπΉ)(+gβπΉ)(π(.gβπΉ)(1rβπΉ)))) |
74 | 72, 51, 49, 73 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ πΉ β oField) β§
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β ((π(.gβπΉ)(1rβπΉ))(+gβπΉ)(1rβπΉ)) = ((1rβπΉ)(+gβπΉ)(π(.gβπΉ)(1rβπΉ)))) |
75 | 70, 74 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ πΉ β oField) β§
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β ((π + 1)(.gβπΉ)(1rβπΉ)) = ((1rβπΉ)(+gβπΉ)(π(.gβπΉ)(1rβπΉ)))) |
76 | 65, 68, 75 | 3brtr4d 5141 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ πΉ β oField) β§
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β (π(.gβπΉ)(1rβπΉ))(ltβπΉ)((π + 1)(.gβπΉ)(1rβπΉ))) |
77 | 10, 29 | plttr 18239 |
. . . . . . . . . . . . . . 15
β’ ((πΉ β Poset β§
((0gβπΉ)
β (BaseβπΉ) β§
(π(.gβπΉ)(1rβπΉ)) β (BaseβπΉ) β§ ((π + 1)(.gβπΉ)(1rβπΉ)) β (BaseβπΉ))) β (((0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ)) β§ (π(.gβπΉ)(1rβπΉ))(ltβπΉ)((π + 1)(.gβπΉ)(1rβπΉ))) β (0gβπΉ)(ltβπΉ)((π + 1)(.gβπΉ)(1rβπΉ)))) |
78 | 77 | imp 408 |
. . . . . . . . . . . . . 14
β’ (((πΉ β Poset β§
((0gβπΉ)
β (BaseβπΉ) β§
(π(.gβπΉ)(1rβπΉ)) β (BaseβπΉ) β§ ((π + 1)(.gβπΉ)(1rβπΉ)) β (BaseβπΉ))) β§ ((0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ)) β§ (π(.gβπΉ)(1rβπΉ))(ltβπΉ)((π + 1)(.gβπΉ)(1rβπΉ)))) β (0gβπΉ)(ltβπΉ)((π + 1)(.gβπΉ)(1rβπΉ))) |
79 | 38, 55, 56, 76, 78 | syl22anc 838 |
. . . . . . . . . . . . 13
β’ (((π β β β§ πΉ β oField) β§
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β (0gβπΉ)(ltβπΉ)((π + 1)(.gβπΉ)(1rβπΉ))) |
80 | 79 | exp31 421 |
. . . . . . . . . . . 12
β’ (π β β β (πΉ β oField β
((0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ)) β (0gβπΉ)(ltβπΉ)((π + 1)(.gβπΉ)(1rβπΉ))))) |
81 | 80 | a2d 29 |
. . . . . . . . . . 11
β’ (π β β β ((πΉ β oField β
(0gβπΉ)(ltβπΉ)(π(.gβπΉ)(1rβπΉ))) β (πΉ β oField β
(0gβπΉ)(ltβπΉ)((π + 1)(.gβπΉ)(1rβπΉ))))) |
82 | 19, 22, 25, 28, 34, 81 | nnind 12179 |
. . . . . . . . . 10
β’ (π¦ β β β (πΉ β oField β
(0gβπΉ)(ltβπΉ)(π¦(.gβπΉ)(1rβπΉ)))) |
83 | 82 | impcom 409 |
. . . . . . . . 9
β’ ((πΉ β oField β§ π¦ β β) β
(0gβπΉ)(ltβπΉ)(π¦(.gβπΉ)(1rβπΉ))) |
84 | | fvex 6859 |
. . . . . . . . . . 11
β’
(0gβπΉ) β V |
85 | | ovex 7394 |
. . . . . . . . . . 11
β’ (π¦(.gβπΉ)(1rβπΉ)) β V |
86 | 29 | pltne 18231 |
. . . . . . . . . . 11
β’ ((πΉ β oField β§
(0gβπΉ)
β V β§ (π¦(.gβπΉ)(1rβπΉ)) β V) β
((0gβπΉ)(ltβπΉ)(π¦(.gβπΉ)(1rβπΉ)) β (0gβπΉ) β (π¦(.gβπΉ)(1rβπΉ)))) |
87 | 84, 85, 86 | mp3an23 1454 |
. . . . . . . . . 10
β’ (πΉ β oField β
((0gβπΉ)(ltβπΉ)(π¦(.gβπΉ)(1rβπΉ)) β (0gβπΉ) β (π¦(.gβπΉ)(1rβπΉ)))) |
88 | 87 | adantr 482 |
. . . . . . . . 9
β’ ((πΉ β oField β§ π¦ β β) β
((0gβπΉ)(ltβπΉ)(π¦(.gβπΉ)(1rβπΉ)) β (0gβπΉ) β (π¦(.gβπΉ)(1rβπΉ)))) |
89 | 83, 88 | mpd 15 |
. . . . . . . 8
β’ ((πΉ β oField β§ π¦ β β) β
(0gβπΉ)
β (π¦(.gβπΉ)(1rβπΉ))) |
90 | 89 | necomd 2996 |
. . . . . . 7
β’ ((πΉ β oField β§ π¦ β β) β (π¦(.gβπΉ)(1rβπΉ)) β
(0gβπΉ)) |
91 | 90 | neneqd 2945 |
. . . . . 6
β’ ((πΉ β oField β§ π¦ β β) β Β¬
(π¦(.gβπΉ)(1rβπΉ)) = (0gβπΉ)) |
92 | 91 | ralrimiva 3140 |
. . . . 5
β’ (πΉ β oField β
βπ¦ β β
Β¬ (π¦(.gβπΉ)(1rβπΉ)) = (0gβπΉ)) |
93 | | rabeq0 4348 |
. . . . 5
β’ ({π¦ β β β£ (π¦(.gβπΉ)(1rβπΉ)) = (0gβπΉ)} = β
β
βπ¦ β β
Β¬ (π¦(.gβπΉ)(1rβπΉ)) = (0gβπΉ)) |
94 | 92, 93 | sylibr 233 |
. . . 4
β’ (πΉ β oField β {π¦ β β β£ (π¦(.gβπΉ)(1rβπΉ)) = (0gβπΉ)} = β
) |
95 | 94 | iftrued 4498 |
. . 3
β’ (πΉ β oField β if({π¦ β β β£ (π¦(.gβπΉ)(1rβπΉ)) = (0gβπΉ)} = β
, 0, inf({π¦ β β β£ (π¦(.gβπΉ)(1rβπΉ)) = (0gβπΉ)}, β, < )) =
0) |
96 | 16, 95 | eqtrd 2773 |
. 2
β’ (πΉ β oField β
((odβπΉ)β(1rβπΉ)) = 0) |
97 | 4, 96 | eqtr3id 2787 |
1
β’ (πΉ β oField β
(chrβπΉ) =
0) |