Metamath Proof Explorer

Theorem ofldchr

Description: The characteristic of an ordered field is zero. (Contributed by Thierry Arnoux, 21-Jan-2018) (Proof shortened by AV, 6-Oct-2020)

Ref Expression
Assertion ofldchr 
|- ( F e. oField -> ( chr ` F ) = 0 )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( od ` F ) = ( od ` F )
2 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
3 eqid 
 |-  ( chr ` F ) = ( chr ` F )
4 1 2 3 chrval 
 |-  ( ( od ` F ) ` ( 1r ` F ) ) = ( chr ` F )
5 ofldfld 
 |-  ( F e. oField -> F e. Field )
6 isfld 
 |-  ( F e. Field <-> ( F e. DivRing /\ F e. CRing ) )
7 6 simplbi 
 |-  ( F e. Field -> F e. DivRing )
8 drngring 
 |-  ( F e. DivRing -> F e. Ring )
9 5 7 8 3syl 
 |-  ( F e. oField -> F e. Ring )
10 eqid 
 |-  ( Base ` F ) = ( Base ` F )
11 10 2 ringidcl 
 |-  ( F e. Ring -> ( 1r ` F ) e. ( Base ` F ) )
12 eqid 
 |-  ( .g ` F ) = ( .g ` F )
13 eqid 
 |-  ( 0g ` F ) = ( 0g ` F )
14 eqid 
 |-  { y e. NN | ( y ( .g ` F ) ( 1r ` F ) ) = ( 0g ` F ) } = { y e. NN | ( y ( .g ` F ) ( 1r ` F ) ) = ( 0g ` F ) }
15 10 12 13 1 14 odval 
 |-  ( ( 1r ` F ) e. ( Base ` F ) -> ( ( od ` F ) ` ( 1r ` F ) ) = if ( { y e. NN | ( y ( .g ` F ) ( 1r ` F ) ) = ( 0g ` F ) } = (/) , 0 , inf ( { y e. NN | ( y ( .g ` F ) ( 1r ` F ) ) = ( 0g ` F ) } , RR , < ) ) )
