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 9 ringgrpd 
 |-  ( F e. oField -> F e. Grp )
40 39 ad2antlr 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> F e. Grp )
41 10 13 grpidcl 
 |-  ( F e. Grp -> ( 0g ` F ) e. ( Base ` F ) )
42 40 41 syl 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> ( 0g ` F ) e. ( Base ` F ) )
43 40 grpmgmd 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> F e. Mgm )
44 simpll 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> m e. NN )
45 31 ad2antlr 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> ( 1r ` F ) e. ( Base ` F ) )
46 10 12 mulgnncl 
 |-  ( ( F e. Mgm /\ m e. NN /\ ( 1r ` F ) e. ( Base ` F ) ) -> ( m ( .g ` F ) ( 1r ` F ) ) e. ( Base ` F ) )
47 43 44 45 46 syl3anc 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> ( m ( .g ` F ) ( 1r ` F ) ) e. ( Base ` F ) )
48 44 peano2nnd 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> ( m + 1 ) e. NN )
49 10 12 mulgnncl 
 |-  ( ( F e. Mgm /\ ( m + 1 ) e. NN /\ ( 1r ` F ) e. ( Base ` F ) ) -> ( ( m + 1 ) ( .g ` F ) ( 1r ` F ) ) e. ( Base ` F ) )
50 43 48 45 49 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 ) )
51 42 47 50 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 ) ) )
52 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 ) ) )
53 simplr 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> F e. oField )
54 isofld 
 |-  ( F e. oField <-> ( F e. Field /\ F e. oRing ) )
55 54 simprbi 
 |-  ( F e. oField -> F e. oRing )
56 orngogrp 
 |-  ( F e. oRing -> F e. oGrp )
57 53 55 56 3syl 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> F e. oGrp )
58 30 ad2antlr 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> ( 0g ` F ) ( lt ` F ) ( 1r ` F ) )
59 eqid 
 |-  ( +g ` F ) = ( +g ` F )
60 10 29 59 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 ) ) ) )
61 57 42 45 47 58 60 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 ) ) ) )
62 10 59 13 40 47 grplidd 
 |-  ( ( ( 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 ) ) )
63 62 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 ) ) ) )
64 10 12 59 mulgnnp1 
 |-  ( ( m e. NN /\ ( 1r ` F ) e. ( Base ` F ) ) -> ( ( m + 1 ) ( .g ` F ) ( 1r ` F ) ) = ( ( m ( .g ` F ) ( 1r ` F ) ) ( +g ` F ) ( 1r ` F ) ) )
65 44 45 64 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 ) ) )
66 ringcmn 
 |-  ( F e. Ring -> F e. CMnd )
67 53 9 66 3syl 
 |-  ( ( ( m e. NN /\ F e. oField ) /\ ( 0g ` F ) ( lt ` F ) ( m ( .g ` F ) ( 1r ` F ) ) ) -> F e. CMnd )
68 10 59 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 ) ) ) )
69 67 47 45 68 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 ) ) ) )
70 65 69 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 ) ) ) )
71 61 63 70 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 ) ) )
72 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 ) ) ) )
73 72 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 ) ) )
74 38 51 52 71 73 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 ) ) )
75 74 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 ) ) ) ) )
76 75 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 ) ) ) ) )
77 19 22 25 28 34 76 nnind 
 |-  ( y e. NN -> ( F e. oField -> ( 0g ` F ) ( lt ` F ) ( y ( .g ` F ) ( 1r ` F ) ) ) )
78 77 impcom 
 |-  ( ( F e. oField /\ y e. NN ) -> ( 0g ` F ) ( lt ` F ) ( y ( .g ` F ) ( 1r ` F ) ) )
79 fvex 
 |-  ( 0g ` F ) e. _V
80 ovex 
 |-  ( y ( .g ` F ) ( 1r ` F ) ) e. _V
81 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 ) ) ) )
82 79 80 81 mp3an23 
 |-  ( F e. oField -> ( ( 0g ` F ) ( lt ` F ) ( y ( .g ` F ) ( 1r ` F ) ) -> ( 0g ` F ) =/= ( y ( .g ` F ) ( 1r ` F ) ) ) )
83 82 adantr 
 |-  ( ( F e. oField /\ y e. NN ) -> ( ( 0g ` F ) ( lt ` F ) ( y ( .g ` F ) ( 1r ` F ) ) -> ( 0g ` F ) =/= ( y ( .g ` F ) ( 1r ` F ) ) ) )
84 78 83 mpd 
 |-  ( ( F e. oField /\ y e. NN ) -> ( 0g ` F ) =/= ( y ( .g ` F ) ( 1r ` F ) ) )
85 84 necomd 
 |-  ( ( F e. oField /\ y e. NN ) -> ( y ( .g ` F ) ( 1r ` F ) ) =/= ( 0g ` F ) )
86 85 neneqd 
 |-  ( ( F e. oField /\ y e. NN ) -> -. ( y ( .g ` F ) ( 1r ` F ) ) = ( 0g ` F ) )
87 86 ralrimiva 
 |-  ( F e. oField -> A. y e. NN -. ( y ( .g ` F ) ( 1r ` F ) ) = ( 0g ` F ) )
88 rabeq0 
 |-  ( { y e. NN | ( y ( .g ` F ) ( 1r ` F ) ) = ( 0g ` F ) } = (/) <-> A. y e. NN -. ( y ( .g ` F ) ( 1r ` F ) ) = ( 0g ` F ) )
89 87 88 sylibr 
 |-  ( F e. oField -> { y e. NN | ( y ( .g ` F ) ( 1r ` F ) ) = ( 0g ` F ) } = (/) )
90 89 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 )
91 16 90 eqtrd 
 |-  ( F e. oField -> ( ( od ` F ) ` ( 1r ` F ) ) = 0 )
92 4 91 eqtr3id 
 |-  ( F e. oField -> ( chr ` F ) = 0 )