Theorem abvtrivd

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

	Ref	Expression
Hypotheses	abvtriv.a	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
	abvtriv.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	abvtriv.z	⊢ 0 = ( 0g ‘ 𝑅 )
	abvtriv.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 = 0 , 0 , 1 ) )
	abvtrivd.1	⊢ · = ( .r ‘ 𝑅 )
	abvtrivd.2	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	abvtrivd.3	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑦 · 𝑧 ) ≠ 0 )
Assertion	abvtrivd	⊢ ( 𝜑 → 𝐹 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		abvtriv.a	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
2		abvtriv.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		abvtriv.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		abvtriv.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 = 0 , 0 , 1 ) )
5		abvtrivd.1	⊢ · = ( .r ‘ 𝑅 )
6		abvtrivd.2	⊢ ( 𝜑 → 𝑅 ∈ Ring )
7		abvtrivd.3	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑦 · 𝑧 ) ≠ 0 )
8	1	a1i	⊢ ( 𝜑 → 𝐴 = ( AbsVal ‘ 𝑅 ) )
9	2	a1i	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
10		eqidd	⊢ ( 𝜑 → ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 ) )
11	5	a1i	⊢ ( 𝜑 → · = ( .r ‘ 𝑅 ) )
12	3	a1i	⊢ ( 𝜑 → 0 = ( 0g ‘ 𝑅 ) )
13		0re	⊢ 0 ∈ ℝ
14		1re	⊢ 1 ∈ ℝ
15	13 14	ifcli	⊢ if ( 𝑥 = 0 , 0 , 1 ) ∈ ℝ
16	15	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → if ( 𝑥 = 0 , 0 , 1 ) ∈ ℝ )
17	16 4	fmptd	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ℝ )
18	2 3	ring0cl	⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐵 )
19		iftrue	⊢ ( 𝑥 = 0 → if ( 𝑥 = 0 , 0 , 1 ) = 0 )
20		c0ex	⊢ 0 ∈ V
21	19 4 20	fvmpt	⊢ ( 0 ∈ 𝐵 → ( 𝐹 ‘ 0 ) = 0 )
22	6 18 21	3syl	⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = 0 )
23		0lt1	⊢ 0 < 1
24		eqeq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 0 ↔ 𝑦 = 0 ) )
25	24	ifbid	⊢ ( 𝑥 = 𝑦 → if ( 𝑥 = 0 , 0 , 1 ) = if ( 𝑦 = 0 , 0 , 1 ) )
26		1ex	⊢ 1 ∈ V
27	20 26	ifex	⊢ if ( 𝑦 = 0 , 0 , 1 ) ∈ V
28	25 4 27	fvmpt	⊢ ( 𝑦 ∈ 𝐵 → ( 𝐹 ‘ 𝑦 ) = if ( 𝑦 = 0 , 0 , 1 ) )
29		ifnefalse	⊢ ( 𝑦 ≠ 0 → if ( 𝑦 = 0 , 0 , 1 ) = 1 )
30	28 29	sylan9eq	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) → ( 𝐹 ‘ 𝑦 ) = 1 )
31	30	3adant1	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) → ( 𝐹 ‘ 𝑦 ) = 1 )
32	23 31	breqtrrid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) → 0 < ( 𝐹 ‘ 𝑦 ) )
33		1t1e1	⊢ ( 1 · 1 ) = 1
34	33	eqcomi	⊢ 1 = ( 1 · 1 )
35	6	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → 𝑅 ∈ Ring )
36		simp2l	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → 𝑦 ∈ 𝐵 )
37		simp3l	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → 𝑧 ∈ 𝐵 )
38	2 5	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 · 𝑧 ) ∈ 𝐵 )
39	35 36 37 38	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑦 · 𝑧 ) ∈ 𝐵 )
40		eqeq1	⊢ ( 𝑥 = ( 𝑦 · 𝑧 ) → ( 𝑥 = 0 ↔ ( 𝑦 · 𝑧 ) = 0 ) )
41	40	ifbid	⊢ ( 𝑥 = ( 𝑦 · 𝑧 ) → if ( 𝑥 = 0 , 0 , 1 ) = if ( ( 𝑦 · 𝑧 ) = 0 , 0 , 1 ) )
42	20 26	ifex	⊢ if ( ( 𝑦 · 𝑧 ) = 0 , 0 , 1 ) ∈ V
43	41 4 42	fvmpt	⊢ ( ( 𝑦 · 𝑧 ) ∈ 𝐵 → ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = if ( ( 𝑦 · 𝑧 ) = 0 , 0 , 1 ) )
44	39 43	syl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = if ( ( 𝑦 · 𝑧 ) = 0 , 0 , 1 ) )
45	7	neneqd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ¬ ( 𝑦 · 𝑧 ) = 0 )
46	45	iffalsed	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → if ( ( 𝑦 · 𝑧 ) = 0 , 0 , 1 ) = 1 )
47	44 46	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = 1 )
48	36 28	syl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ 𝑦 ) = if ( 𝑦 = 0 , 0 , 1 ) )
49		simp2r	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → 𝑦 ≠ 0 )
50	49	neneqd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ¬ 𝑦 = 0 )
51	50	iffalsed	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → if ( 𝑦 = 0 , 0 , 1 ) = 1 )
52	48 51	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ 𝑦 ) = 1 )
53		eqeq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 0 ↔ 𝑧 = 0 ) )
54	53	ifbid	⊢ ( 𝑥 = 𝑧 → if ( 𝑥 = 0 , 0 , 1 ) = if ( 𝑧 = 0 , 0 , 1 ) )
55	20 26	ifex	⊢ if ( 𝑧 = 0 , 0 , 1 ) ∈ V
56	54 4 55	fvmpt	⊢ ( 𝑧 ∈ 𝐵 → ( 𝐹 ‘ 𝑧 ) = if ( 𝑧 = 0 , 0 , 1 ) )
57	37 56	syl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ 𝑧 ) = if ( 𝑧 = 0 , 0 , 1 ) )
58		simp3r	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → 𝑧 ≠ 0 )
59	58	neneqd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ¬ 𝑧 = 0 )
60	59	iffalsed	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → if ( 𝑧 = 0 , 0 , 1 ) = 1 )
61	57 60	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ 𝑧 ) = 1 )
62	52 61	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( ( 𝐹 ‘ 𝑦 ) · ( 𝐹 ‘ 𝑧 ) ) = ( 1 · 1 ) )
63	34 47 62	3eqtr4a	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = ( ( 𝐹 ‘ 𝑦 ) · ( 𝐹 ‘ 𝑧 ) ) )
64		breq1	⊢ ( 0 = if ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = 0 , 0 , 1 ) → ( 0 ≤ 2 ↔ if ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = 0 , 0 , 1 ) ≤ 2 ) )
65		breq1	⊢ ( 1 = if ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = 0 , 0 , 1 ) → ( 1 ≤ 2 ↔ if ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = 0 , 0 , 1 ) ≤ 2 ) )
66		0le2	⊢ 0 ≤ 2
67		1le2	⊢ 1 ≤ 2
68	64 65 66 67	keephyp	⊢ if ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = 0 , 0 , 1 ) ≤ 2
69		df-2	⊢ 2 = ( 1 + 1 )
70	68 69	breqtri	⊢ if ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = 0 , 0 , 1 ) ≤ ( 1 + 1 )
71	70	a1i	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → if ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = 0 , 0 , 1 ) ≤ ( 1 + 1 ) )
72		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
73	6 72	syl	⊢ ( 𝜑 → 𝑅 ∈ Grp )
74	73	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → 𝑅 ∈ Grp )
75		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
76	2 75	grpcl	⊢ ( ( 𝑅 ∈ Grp ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐵 )
77	74 36 37 76	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐵 )
78		eqeq1	⊢ ( 𝑥 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) → ( 𝑥 = 0 ↔ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = 0 ) )
79	78	ifbid	⊢ ( 𝑥 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) → if ( 𝑥 = 0 , 0 , 1 ) = if ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = 0 , 0 , 1 ) )
80	20 26	ifex	⊢ if ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = 0 , 0 , 1 ) ∈ V
81	79 4 80	fvmpt	⊢ ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐵 → ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) = if ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = 0 , 0 , 1 ) )
82	77 81	syl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) = if ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = 0 , 0 , 1 ) )
83	52 61	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( ( 𝐹 ‘ 𝑦 ) + ( 𝐹 ‘ 𝑧 ) ) = ( 1 + 1 ) )
84	71 82 83	3brtr4d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) ≤ ( ( 𝐹 ‘ 𝑦 ) + ( 𝐹 ‘ 𝑧 ) ) )
85	8 9 10 11 12 6 17 22 32 63 84	isabvd	⊢ ( 𝜑 → 𝐹 ∈ 𝐴 )