16 9 11 15 3syl 
 |-  ( F e. oField -> ( ( od ` F ) ` ( 1r ` F ) ) = if ( { y e. NN | ( y ( .g ` F ) ( 1r ` F ) ) = ( 0g ` F ) } = (/) , 0 , inf ( { y e. NN | ( y ( .g ` F ) ( 1r ` F ) ) = ( 0g ` F ) } , RR , < ) ) )
17 oveq1 
 |-  ( n = 1 -> ( n ( .g ` F ) ( 1r ` F ) ) = ( 1 ( .g ` F ) ( 1r ` F ) ) )
18 17 breq2d 
 |-  ( n = 1 -> ( ( 0g ` F ) ( lt ` F ) ( n ( .g ` F ) ( 1r ` F ) ) <-> ( 0g ` F ) ( lt ` F ) ( 1 ( .g ` F ) ( 1r ` F ) ) ) )
19 18 imbi2d 
 |-  ( n = 1 -> ( ( F e. oField -> ( 0g ` F ) ( lt ` F ) ( n ( .g ` F ) ( 1r ` F ) ) ) <-> ( F e. oField -> ( 0g ` F ) ( lt ` F ) ( 1 ( .g ` F ) ( 1r ` F ) ) ) ) )
20 oveq1 
 |-  ( n = m -> ( n ( .g ` F ) ( 1r ` F ) ) = ( m ( .g ` F ) ( 1r ` F ) ) )
21 20 breq2d 
 |-  ( n = m -> ( ( 0g ` F ) ( lt ` F ) ( n ( .g ` F ) ( 1r ` F ) ) <-> ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) )
22 21 imbi2d 
 |-  ( n = m -> ( ( F e. oField -> ( 0g ` F ) ( lt ` F ) ( n ( .g ` F ) ( 1r ` F ) ) ) <-> ( F e. oField -> ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) ) )
23 oveq1 
 |-  ( n = ( m + 1 ) -> ( n ( .g ` F ) ( 1r ` F ) ) = ( ( m + 1 ) ( .g ` F ) ( 1r ` F ) ) )
24 23 breq2d 
 |-  ( n = ( m + 1 ) -> ( ( 0g ` F ) ( lt ` F ) ( n ( .g ` F ) ( 1r ` F ) ) <-> ( 0g ` F ) ( lt ` F ) ( ( m + 1 ) ( .g ` F ) ( 1r ` F ) ) ) )
25 24 imbi2d 
 |-  ( n = ( m + 1 ) -> ( ( F e. oField -> ( 0g ` F ) ( lt ` F ) ( n ( .g ` F ) ( 1r ` F ) ) ) <-> ( F e. oField -> ( 0g ` F ) ( lt ` F ) ( ( m + 1 ) ( .g ` F ) ( 1r ` F ) ) ) ) )
26 oveq1 
 |-  ( n = y -> ( n ( .g ` F ) ( 1r ` F ) ) = ( y ( .g ` F ) ( 1r ` F ) ) )
27 26 breq2d 
 |-  ( n = y -> ( ( 0g ` F ) ( lt ` F ) ( n ( .g ` F ) ( 1r ` F ) ) <-> ( 0g ` F ) ( lt ` F ) ( y ( .g ` F ) ( 1r ` F ) ) ) )
28 27 imbi2d 
 |-  ( n = y -> ( ( F e. oField -> ( 0g ` F ) ( lt ` F ) ( n ( .g ` F ) ( 1r ` F ) ) ) <-> ( F e. oField -> ( 0g ` F ) ( lt ` F ) ( y ( .g ` F ) ( 1r ` F ) ) ) ) )
29 eqid 
 |-  ( lt ` F ) = ( lt ` F )
30 13 2 29 ofldlt1 
 |-  ( F e. oField -> ( 0g ` F ) ( lt ` F ) ( 1r ` F ) )
31 9 11 syl 
 |-  ( F e. oField -> ( 1r ` F ) e. ( Base ` F ) )
32 10 12 mulg1 
 |-  ( ( 1r ` F ) e. ( Base ` F ) -> ( 1 ( .g ` F ) ( 1r ` F ) ) = ( 1r ` F ) )
33 31 32 syl 
 |-  ( F e. oField -> ( 1 ( .g ` F ) ( 1r ` F ) ) = ( 1r ` F ) )
34 30 33 breqtrrd 
 |-  ( F e. oField -> ( 0g ` F ) ( lt ` F ) ( 1 ( .g ` F ) ( 1r ` F ) ) )
35 ofldtos 
 |-  ( F e. oField -> F e. Toset )
36 tospos 
 |-  ( F e. Toset -> F e. Poset )
37 35 36 syl 
 |-  ( F e. oField -> F e. Poset )
38 37 ad2antlr 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> F e. Poset )
39 ringgrp 
 |-  ( F e. Ring -> F e. Grp )
40 9 39 syl 
 |-  ( F e. oField -> F e. Grp )
41 40 ad2antlr 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> F e. Grp )
42 10 13 grpidcl 
 |-  ( F e. Grp -> ( 0g ` F ) e. ( Base ` F ) )
43 41 42 syl 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> ( 0g ` F ) e. ( Base ` F ) )
44 grpmnd 
 |-  ( F e. Grp -> F e. Mnd )
45 mndmgm 
 |-  ( F e. Mnd -> F e. Mgm )
46 44 45 syl 
 |-  ( F e. Grp -> F e. Mgm )
47 41 46 syl 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> F e. Mgm )
48 simpll 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> m e. NN )
49 31 ad2antlr 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> ( 1r ` F ) e. ( Base ` F ) )
50 10 12 mulgnncl 
 |-  ( ( F e. Mgm /\ m e. NN /\ ( 1r ` F ) e. ( Base ` F ) ) -> ( m ( .g ` F ) ( 1r ` F ) ) e. ( Base ` F ) )
51 47 48 49 50 syl3anc 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> ( m ( .g ` F ) ( 1r ` F ) ) e. ( Base ` F ) )
52 48 peano2nnd 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> ( m + 1 ) e. NN )
53 10 12 mulgnncl 
 |-  ( ( F e. Mgm /\ ( m + 1 ) e. NN /\ ( 1r ` F ) e. ( Base ` F ) ) -> ( ( m + 1 ) ( .g ` F ) ( 1r ` F ) ) e. ( Base ` F ) )
54 47 52 49 53 syl3anc 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> ( ( m + 1 ) ( .g ` F ) ( 1r ` F ) ) e. ( Base ` F ) )
55 43 51 54 3jca 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> ( ( 0g ` F ) e. ( Base ` F ) /\ ( m ( .g ` F ) ( 1r ` F ) ) e. ( Base ` F ) /\ ( ( m + 1 ) ( .g ` F ) ( 1r ` F ) ) e. ( Base ` F ) ) )
56 simpr 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) )
57 simplr 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> F e. oField )
58 isofld 
 |-  ( F e. oField <-> ( F e. Field /\ F e. oRing ) )
