isabvd

Description: Properties that determine an absolute value. (Contributed by Mario Carneiro, 8-Sep-2014) (Revised by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	isabvd.a	$⊢ φ \to A = AbsVal (R)$
	isabvd.b	$⊢ φ \to B = {Base}_{R}$
	isabvd.p	$⊢ φ \to \underset{˙}{+} = +_{R}$
	isabvd.t	$⊢ φ \to \underset{˙}{\cdot} = \cdot_{R}$
	isabvd.z	$⊢ φ \to \underset{˙}{0} = 0_{R}$
	isabvd.1	$⊢ φ \to R \in Ring$
	isabvd.2	$⊢ φ \to F : B ⟶ ℝ$
	isabvd.3	$⊢ φ \to F (\underset{˙}{0}) = 0$
	isabvd.4	$⊢ (φ \land x \in B \land x \neq \underset{˙}{0}) \to 0 < F (x)$
	isabvd.5	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0}) \land (y \in B \land y \neq \underset{˙}{0})) \to F (x \underset{˙}{\cdot} y) = F (x) F (y)$
	isabvd.6	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0}) \land (y \in B \land y \neq \underset{˙}{0})) \to F (x \underset{˙}{+} y) \leq F (x) + F (y)$
Assertion	isabvd	$⊢ φ \to F \in A$

Proof

