abvtrivd

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

	Ref	Expression
Hypotheses	abvtriv.a	$⊢ A = AbsVal (R)$
	abvtriv.b	$⊢ B = {Base}_{R}$
	abvtriv.z	$⊢ \underset{˙}{0} = 0_{R}$
	abvtriv.f	$⊢ F = (x \in B ⟼ if (x = \underset{˙}{0}, 0, 1))$
	abvtrivd.1	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	abvtrivd.2	$⊢ φ \to R \in Ring$
	abvtrivd.3	$⊢ (φ \land (y \in B \land y \neq \underset{˙}{0}) \land (z \in B \land z \neq \underset{˙}{0})) \to y \underset{˙}{\cdot} z \neq \underset{˙}{0}$
Assertion	abvtrivd	$⊢ φ \to F \in A$

Proof

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

Metamath Proof Explorer

Theorem abvtrivd

Proof