59 58 simprbi 
 |-  ( F e. oField -> F e. oRing )
60 orngogrp 
 |-  ( F e. oRing -> F e. oGrp )
61 57 59 60 3syl 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> F e. oGrp )
62 30 ad2antlr 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> ( 0g ` F ) ( lt ` F ) ( 1r ` F ) )
63 eqid 
 |-  ( +g ` F ) = ( +g ` F )
64 10 29 63 ogrpaddlt 
 |-  ( ( F e. oGrp /\ ( ( 0g ` F ) e. ( Base ` F ) /\ ( 1r ` F ) e. ( Base ` F ) /\ ( m ( .g ` F ) ( 1r ` F ) ) e. ( Base ` F ) ) /\ ( 0g ` F ) ( lt ` F ) ( 1r ` F ) ) -> ( ( 0g ` F ) ( +g ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) ( lt ` F ) ( ( 1r ` F ) ( +g ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) )
65 61 43 49 51 62 64 syl131anc 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> ( ( 0g ` F ) ( +g ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) ( lt ` F ) ( ( 1r ` F ) ( +g ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) )
66 10 63 13 grplid 
 |-  ( ( F e. Grp /\ ( m ( .g ` F ) ( 1r ` F ) ) e. ( Base ` F ) ) -> ( ( 0g ` F ) ( +g ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) = ( m ( .g ` F ) ( 1r ` F ) ) )
67 41 51 66 syl2anc 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> ( ( 0g ` F ) ( +g ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) = ( m ( .g ` F ) ( 1r ` F ) ) )
68 67 eqcomd 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> ( m ( .g ` F ) ( 1r ` F ) ) = ( ( 0g ` F ) ( +g ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) )
69 10 12 63 mulgnnp1 
 |-  ( ( m e. NN /\ ( 1r ` F ) e. ( Base ` F ) ) -> ( ( m + 1 ) ( .g ` F ) ( 1r ` F ) ) = ( ( m ( .g ` F ) ( 1r ` F ) ) ( +g ` F ) ( 1r ` F ) ) )
70 48 49 69 syl2anc 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> ( ( m + 1 ) ( .g ` F ) ( 1r ` F ) ) = ( ( m ( .g ` F ) ( 1r ` F ) ) ( +g ` F ) ( 1r ` F ) ) )
71 ringcmn 
 |-  ( F e. Ring -> F e. CMnd )
72 57 9 71 3syl 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> F e. CMnd )
73 10 63 cmncom 
 |-  ( ( F e. CMnd /\ ( m ( .g ` F ) ( 1r ` F ) ) e. ( Base ` F ) /\ ( 1r ` F ) e. ( Base ` F ) ) -> ( ( m ( .g ` F ) ( 1r ` F ) ) ( +g ` F ) ( 1r ` F ) ) = ( ( 1r ` F ) ( +g ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) )
74 72 51 49 73 syl3anc 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> ( ( m ( .g ` F ) ( 1r ` F ) ) ( +g ` F ) ( 1r ` F ) ) = ( ( 1r ` F ) ( +g ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) )
75 70 74 eqtrd 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> ( ( m + 1 ) ( .g ` F ) ( 1r ` F ) ) = ( ( 1r ` F ) ( +g ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) )
76 65 68 75 3brtr4d 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> ( m ( .g ` F ) ( 1r ` F ) ) ( lt ` F ) ( ( m + 1 ) ( .g ` F ) ( 1r ` F ) ) )
77 10 29 plttr 
 |-  ( ( F e. Poset /\ ( ( 0g ` F ) e. ( Base ` F ) /\ ( m ( .g ` F ) ( 1r ` F ) ) e. ( Base ` F ) /\ ( ( m + 1 ) ( .g ` F ) ( 1r ` F ) ) e. ( Base ` F ) ) ) -> ( ( ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) /\ ( m ( .g ` F ) ( 1r ` F ) ) ( lt ` F ) ( ( m + 1 ) ( .g ` F ) ( 1r ` F ) ) ) -> ( 0g ` F ) ( lt ` F ) ( ( m + 1 ) ( .g ` F ) ( 1r ` F ) ) ) )
78 77 imp 
 |-  ( ( ( F e. Poset /\ ( ( 0g ` F ) e. ( Base ` F ) /\ ( m ( .g ` F ) ( 1r ` F ) ) e. ( Base ` F ) /\ ( ( m + 1 ) ( .g ` F ) ( 1r ` F ) ) e. ( Base ` F ) ) ) /\ ( ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) /\ ( m ( .g ` F ) ( 1r ` F ) ) ( lt ` F ) ( ( m + 1 ) ( .g ` F ) ( 1r ` F ) ) ) ) -> ( 0g ` F ) ( lt ` F ) ( ( m + 1 ) ( .g ` F ) ( 1r ` F ) ) )
