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 
|- A = ( AbsVal ` R )
fiabv.b 
|- B = ( Base ` R )
fiabv.0 
|- .0. = ( 0g ` R )
fiabv.t 
|- T = ( x e. B |-> if ( x = .0. , 0 , 1 ) )
fiabv.r 
|- ( ph -> R e. Domn )
fiabv.f 
|- ( ph -> B e. Fin )
Assertion fiabv 
|- ( ph -> A = { T } )

Proof

Step Hyp Ref Expression
1 fiabv.a 
 |-  A = ( AbsVal ` R )
2 fiabv.b 
 |-  B = ( Base ` R )
3 fiabv.0 
 |-  .0. = ( 0g ` R )
4 fiabv.t 
 |-  T = ( x e. B |-> if ( x = .0. , 0 , 1 ) )
5 fiabv.r 
 |-  ( ph -> R e. Domn )
6 fiabv.f 
 |-  ( ph -> B e. Fin )
7 1 2 abvf 
 |-  ( a e. A -> a : B --> RR )
8 7 ffnd 
 |-  ( a e. A -> a Fn B )
9 8 adantl 
 |-  ( ( ph /\ a e. A ) -> a Fn B )
10 1 2 3 4 abvtrivg 
 |-  ( R e. Domn -> T e. A )
11 5 10 syl 
 |-  ( ph -> T e. A )
12 1 2 abvf 
 |-  ( T e. A -> T : B --> RR )
13 11 12 syl 
 |-  ( ph -> T : B --> RR )
14 13 ffnd 
 |-  ( ph -> T Fn B )
15 14 adantr 
 |-  ( ( ph /\ a e. A ) -> T Fn B )
16 fveq2 
 |-  ( b = .0. -> ( a ` b ) = ( a ` .0. ) )
17 fveq2 
 |-  ( b = .0. -> ( T ` b ) = ( T ` .0. ) )
18 16 17 eqeq12d 
 |-  ( b = .0. -> ( ( a ` b ) = ( T ` b ) <-> ( a ` .0. ) = ( T ` .0. ) ) )
19 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
20 eqid 
 |-  ( .g ` ( mulGrp ` R ) ) = ( .g ` ( mulGrp ` R ) )
21 5 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. A ) /\ b e. B ) /\ b =/= .0. ) -> R e. Domn )
22 6 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. A ) /\ b e. B ) /\ b =/= .0. ) -> B e. Fin )
23 eldifsn 
 |-  ( b e. ( B \ { .0. } ) <-> ( b e. B /\ b =/= .0. ) )
24 23 biimpri 
 |-  ( ( b e. B /\ b =/= .0. ) -> b e. ( B \ { .0. } ) )
25 24 adantll 
 |-  ( ( ( ( ph /\ a e. A ) /\ b e. B ) /\ b =/= .0. ) -> b e. ( B \ { .0. } ) )
26 2 3 19 20 21 22 25 fidomncyc 
 |-  ( ( ( ( ph /\ a e. A ) /\ b e. B ) /\ b =/= .0. ) -> E. n e. NN ( n ( .g ` ( mulGrp ` R ) ) b ) = ( 1r ` R ) )
27 simprr 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. B ) /\ b =/= .0. ) /\ ( n e. NN /\ ( n ( .g ` ( mulGrp ` R ) ) b ) = ( 1r ` R ) ) ) -> ( n ( .g ` ( mulGrp ` R ) ) b ) = ( 1r ` R ) )
28 27 fveq2d 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. B ) /\ b =/= .0. ) /\ ( n e. NN /\ ( n ( .g ` ( mulGrp ` R ) ) b ) = ( 1r ` R ) ) ) -> ( a ` ( n ( .g ` ( mulGrp ` R ) ) b ) ) = ( a ` ( 1r ` R ) ) )
29 domnnzr 
 |-  ( R e. Domn -> R e. NzRing )
30 5 29 syl 
 |-  ( ph -> R e. NzRing )
31 30 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. B ) /\ b =/= .0. ) /\ ( n e. NN /\ ( n ( .g ` ( mulGrp ` R ) ) b ) = ( 1r ` R ) ) ) -> R e. NzRing )
32 simp-4r 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. B ) /\ b =/= .0. ) /\ ( n e. NN /\ ( n ( .g ` ( mulGrp ` R ) ) b ) = ( 1r ` R ) ) ) -> a e. A )
33 simpllr 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. B ) /\ b =/= .0. ) /\ ( n e. NN /\ ( n ( .g ` ( mulGrp ` R ) ) b ) = ( 1r ` R ) ) ) -> b e. B )
34 simprl 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. B ) /\ b =/= .0. ) /\ ( n e. NN /\ ( n ( .g ` ( mulGrp ` R ) ) b ) = ( 1r ` R ) ) ) -> n e. NN )
35 34 nnnn0d 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. B ) /\ b =/= .0. ) /\ ( n e. NN /\ ( n ( .g ` ( mulGrp ` R ) ) b ) = ( 1r ` R ) ) ) -> n e. NN0 )
36 1 20 2 31 32 33 35 abvexp 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. B ) /\ b =/= .0. ) /\ ( n e. NN /\ ( n ( .g ` ( mulGrp ` R ) ) b ) = ( 1r ` R ) ) ) -> ( a ` ( n ( .g ` ( mulGrp ` R ) ) b ) ) = ( ( a ` b ) ^ n ) )
37 simpr 
 |-  ( ( ph /\ a e. A ) -> a e. A )
38 19 3 nzrnz 
 |-  ( R e. NzRing -> ( 1r ` R ) =/= .0. )
