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 ( 𝐹 ∈ oField → ( chr ‘ 𝐹 ) = 0 )

Proof

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