Theorem abvtrivd

Description: The trivial absolute value. (Contributed by Mario Carneiro, 6-May-2015)

	Ref	Expression
Hypotheses	abvtriv.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
	abvtriv.b	$$⊢B={\mathrm{Base}}_R$$
	abvtriv.z	$$⊢\underset{\dot{}}{0}=0_R$$
	abvtriv.f	$$⊢F=\left(x\in B⟼if\left(x=\underset{\dot{}}{0},0,1\right)\right)$$
	abvtrivd.1	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	abvtrivd.2	$$⊢\phi \to R\in \mathrm{Ring}$$
	abvtrivd.3	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to y\underset{\dot{}}{·}z\ne \underset{\dot{}}{0}$$
Assertion	abvtrivd	$$⊢\phi \to F\in A$$

Proof

Step	Hyp	Ref	Expression
1		abvtriv.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
2		abvtriv.b	$$⊢B={\mathrm{Base}}_R$$
3		abvtriv.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		abvtriv.f	$$⊢F=\left(x\in B⟼if\left(x=\underset{\dot{}}{0},0,1\right)\right)$$
5		abvtrivd.1	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
6		abvtrivd.2	$$⊢\phi \to R\in \mathrm{Ring}$$
7		abvtrivd.3	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to y\underset{\dot{}}{·}z\ne \underset{\dot{}}{0}$$
8	1	a1i	$$⊢\phi \to A=\mathrm{AbsVal}\left(R\right)$$
9	2	a1i	$$⊢\phi \to B={\mathrm{Base}}_R$$
10		eqidd	$$⊢\phi \to {+}_R={+}_R$$
11	5	a1i	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_R$$
12	3	a1i	$$⊢\phi \to \underset{\dot{}}{0}=0_R$$
13		0re	$$⊢0\in ℝ$$
14		1re	$$⊢1\in ℝ$$
15	13 14	ifcli	$$⊢if\left(x=\underset{\dot{}}{0},0,1\right)\in ℝ$$
16	15	a1i	$$⊢\left(\phi \wedge x\in B\right)\to if\left(x=\underset{\dot{}}{0},0,1\right)\in ℝ$$
17	16 4	fmptd	$$⊢\phi \to F:B⟶ℝ$$
18	2 3	ring0cl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\in B$$
19		iftrue	$$⊢x=\underset{\dot{}}{0}\to if\left(x=\underset{\dot{}}{0},0,1\right)=0$$
20		c0ex	$$⊢0\in \mathrm{V}$$
21	19 4 20	fvmpt	$$⊢\underset{\dot{}}{0}\in B\to F\left(\underset{\dot{}}{0}\right)=0$$
22	6 18 21	3syl	$$⊢\phi \to F\left(\underset{\dot{}}{0}\right)=0$$
23		0lt1	$$⊢0<1$$
24		eqeq1	$$⊢x=y\to \left(x=\underset{\dot{}}{0}\leftrightarrow y=\underset{\dot{}}{0}\right)$$
25	24	ifbid	$$⊢x=y\to if\left(x=\underset{\dot{}}{0},0,1\right)=if\left(y=\underset{\dot{}}{0},0,1\right)$$
26		1ex	$$⊢1\in \mathrm{V}$$
27	20 26	ifex	$$⊢if\left(y=\underset{\dot{}}{0},0,1\right)\in \mathrm{V}$$
28	25 4 27	fvmpt	$$⊢y\in B\to F\left(y\right)=if\left(y=\underset{\dot{}}{0},0,1\right)$$
29		ifnefalse	$$⊢y\ne \underset{\dot{}}{0}\to if\left(y=\underset{\dot{}}{0},0,1\right)=1$$
30	28 29	sylan9eq	$$⊢\left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\to F\left(y\right)=1$$
31	30	3adant1	$$⊢\left(\phi \wedge y\in B\wedge y\ne \underset{\dot{}}{0}\right)\to F\left(y\right)=1$$
32	23 31	breqtrrid	$$⊢\left(\phi \wedge y\in B\wedge y\ne \underset{\dot{}}{0}\right)\to 0<F\left(y\right)$$
33		1t1e1	$$⊢1\cdot 1=1$$
34	33	eqcomi	$$⊢1=1\cdot 1$$
35	6	3ad2ant1	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to R\in \mathrm{Ring}$$
36		simp2l	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to y\in B$$
37		simp3l	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to z\in B$$
38	2 5	ringcl	$$⊢\left(R\in \mathrm{Ring}\wedge y\in B\wedge z\in B\right)\to y\underset{\dot{}}{·}z\in B$$
39	35 36 37 38	syl3anc	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to y\underset{\dot{}}{·}z\in B$$
40		eqeq1	$$⊢x=y\underset{\dot{}}{·}z\to \left(x=\underset{\dot{}}{0}\leftrightarrow y\underset{\dot{}}{·}z=\underset{\dot{}}{0}\right)$$
41	40	ifbid	$$⊢x=y\underset{\dot{}}{·}z\to if\left(x=\underset{\dot{}}{0},0,1\right)=if\left(y\underset{\dot{}}{·}z=\underset{\dot{}}{0},0,1\right)$$
42	20 26	ifex	$$⊢if\left(y\underset{\dot{}}{·}z=\underset{\dot{}}{0},0,1\right)\in \mathrm{V}$$
43	41 4 42	fvmpt	$$⊢y\underset{\dot{}}{·}z\in B\to F\left(y\underset{\dot{}}{·}z\right)=if\left(y\underset{\dot{}}{·}z=\underset{\dot{}}{0},0,1\right)$$
44	39 43	syl	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to F\left(y\underset{\dot{}}{·}z\right)=if\left(y\underset{\dot{}}{·}z=\underset{\dot{}}{0},0,1\right)$$
45	7	neneqd	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to \neg y\underset{\dot{}}{·}z=\underset{\dot{}}{0}$$
46	45	iffalsed	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to if\left(y\underset{\dot{}}{·}z=\underset{\dot{}}{0},0,1\right)=1$$
47	44 46	eqtrd	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to F\left(y\underset{\dot{}}{·}z\right)=1$$
48	36 28	syl	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to F\left(y\right)=if\left(y=\underset{\dot{}}{0},0,1\right)$$
49		simp2r	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to y\ne \underset{\dot{}}{0}$$
50	49	neneqd	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to \neg y=\underset{\dot{}}{0}$$
51	50	iffalsed	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to if\left(y=\underset{\dot{}}{0},0,1\right)=1$$
52	48 51	eqtrd	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to F\left(y\right)=1$$
53		eqeq1	$$⊢x=z\to \left(x=\underset{\dot{}}{0}\leftrightarrow z=\underset{\dot{}}{0}\right)$$
54	53	ifbid	$$⊢x=z\to if\left(x=\underset{\dot{}}{0},0,1\right)=if\left(z=\underset{\dot{}}{0},0,1\right)$$
55	20 26	ifex	$$⊢if\left(z=\underset{\dot{}}{0},0,1\right)\in \mathrm{V}$$
56	54 4 55	fvmpt	$$⊢z\in B\to F\left(z\right)=if\left(z=\underset{\dot{}}{0},0,1\right)$$
57	37 56	syl	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to F\left(z\right)=if\left(z=\underset{\dot{}}{0},0,1\right)$$
58		simp3r	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to z\ne \underset{\dot{}}{0}$$
59	58	neneqd	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to \neg z=\underset{\dot{}}{0}$$
60	59	iffalsed	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to if\left(z=\underset{\dot{}}{0},0,1\right)=1$$
61	57 60	eqtrd	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to F\left(z\right)=1$$
62	52 61	oveq12d	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to F\left(y\right)F\left(z\right)=1\cdot 1$$
63	34 47 62	3eqtr4a	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to F\left(y\underset{\dot{}}{·}z\right)=F\left(y\right)F\left(z\right)$$
64		breq1	$$⊢0=if\left(y{+}_{R}z=\underset{\dot{}}{0},0,1\right)\to \left(0\le 2\leftrightarrow if\left(y{+}_{R}z=\underset{\dot{}}{0},0,1\right)\le 2\right)$$
65		breq1	$$⊢1=if\left(y{+}_{R}z=\underset{\dot{}}{0},0,1\right)\to \left(1\le 2\leftrightarrow if\left(y{+}_{R}z=\underset{\dot{}}{0},0,1\right)\le 2\right)$$
66		0le2	$$⊢0\le 2$$
67		1le2	$$⊢1\le 2$$
68	64 65 66 67	keephyp	$$⊢if\left(y{+}_{R}z=\underset{\dot{}}{0},0,1\right)\le 2$$
69		df-2	$$⊢2=1+1$$
70	68 69	breqtri	$$⊢if\left(y{+}_{R}z=\underset{\dot{}}{0},0,1\right)\le 1+1$$
71	70	a1i	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to if\left(y{+}_{R}z=\underset{\dot{}}{0},0,1\right)\le 1+1$$
72		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
73	6 72	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
74	73	3ad2ant1	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to R\in \mathrm{Grp}$$
75		eqid	$$⊢{+}_R={+}_R$$
76	2 75	grpcl	$$⊢\left(R\in \mathrm{Grp}\wedge y\in B\wedge z\in B\right)\to y{+}_{R}z\in B$$
77	74 36 37 76	syl3anc	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to y{+}_{R}z\in B$$
78		eqeq1	$$⊢x=y{+}_{R}z\to \left(x=\underset{\dot{}}{0}\leftrightarrow y{+}_{R}z=\underset{\dot{}}{0}\right)$$
79	78	ifbid	$$⊢x=y{+}_{R}z\to if\left(x=\underset{\dot{}}{0},0,1\right)=if\left(y{+}_{R}z=\underset{\dot{}}{0},0,1\right)$$
80	20 26	ifex	$$⊢if\left(y{+}_{R}z=\underset{\dot{}}{0},0,1\right)\in \mathrm{V}$$
81	79 4 80	fvmpt	$$⊢y{+}_{R}z\in B\to F\left(y{+}_{R}z\right)=if\left(y{+}_{R}z=\underset{\dot{}}{0},0,1\right)$$
82	77 81	syl	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to F\left(y{+}_{R}z\right)=if\left(y{+}_{R}z=\underset{\dot{}}{0},0,1\right)$$
83	52 61	oveq12d	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to F\left(y\right)+F\left(z\right)=1+1$$
84	71 82 83	3brtr4d	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to F\left(y{+}_{R}z\right)\le F\left(y\right)+F\left(z\right)$$
85	8 9 10 11 12 6 17 22 32 63 84	isabvd	$$⊢\phi \to F\in A$$