39 29 38 syl 
 |-  ( R e. Domn -> ( 1r ` R ) =/= .0. )
40 5 39 syl 
 |-  ( ph -> ( 1r ` R ) =/= .0. )
41 40 adantr 
 |-  ( ( ph /\ a e. A ) -> ( 1r ` R ) =/= .0. )
42 1 19 3 abv1z 
 |-  ( ( a e. A /\ ( 1r ` R ) =/= .0. ) -> ( a ` ( 1r ` R ) ) = 1 )
43 37 41 42 syl2anc 
 |-  ( ( ph /\ a e. A ) -> ( a ` ( 1r ` R ) ) = 1 )
44 43 ad3antrrr 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. B ) /\ b =/= .0. ) /\ ( n e. NN /\ ( n ( .g ` ( mulGrp ` R ) ) b ) = ( 1r ` R ) ) ) -> ( a ` ( 1r ` R ) ) = 1 )
45 28 36 44 3eqtr3d 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. B ) /\ b =/= .0. ) /\ ( n e. NN /\ ( n ( .g ` ( mulGrp ` R ) ) b ) = ( 1r ` R ) ) ) -> ( ( a ` b ) ^ n ) = 1 )
46 1 2 abvcl 
 |-  ( ( a e. A /\ b e. B ) -> ( a ` b ) e. RR )
47 32 33 46 syl2anc 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. B ) /\ b =/= .0. ) /\ ( n e. NN /\ ( n ( .g ` ( mulGrp ` R ) ) b ) = ( 1r ` R ) ) ) -> ( a ` b ) e. RR )
48 1 2 abvge0 
 |-  ( ( a e. A /\ b e. B ) -> 0 <_ ( a ` b ) )
49 32 33 48 syl2anc 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. B ) /\ b =/= .0. ) /\ ( n e. NN /\ ( n ( .g ` ( mulGrp ` R ) ) b ) = ( 1r ` R ) ) ) -> 0 <_ ( a ` b ) )
50 47 34 49 expeq1d 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. B ) /\ b =/= .0. ) /\ ( n e. NN /\ ( n ( .g ` ( mulGrp ` R ) ) b ) = ( 1r ` R ) ) ) -> ( ( ( a ` b ) ^ n ) = 1 <-> ( a ` b ) = 1 ) )
51 45 50 mpbid 
 |-  ( ( ( ( ( ph /\ a e. A ) /\ b e. B ) /\ b =/= .0. ) /\ ( n e. NN /\ ( n ( .g ` ( mulGrp ` R ) ) b ) = ( 1r ` R ) ) ) -> ( a ` b ) = 1 )
52 26 51 rexlimddv 
 |-  ( ( ( ( ph /\ a e. A ) /\ b e. B ) /\ b =/= .0. ) -> ( a ` b ) = 1 )
53 eqeq1 
 |-  ( x = b -> ( x = .0. <-> b = .0. ) )
54 53 ifbid 
 |-  ( x = b -> if ( x = .0. , 0 , 1 ) = if ( b = .0. , 0 , 1 ) )
55 ifnefalse 
 |-  ( b =/= .0. -> if ( b = .0. , 0 , 1 ) = 1 )
56 55 adantl 
 |-  ( ( ( ph /\ b e. B ) /\ b =/= .0. ) -> if ( b = .0. , 0 , 1 ) = 1 )
57 54 56 sylan9eqr 
 |-  ( ( ( ( ph /\ b e. B ) /\ b =/= .0. ) /\ x = b ) -> if ( x = .0. , 0 , 1 ) = 1 )
58 simplr 
 |-  ( ( ( ph /\ b e. B ) /\ b =/= .0. ) -> b e. B )
59 1cnd 
 |-  ( ( ( ph /\ b e. B ) /\ b =/= .0. ) -> 1 e. CC )
60 4 57 58 59 fvmptd2 
 |-  ( ( ( ph /\ b e. B ) /\ b =/= .0. ) -> ( T ` b ) = 1 )
61 60 adantllr 
 |-  ( ( ( ( ph /\ a e. A ) /\ b e. B ) /\ b =/= .0. ) -> ( T ` b ) = 1 )
62 52 61 eqtr4d 
 |-  ( ( ( ( ph /\ a e. A ) /\ b e. B ) /\ b =/= .0. ) -> ( a ` b ) = ( T ` b ) )
63 1 3 abv0 
 |-  ( a e. A -> ( a ` .0. ) = 0 )
64 63 adantl 
 |-  ( ( ph /\ a e. A ) -> ( a ` .0. ) = 0 )
65 1 3 abv0 
 |-  ( T e. A -> ( T ` .0. ) = 0 )
66 11 65 syl 
 |-  ( ph -> ( T ` .0. ) = 0 )
67 66 adantr 
 |-  ( ( ph /\ a e. A ) -> ( T ` .0. ) = 0 )
68 64 67 eqtr4d 
 |-  ( ( ph /\ a e. A ) -> ( a ` .0. ) = ( T ` .0. ) )
69 68 adantr 
 |-  ( ( ( ph /\ a e. A ) /\ b e. B ) -> ( a ` .0. ) = ( T ` .0. ) )
70 18 62 69 pm2.61ne 
 |-  ( ( ( ph /\ a e. A ) /\ b e. B ) -> ( a ` b ) = ( T ` b ) )
71 9 15 70 eqfnfvd 
 |-  ( ( ph /\ a e. A ) -> a = T )
72 71 11 eqsnd 
 |-  ( ph -> A = { T } )