Step	Hyp	Ref	Expression
1		isabvd.a	$⊢ φ \to A = AbsVal (R)$
2		isabvd.b	$⊢ φ \to B = {Base}_{R}$
3		isabvd.p	$⊢ φ \to \underset{˙}{+} = +_{R}$
4		isabvd.t	$⊢ φ \to \underset{˙}{\cdot} = \cdot_{R}$
5		isabvd.z	$⊢ φ \to \underset{˙}{0} = 0_{R}$
6		isabvd.1	$⊢ φ \to R \in Ring$
7		isabvd.2	$⊢ φ \to F : B ⟶ ℝ$
8		isabvd.3	$⊢ φ \to F (\underset{˙}{0}) = 0$
9		isabvd.4	$⊢ (φ \land x \in B \land x \neq \underset{˙}{0}) \to 0 < F (x)$
10		isabvd.5	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0}) \land (y \in B \land y \neq \underset{˙}{0})) \to F (x \underset{˙}{\cdot} y) = F (x) F (y)$
11		isabvd.6	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0}) \land (y \in B \land y \neq \underset{˙}{0})) \to F (x \underset{˙}{+} y) \leq F (x) + F (y)$
12	2	feq2d	$⊢ φ \to (F : B ⟶ ℝ \leftrightarrow F : {Base}_{R} ⟶ ℝ)$
13	7 12	mpbid	$⊢ φ \to F : {Base}_{R} ⟶ ℝ$
14	13	ffnd	$⊢ φ \to F Fn {Base}_{R}$
15	13	ffvelrnda	$⊢ (φ \land x \in {Base}_{R}) \to F (x) \in ℝ$
16		0le0	$⊢ 0 \leq 0$
17	5	fveq2d	$⊢ φ \to F (\underset{˙}{0}) = F (0_{R})$
18	17 8	eqtr3d	$⊢ φ \to F (0_{R}) = 0$
19	16 18	breqtrrid	$⊢ φ \to 0 \leq F (0_{R})$
20	19	adantr	$⊢ (φ \land x \in {Base}_{R}) \to 0 \leq F (0_{R})$
21		fveq2	$⊢ x = 0_{R} \to F (x) = F (0_{R})$
22	21	breq2d	$⊢ x = 0_{R} \to (0 \leq F (x) \leftrightarrow 0 \leq F (0_{R}))$
23	20 22	syl5ibrcom	$⊢ (φ \land x \in {Base}_{R}) \to (x = 0_{R} \to 0 \leq F (x))$
24		simp1	$⊢ (φ \land x \in {Base}_{R} \land x \neq 0_{R}) \to φ$
25		simp2	$⊢ (φ \land x \in {Base}_{R} \land x \neq 0_{R}) \to x \in {Base}_{R}$
26	2	3ad2ant1	$⊢ (φ \land x \in {Base}_{R} \land x \neq 0_{R}) \to B = {Base}_{R}$
27	25 26	eleqtrrd	$⊢ (φ \land x \in {Base}_{R} \land x \neq 0_{R}) \to x \in B$
28		simp3	$⊢ (φ \land x \in {Base}_{R} \land x \neq 0_{R}) \to x \neq 0_{R}$
29	5	3ad2ant1	$⊢ (φ \land x \in {Base}_{R} \land x \neq 0_{R}) \to \underset{˙}{0} = 0_{R}$
30	28 29	neeqtrrd	$⊢ (φ \land x \in {Base}_{R} \land x \neq 0_{R}) \to x \neq \underset{˙}{0}$
31	24 27 30 9	syl3anc	$⊢ (φ \land x \in {Base}_{R} \land x \neq 0_{R}) \to 0 < F (x)$
32		0re	$⊢ 0 \in ℝ$
33	15	3adant3	$⊢ (φ \land x \in {Base}_{R} \land x \neq 0_{R}) \to F (x) \in ℝ$
34		ltle	$⊢ (0 \in ℝ \land F (x) \in ℝ) \to (0 < F (x) \to 0 \leq F (x))$
35	32 33 34	sylancr	$⊢ (φ \land x \in {Base}_{R} \land x \neq 0_{R}) \to (0 < F (x) \to 0 \leq F (x))$
36	31 35	mpd	$⊢ (φ \land x \in {Base}_{R} \land x \neq 0_{R}) \to 0 \leq F (x)$
37	36	3expia	$⊢ (φ \land x \in {Base}_{R}) \to (x \neq 0_{R} \to 0 \leq F (x))$
38	23 37	pm2.61dne	$⊢ (φ \land x \in {Base}_{R}) \to 0 \leq F (x)$
39		elrege0	$⊢ F (x) \in [0, +∞) \leftrightarrow (F (x) \in ℝ \land 0 \leq F (x))$
40	15 38 39	sylanbrc	$⊢ (φ \land x \in {Base}_{R}) \to F (x) \in [0, +∞)$
41	40	ralrimiva	$⊢ φ \to \forall x \in {Base}_{R} F (x) \in [0, +∞)$
42		ffnfv	$⊢ F : {Base}_{R} ⟶ [0, +∞) \leftrightarrow (F Fn {Base}_{R} \land \forall x \in {Base}_{R} F (x) \in [0, +∞))$
43	14 41 42	sylanbrc	$⊢ φ \to F : {Base}_{R} ⟶ [0, +∞)$
44	31	gt0ne0d	$⊢ (φ \land x \in {Base}_{R} \land x \neq 0_{R}) \to F (x) \neq 0$
45	44	3expia	$⊢ (φ \land x \in {Base}_{R}) \to (x \neq 0_{R} \to F (x) \neq 0)$
46	45	necon4d	$⊢ (φ \land x \in {Base}_{R}) \to (F (x) = 0 \to x = 0_{R})$
47	18	adantr	$⊢ (φ \land x \in {Base}_{R}) \to F (0_{R}) = 0$
48		fveqeq2	$⊢ x = 0_{R} \to (F (x) = 0 \leftrightarrow F (0_{R}) = 0)$
49	47 48	syl5ibrcom	$⊢ (φ \land x \in {Base}_{R}) \to (x = 0_{R} \to F (x) = 0)$
50	46 49	impbid	$⊢ (φ \land x \in {Base}_{R}) \to (F (x) = 0 \leftrightarrow x = 0_{R})$
51	18	3ad2ant1	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \to F (0_{R}) = 0$
52	51	adantr	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land x = 0_{R}) \to F (0_{R}) = 0$
53		oveq1	$⊢ x = 0_{R} \to x \cdot_{R} y = 0_{R} \cdot_{R} y$
54	6	3ad2ant1	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \to R \in Ring$
55		simp3	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \to y \in {Base}_{R}$
56		eqid	$⊢ {Base}_{R} = {Base}_{R}$
57		eqid	$⊢ \cdot_{R} = \cdot_{R}$
58		eqid	$⊢ 0_{R} = 0_{R}$
59	56 57 58	ringlz	$⊢ (R \in Ring \land y \in {Base}_{R}) \to 0_{R} \cdot_{R} y = 0_{R}$
60	54 55 59	syl2anc	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \to 0_{R} \cdot_{R} y = 0_{R}$
61	53 60	sylan9eqr	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land x = 0_{R}) \to x \cdot_{R} y = 0_{R}$
62	61	fveq2d	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land x = 0_{R}) \to F (x \cdot_{R} y) = F (0_{R})$
63	21 51	sylan9eqr	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land x = 0_{R}) \to F (x) = 0$
64	63	oveq1d	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land x = 0_{R}) \to F (x) F (y) = 0 \cdot F (y)$
65	13	3ad2ant1	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \to F : {Base}_{R} ⟶ ℝ$
66	65 55	ffvelrnd	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \to F (y) \in ℝ$
67	66	recnd	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \to F (y) \in ℂ$
68	67	adantr	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land x = 0_{R}) \to F (y) \in ℂ$
69	68	mul02d	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land x = 0_{R}) \to 0 \cdot F (y) = 0$
70	64 69	eqtrd	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land x = 0_{R}) \to F (x) F (y) = 0$
71	52 62 70	3eqtr4d	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land x = 0_{R}) \to F (x \cdot_{R} y) = F (x) F (y)$
72	51	adantr	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land y = 0_{R}) \to F (0_{R}) = 0$
73		oveq2	$⊢ y = 0_{R} \to x \cdot_{R} y = x \cdot_{R} 0_{R}$
74		simp2	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x \in {Base}_{R}$
75	56 57 58	ringrz	$⊢ (R \in Ring \land x \in {Base}_{R}) \to x \cdot_{R} 0_{R} = 0_{R}$
76	54 74 75	syl2anc	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x \cdot_{R} 0_{R} = 0_{R}$
77	73 76	sylan9eqr	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land y = 0_{R}) \to x \cdot_{R} y = 0_{R}$
78	77	fveq2d	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land y = 0_{R}) \to F (x \cdot_{R} y) = F (0_{R})$
79		fveq2	$⊢ y = 0_{R} \to F (y) = F (0_{R})$
80	79 51	sylan9eqr	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land y = 0_{R}) \to F (y) = 0$
81	80	oveq2d	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land y = 0_{R}) \to F (x) F (y) = F (x) \cdot 0$
82	65 74	ffvelrnd	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \to F (x) \in ℝ$
83	82	recnd	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \to F (x) \in ℂ$
84	83	adantr	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land y = 0_{R}) \to F (x) \in ℂ$
85	84	mul01d	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land y = 0_{R}) \to F (x) \cdot 0 = 0$
86	81 85	eqtrd	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land y = 0_{R}) \to F (x) F (y) = 0$
87	72 78 86	3eqtr4d	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land y = 0_{R}) \to F (x \cdot_{R} y) = F (x) F (y)$
88		simpl1	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land (x \neq 0_{R} \land y \neq 0_{R})) \to φ$
89	88 4	syl	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land (x \neq 0_{R} \land y \neq 0_{R})) \to \underset{˙}{\cdot} = \cdot_{R}$
90	89	oveqd	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land (x \neq 0_{R} \land y \neq 0_{R})) \to x \underset{˙}{\cdot} y = x \cdot_{R} y$
91	90	fveq2d	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land (x \neq 0_{R} \land y \neq 0_{R})) \to F (x \underset{˙}{\cdot} y) = F (x \cdot_{R} y)$
92		simpl2	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land (x \neq 0_{R} \land y \neq 0_{R})) \to x \in {Base}_{R}$
93	88 2	syl	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land (x \neq 0_{R} \land y \neq 0_{R})) \to B = {Base}_{R}$
94	92 93	eleqtrrd	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land (x \neq 0_{R} \land y \neq 0_{R})) \to x \in B$
95		simprl	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land (x \neq 0_{R} \land y \neq 0_{R})) \to x \neq 0_{R}$
96	88 5	syl	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land (x \neq 0_{R} \land y \neq 0_{R})) \to \underset{˙}{0} = 0_{R}$
97	95 96	neeqtrrd	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land (x \neq 0_{R} \land y \neq 0_{R})) \to x \neq \underset{˙}{0}$
98		simpl3	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land (x \neq 0_{R} \land y \neq 0_{R})) \to y \in {Base}_{R}$
99	98 93	eleqtrrd	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land (x \neq 0_{R} \land y \neq 0_{R})) \to y \in B$
100		simprr	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land (x \neq 0_{R} \land y \neq 0_{R})) \to y \neq 0_{R}$
101	100 96	neeqtrrd	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land (x \neq 0_{R} \land y \neq 0_{R})) \to y \neq \underset{˙}{0}$
102	88 94 97 99 101 10	syl122anc	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land (x \neq 0_{R} \land y \neq 0_{R})) \to F (x \underset{˙}{\cdot} y) = F (x) F (y)$
103	91 102	eqtr3d	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land (x \neq 0_{R} \land y \neq 0_{R})) \to F (x \cdot_{R} y) = F (x) F (y)$
104	71 87 103	pm2.61da2ne	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \to F (x \cdot_{R} y) = F (x) F (y)$
105		oveq1	$⊢ x = 0_{R} \to x +_{R} y = 0_{R} +_{R} y$
106		ringgrp	$⊢ R \in Ring \to R \in Grp$
107	54 106	syl	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \to R \in Grp$
108		eqid	$⊢ +_{R} = +_{R}$
109	56 108 58	grplid	$⊢ (R \in Grp \land y \in {Base}_{R}) \to 0_{R} +_{R} y = y$
110	107 55 109	syl2anc	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \to 0_{R} +_{R} y = y$
111	105 110	sylan9eqr	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land x = 0_{R}) \to x +_{R} y = y$
112	111	fveq2d	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land x = 0_{R}) \to F (x +_{R} y) = F (y)$
113	16 63	breqtrrid	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land x = 0_{R}) \to 0 \leq F (x)$
114	66 82	addge02d	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \to (0 \leq F (x) \leftrightarrow F (y) \leq F (x) + F (y))$
115	114	adantr	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land x = 0_{R}) \to (0 \leq F (x) \leftrightarrow F (y) \leq F (x) + F (y))$
116	113 115	mpbid	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land x = 0_{R}) \to F (y) \leq F (x) + F (y)$
117	112 116	eqbrtrd	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land x = 0_{R}) \to F (x +_{R} y) \leq F (x) + F (y)$
118		oveq2	$⊢ y = 0_{R} \to x +_{R} y = x +_{R} 0_{R}$
119	56 108 58	grprid	$⊢ (R \in Grp \land x \in {Base}_{R}) \to x +_{R} 0_{R} = x$
120	107 74 119	syl2anc	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x +_{R} 0_{R} = x$
121	118 120	sylan9eqr	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land y = 0_{R}) \to x +_{R} y = x$
122	121	fveq2d	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land y = 0_{R}) \to F (x +_{R} y) = F (x)$
123	16 80	breqtrrid	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land y = 0_{R}) \to 0 \leq F (y)$
124	82 66	addge01d	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \to (0 \leq F (y) \leftrightarrow F (x) \leq F (x) + F (y))$
125	124	adantr	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land y = 0_{R}) \to (0 \leq F (y) \leftrightarrow F (x) \leq F (x) + F (y))$
126	123 125	mpbid	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land y = 0_{R}) \to F (x) \leq F (x) + F (y)$
127	122 126	eqbrtrd	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land y = 0_{R}) \to F (x +_{R} y) \leq F (x) + F (y)$
128	88 3	syl	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land (x \neq 0_{R} \land y \neq 0_{R})) \to \underset{˙}{+} = +_{R}$
129	128	oveqd	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land (x \neq 0_{R} \land y \neq 0_{R})) \to x \underset{˙}{+} y = x +_{R} y$
130	129	fveq2d	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land (x \neq 0_{R} \land y \neq 0_{R})) \to F (x \underset{˙}{+} y) = F (x +_{R} y)$
131	88 94 97 99 101 11	syl122anc	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land (x \neq 0_{R} \land y \neq 0_{R})) \to F (x \underset{˙}{+} y) \leq F (x) + F (y)$
132	130 131	eqbrtrrd	$⊢ ((φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \land (x \neq 0_{R} \land y \neq 0_{R})) \to F (x +_{R} y) \leq F (x) + F (y)$
133	117 127 132	pm2.61da2ne	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \to F (x +_{R} y) \leq F (x) + F (y)$
134	104 133	jca	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \to (F (x \cdot_{R} y) = F (x) F (y) \land F (x +_{R} y) \leq F (x) + F (y))$
135	134	3expia	$⊢ (φ \land x \in {Base}_{R}) \to (y \in {Base}_{R} \to (F (x \cdot_{R} y) = F (x) F (y) \land F (x +_{R} y) \leq F (x) + F (y)))$
136	135	ralrimiv	$⊢ (φ \land x \in {Base}_{R}) \to \forall y \in {Base}_{R} (F (x \cdot_{R} y) = F (x) F (y) \land F (x +_{R} y) \leq F (x) + F (y))$
137	50 136	jca	$⊢ (φ \land x \in {Base}_{R}) \to ((F (x) = 0 \leftrightarrow x = 0_{R}) \land \forall y \in {Base}_{R} (F (x \cdot_{R} y) = F (x) F (y) \land F (x +_{R} y) \leq F (x) + F (y)))$
138	137	ralrimiva	$⊢ φ \to \forall x \in {Base}_{R} ((F (x) = 0 \leftrightarrow x = 0_{R}) \land \forall y \in {Base}_{R} (F (x \cdot_{R} y) = F (x) F (y) \land F (x +_{R} y) \leq F (x) + F (y)))$
139		eqid	$⊢ AbsVal (R) = AbsVal (R)$
140	139 56 108 57 58	isabv	$⊢ R \in Ring \to (F \in AbsVal (R) \leftrightarrow (F : {Base}_{R} ⟶ [0, +∞) \land \forall x \in {Base}_{R} ((F (x) = 0 \leftrightarrow x = 0_{R}) \land \forall y \in {Base}_{R} (F (x \cdot_{R} y) = F (x) F (y) \land F (x +_{R} y) \leq F (x) + F (y)))))$
141	6 140	syl	$⊢ φ \to (F \in AbsVal (R) \leftrightarrow (F : {Base}_{R} ⟶ [0, +∞) \land \forall x \in {Base}_{R} ((F (x) = 0 \leftrightarrow x = 0_{R}) \land \forall y \in {Base}_{R} (F (x \cdot_{R} y) = F (x) F (y) \land F (x +_{R} y) \leq F (x) + F (y)))))$
142	43 138 141	mpbir2and	$⊢ φ \to F \in AbsVal (R)$
143	142 1	eleqtrrd	$⊢ φ \to F \in A$

Metamath Proof Explorer

Theorem isabvd

Proof