This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fiabv

Description: In a finite domain (a finite field), the only absolute value is the trivial one ( abvtrivg ). (Contributed by SN, 3-Jul-2025)

Ref Expression
Hypotheses fiabv.a ⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
fiabv.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
fiabv.0 ⊢ 0 = ( 0g ‘ 𝑅 )
fiabv.t ⊢ 𝑇 = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 = 0 , 0 , 1 ) )
fiabv.r ⊢ ( 𝜑 → 𝑅 ∈ Domn )
fiabv.f ⊢ ( 𝜑 → 𝐵 ∈ Fin )
Assertion fiabv ( 𝜑 → 𝐴 = { 𝑇 } )

Proof

Step Hyp Ref Expression
1 fiabv.a ⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
2 fiabv.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 fiabv.0 ⊢ 0 = ( 0g ‘ 𝑅 )
4 fiabv.t ⊢ 𝑇 = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 = 0 , 0 , 1 ) )
5 fiabv.r ⊢ ( 𝜑 → 𝑅 ∈ Domn )
6 fiabv.f ⊢ ( 𝜑 → 𝐵 ∈ Fin )
7 1 2 abvf ⊢ ( 𝑎 ∈ 𝐴 → 𝑎 : 𝐵 ⟶ ℝ )
8 7 ffnd ⊢ ( 𝑎 ∈ 𝐴 → 𝑎 Fn 𝐵 )
9 8 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑎 Fn 𝐵 )
10 1 2 3 4 abvtrivg ⊢ ( 𝑅 ∈ Domn → 𝑇 ∈ 𝐴 )
11 5 10 syl ⊢ ( 𝜑 → 𝑇 ∈ 𝐴 )
12 1 2 abvf ⊢ ( 𝑇 ∈ 𝐴 → 𝑇 : 𝐵 ⟶ ℝ )
13 11 12 syl ⊢ ( 𝜑 → 𝑇 : 𝐵 ⟶ ℝ )
14 13 ffnd ⊢ ( 𝜑 → 𝑇 Fn 𝐵 )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑇 Fn 𝐵 )
16 fveq2 ⊢ ( 𝑏 = 0 → ( 𝑎 ‘ 𝑏 ) = ( 𝑎 ‘ 0 ) )
17 fveq2 ⊢ ( 𝑏 = 0 → ( 𝑇 ‘ 𝑏 ) = ( 𝑇 ‘ 0 ) )
18 16 17 eqeq12d ⊢ ( 𝑏 = 0 → ( ( 𝑎 ‘ 𝑏 ) = ( 𝑇 ‘ 𝑏 ) ↔ ( 𝑎 ‘ 0 ) = ( 𝑇 ‘ 0 ) ) )
19 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
20 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝑅 ) ) = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
21 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) → 𝑅 ∈ Domn )
22 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) → 𝐵 ∈ Fin )
23 eldifsn ⊢ ( 𝑏 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 𝑏 ∈ 𝐵 ∧ 𝑏 ≠ 0 ) )
24 23 biimpri ⊢ ( ( 𝑏 ∈ 𝐵 ∧ 𝑏 ≠ 0 ) → 𝑏 ∈ ( 𝐵 ∖ { 0 } ) )
25 24 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) → 𝑏 ∈ ( 𝐵 ∖ { 0 } ) )
26 2 3 19 20 21 22 25 fidomncyc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) → ∃ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑏 ) = ( 1r ‘ 𝑅 ) )
27 simprr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑏 ) = ( 1r ‘ 𝑅 ) ) ) → ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑏 ) = ( 1r ‘ 𝑅 ) )
28 27 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑏 ) = ( 1r ‘ 𝑅 ) ) ) → ( 𝑎 ‘ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑏 ) ) = ( 𝑎 ‘ ( 1r ‘ 𝑅 ) ) )
29 domnnzr ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
30 5 29 syl ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
31 30 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑏 ) = ( 1r ‘ 𝑅 ) ) ) → 𝑅 ∈ NzRing )
32 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑏 ) = ( 1r ‘ 𝑅 ) ) ) → 𝑎 ∈ 𝐴 )
33 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑏 ) = ( 1r ‘ 𝑅 ) ) ) → 𝑏 ∈ 𝐵 )
34 simprl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑏 ) = ( 1r ‘ 𝑅 ) ) ) → 𝑛 ∈ ℕ )
35 34 nnnn0d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑏 ) = ( 1r ‘ 𝑅 ) ) ) → 𝑛 ∈ ℕ0 )
36 1 20 2 31 32 33 35 abvexp ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑏 ) = ( 1r ‘ 𝑅 ) ) ) → ( 𝑎 ‘ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑏 ) ) = ( ( 𝑎 ‘ 𝑏 ) ↑ 𝑛 ) )
37 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ 𝐴 )
38 19 3 nzrnz ⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ 0 )
39 29 38 syl ⊢ ( 𝑅 ∈ Domn → ( 1r ‘ 𝑅 ) ≠ 0 )
40 5 39 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ≠ 0 )
41 40 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 1r ‘ 𝑅 ) ≠ 0 )
42 1 19 3 abv1z ⊢ ( ( 𝑎 ∈ 𝐴 ∧ ( 1r ‘ 𝑅 ) ≠ 0 ) → ( 𝑎 ‘ ( 1r ‘ 𝑅 ) ) = 1 )
43 37 41 42 syl2anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑎 ‘ ( 1r ‘ 𝑅 ) ) = 1 )
44 43 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑏 ) = ( 1r ‘ 𝑅 ) ) ) → ( 𝑎 ‘ ( 1r ‘ 𝑅 ) ) = 1 )
45 28 36 44 3eqtr3d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑏 ) = ( 1r ‘ 𝑅 ) ) ) → ( ( 𝑎 ‘ 𝑏 ) ↑ 𝑛 ) = 1 )
46 1 2 abvcl ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ‘ 𝑏 ) ∈ ℝ )
47 32 33 46 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑏 ) = ( 1r ‘ 𝑅 ) ) ) → ( 𝑎 ‘ 𝑏 ) ∈ ℝ )
48 1 2 abvge0 ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → 0 ≤ ( 𝑎 ‘ 𝑏 ) )
49 32 33 48 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑏 ) = ( 1r ‘ 𝑅 ) ) ) → 0 ≤ ( 𝑎 ‘ 𝑏 ) )
50 47 34 49 expeq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑏 ) = ( 1r ‘ 𝑅 ) ) ) → ( ( ( 𝑎 ‘ 𝑏 ) ↑ 𝑛 ) = 1 ↔ ( 𝑎 ‘ 𝑏 ) = 1 ) )
51 45 50 mpbid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑏 ) = ( 1r ‘ 𝑅 ) ) ) → ( 𝑎 ‘ 𝑏 ) = 1 )
52 26 51 rexlimddv ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) → ( 𝑎 ‘ 𝑏 ) = 1 )
53 eqeq1 ⊢ ( 𝑥 = 𝑏 → ( 𝑥 = 0 ↔ 𝑏 = 0 ) )
54 53 ifbid ⊢ ( 𝑥 = 𝑏 → if ( 𝑥 = 0 , 0 , 1 ) = if ( 𝑏 = 0 , 0 , 1 ) )
55 ifnefalse ⊢ ( 𝑏 ≠ 0 → if ( 𝑏 = 0 , 0 , 1 ) = 1 )
56 55 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) → if ( 𝑏 = 0 , 0 , 1 ) = 1 )
57 54 56 sylan9eqr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) ∧ 𝑥 = 𝑏 ) → if ( 𝑥 = 0 , 0 , 1 ) = 1 )
58 simplr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) → 𝑏 ∈ 𝐵 )
59 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) → 1 ∈ ℂ )
60 4 57 58 59 fvmptd2 ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) → ( 𝑇 ‘ 𝑏 ) = 1 )
61 60 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) → ( 𝑇 ‘ 𝑏 ) = 1 )
62 52 61 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 ≠ 0 ) → ( 𝑎 ‘ 𝑏 ) = ( 𝑇 ‘ 𝑏 ) )
63 1 3 abv0 ⊢ ( 𝑎 ∈ 𝐴 → ( 𝑎 ‘ 0 ) = 0 )
64 63 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑎 ‘ 0 ) = 0 )
65 1 3 abv0 ⊢ ( 𝑇 ∈ 𝐴 → ( 𝑇 ‘ 0 ) = 0 )
66 11 65 syl ⊢ ( 𝜑 → ( 𝑇 ‘ 0 ) = 0 )
67 66 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑇 ‘ 0 ) = 0 )
68 64 67 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑎 ‘ 0 ) = ( 𝑇 ‘ 0 ) )
69 68 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ‘ 0 ) = ( 𝑇 ‘ 0 ) )
70 18 62 69 pm2.61ne ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ‘ 𝑏 ) = ( 𝑇 ‘ 𝑏 ) )
71 9 15 70 eqfnfvd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑎 = 𝑇 )
72 71 11 eqsnd ⊢ ( 𝜑 → 𝐴 = { 𝑇 } )