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	$⊢ \underset{˙}{0} = 0_{R}$
	fiabv.t	$⊢ T = (x \in B ⟼ if (x = \underset{˙}{0}, 0, 1))$
	fiabv.r	$⊢ φ \to R \in Domn$
	fiabv.f	$⊢ φ \to B \in Fin$
Assertion	fiabv	$⊢ φ \to A = \{T\}$

Proof

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

Metamath Proof Explorer

Theorem fiabv

Proof