Theorem abv1z

Description: The absolute value of one is one in a non-trivial ring. (Contributed by Mario Carneiro, 8-Sep-2014)

	Ref	Expression
Hypotheses	abv0.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
	abv1.p	$$⊢\underset{\dot{}}{1}=1_R$$
	abv1z.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	abv1z	$$⊢\left(F\in A\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\to F\left(\underset{\dot{}}{1}\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		abv0.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
2		abv1.p	$$⊢\underset{\dot{}}{1}=1_R$$
3		abv1z.z	$$⊢\underset{\dot{}}{0}=0_R$$
4	1	abvrcl	$$⊢F\in A\to R\in \mathrm{Ring}$$
5		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
6	5 2	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
7	4 6	syl	$$⊢F\in A\to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
8	1 5	abvcl	$$⊢\left(F\in A\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_R\right)\to F\left(\underset{\dot{}}{1}\right)\in ℝ$$
9	7 8	mpdan	$$⊢F\in A\to F\left(\underset{\dot{}}{1}\right)\in ℝ$$
10	9	adantr	$$⊢\left(F\in A\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\to F\left(\underset{\dot{}}{1}\right)\in ℝ$$
11	10	recnd	$$⊢\left(F\in A\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\to F\left(\underset{\dot{}}{1}\right)\in ℂ$$
12		simpl	$$⊢\left(F\in A\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\to F\in A$$
13	7	adantr	$$⊢\left(F\in A\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
14		simpr	$$⊢\left(F\in A\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\to \underset{\dot{}}{1}\ne \underset{\dot{}}{0}$$
15	1 5 3	abvne0	$$⊢\left(F\in A\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_R\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\to F\left(\underset{\dot{}}{1}\right)\ne 0$$
16	12 13 14 15	syl3anc	$$⊢\left(F\in A\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\to F\left(\underset{\dot{}}{1}\right)\ne 0$$
17	11 11 16	divcan3d	$$⊢\left(F\in A\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\to \frac{F\left(\underset{\dot{}}{1}\right)F\left(\underset{\dot{}}{1}\right)}{F\left(\underset{\dot{}}{1}\right)}=F\left(\underset{\dot{}}{1}\right)$$
18		eqid	$$⊢{\cdot }_R={\cdot }_R$$
19	5 18 2	ringlidm	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_R\right)\to \underset{\dot{}}{1}{\cdot }_R\underset{\dot{}}{1}=\underset{\dot{}}{1}$$
20	4 13 19	syl2an2r	$$⊢\left(F\in A\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\to \underset{\dot{}}{1}{\cdot }_R\underset{\dot{}}{1}=\underset{\dot{}}{1}$$
21	20	fveq2d	$$⊢\left(F\in A\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\to F\left(\underset{\dot{}}{1}{\cdot }_R\underset{\dot{}}{1}\right)=F\left(\underset{\dot{}}{1}\right)$$
22	1 5 18	abvmul	$$⊢\left(F\in A\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_R\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_R\right)\to F\left(\underset{\dot{}}{1}{\cdot }_R\underset{\dot{}}{1}\right)=F\left(\underset{\dot{}}{1}\right)F\left(\underset{\dot{}}{1}\right)$$
23	12 13 13 22	syl3anc	$$⊢\left(F\in A\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\to F\left(\underset{\dot{}}{1}{\cdot }_R\underset{\dot{}}{1}\right)=F\left(\underset{\dot{}}{1}\right)F\left(\underset{\dot{}}{1}\right)$$
24	21 23	eqtr3d	$$⊢\left(F\in A\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\to F\left(\underset{\dot{}}{1}\right)=F\left(\underset{\dot{}}{1}\right)F\left(\underset{\dot{}}{1}\right)$$
25	24	oveq1d	$$⊢\left(F\in A\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\to \frac{F\left(\underset{\dot{}}{1}\right)}{F\left(\underset{\dot{}}{1}\right)}=\frac{F\left(\underset{\dot{}}{1}\right)F\left(\underset{\dot{}}{1}\right)}{F\left(\underset{\dot{}}{1}\right)}$$
26	11 16	dividd	$$⊢\left(F\in A\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\to \frac{F\left(\underset{\dot{}}{1}\right)}{F\left(\underset{\dot{}}{1}\right)}=1$$
27	25 26	eqtr3d	$$⊢\left(F\in A\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\to \frac{F\left(\underset{\dot{}}{1}\right)F\left(\underset{\dot{}}{1}\right)}{F\left(\underset{\dot{}}{1}\right)}=1$$
28	17 27	eqtr3d	$$⊢\left(F\in A\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\to F\left(\underset{\dot{}}{1}\right)=1$$