79 38 55 56 76 78 syl22anc 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> ( 0g ` F ) ( lt ` F ) ( ( m + 1 ) ( .g ` F ) ( 1r ` F ) ) )
80 79 exp31 
 |-  ( m e. NN -> ( F e. oField -> ( ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) -> ( 0g ` F ) ( lt ` F ) ( ( m + 1 ) ( .g ` F ) ( 1r ` F ) ) ) ) )
81 80 a2d 
 |-  ( m e. NN -> ( ( F e. oField -> ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> ( F e. oField -> ( 0g ` F ) ( lt ` F ) ( ( m + 1 ) ( .g ` F ) ( 1r ` F ) ) ) ) )
82 19 22 25 28 34 81 nnind 
 |-  ( y e. NN -> ( F e. oField -> ( 0g ` F ) ( lt ` F ) ( y ( .g ` F ) ( 1r ` F ) ) ) )
83 82 impcom 
 |-  ( ( F e. oField /\ y e. NN ) -> ( 0g ` F ) ( lt ` F ) ( y ( .g ` F ) ( 1r ` F ) ) )
84 fvex 
 |-  ( 0g ` F ) e. _V
85 ovex 
 |-  ( y ( .g ` F ) ( 1r ` F ) ) e. _V
86 29 pltne 
 |-  ( ( F e. oField /\ ( 0g ` F ) e. _V /\ ( y ( .g ` F ) ( 1r ` F ) ) e. _V ) -> ( ( 0g ` F ) ( lt ` F ) ( y ( .g ` F ) ( 1r ` F ) ) -> ( 0g ` F ) =/= ( y ( .g ` F ) ( 1r ` F ) ) ) )
87 84 85 86 mp3an23 
 |-  ( F e. oField -> ( ( 0g ` F ) ( lt ` F ) ( y ( .g ` F ) ( 1r ` F ) ) -> ( 0g ` F ) =/= ( y ( .g ` F ) ( 1r ` F ) ) ) )
88 87 adantr 
 |-  ( ( F e. oField /\ y e. NN ) -> ( ( 0g ` F ) ( lt ` F ) ( y ( .g ` F ) ( 1r ` F ) ) -> ( 0g ` F ) =/= ( y ( .g ` F ) ( 1r ` F ) ) ) )
89 83 88 mpd 
 |-  ( ( F e. oField /\ y e. NN ) -> ( 0g ` F ) =/= ( y ( .g ` F ) ( 1r ` F ) ) )
90 89 necomd 
 |-  ( ( F e. oField /\ y e. NN ) -> ( y ( .g ` F ) ( 1r ` F ) ) =/= ( 0g ` F ) )
91 90 neneqd 
 |-  ( ( F e. oField /\ y e. NN ) -> -. ( y ( .g ` F ) ( 1r ` F ) ) = ( 0g ` F ) )
92 91 ralrimiva 
 |-  ( F e. oField -> A. y e. NN -. ( y ( .g ` F ) ( 1r ` F ) ) = ( 0g ` F ) )
93 rabeq0 
 |-  ( { y e. NN | ( y ( .g ` F ) ( 1r ` F ) ) = ( 0g ` F ) } = (/) <-> A. y e. NN -. ( y ( .g ` F ) ( 1r ` F ) ) = ( 0g ` F ) )
94 92 93 sylibr 
 |-  ( F e. oField -> { y e. NN | ( y ( .g ` F ) ( 1r ` F ) ) = ( 0g ` F ) } = (/) )
95 94 iftrued 
 |-  ( F e. oField -> if ( { y e. NN | ( y ( .g ` F ) ( 1r ` F ) ) = ( 0g ` F ) } = (/) , 0 , inf ( { y e. NN | ( y ( .g ` F ) ( 1r ` F ) ) = ( 0g ` F ) } , RR , < ) ) = 0 )
96 16 95 eqtrd 
 |-  ( F e. oField -> ( ( od ` F ) ` ( 1r ` F ) ) = 0 )
97 4 96 eqtr3id 
 |-  ( F e. oField -> ( chr ` F ) = 0 )