Theorem isabv

Description: Elementhood in the set of absolute values. (Contributed by Mario Carneiro, 8-Sep-2014)

	Ref	Expression
Hypotheses	abvfval.a	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
	abvfval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	abvfval.p	⊢ + = ( +g ‘ 𝑅 )
	abvfval.t	⊢ · = ( .r ‘ 𝑅 )
	abvfval.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	isabv	⊢ ( 𝑅 ∈ Ring → ( 𝐹 ∈ 𝐴 ↔ ( 𝐹 : 𝐵 ⟶ ( 0 [,) +∞ ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		abvfval.a	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
2		abvfval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		abvfval.p	⊢ + = ( +g ‘ 𝑅 )
4		abvfval.t	⊢ · = ( .r ‘ 𝑅 )
5		abvfval.z	⊢ 0 = ( 0g ‘ 𝑅 )
6	1 2 3 4 5	abvfval	⊢ ( 𝑅 ∈ Ring → 𝐴 = { 𝑓 ∈ ( ( 0 [,) +∞ ) ↑m 𝐵 ) ∣ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ) } )
7	6	eleq2d	⊢ ( 𝑅 ∈ Ring → ( 𝐹 ∈ 𝐴 ↔ 𝐹 ∈ { 𝑓 ∈ ( ( 0 [,) +∞ ) ↑m 𝐵 ) ∣ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ) } ) )
8		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
9	8	eqeq1d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ ( 𝐹 ‘ 𝑥 ) = 0 ) )
10	9	bibi1d	⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ) )
11		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) )
12		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
13	8 12	oveq12d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) )
14	11 13	eqeq12d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) ) )
15		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) )
16	8 12	oveq12d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) )
17	15 16	breq12d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) )
18	14 17	anbi12d	⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) ) )
19	18	ralbidv	⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) ) )
20	10 19	anbi12d	⊢ ( 𝑓 = 𝐹 → ( ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ) ↔ ( ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
21	20	ralbidv	⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
22	21	elrab	⊢ ( 𝐹 ∈ { 𝑓 ∈ ( ( 0 [,) +∞ ) ↑m 𝐵 ) ∣ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ) } ↔ ( 𝐹 ∈ ( ( 0 [,) +∞ ) ↑m 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
23		ovex	⊢ ( 0 [,) +∞ ) ∈ V
24	2	fvexi	⊢ 𝐵 ∈ V
25	23 24	elmap	⊢ ( 𝐹 ∈ ( ( 0 [,) +∞ ) ↑m 𝐵 ) ↔ 𝐹 : 𝐵 ⟶ ( 0 [,) +∞ ) )
26	25	anbi1i	⊢ ( ( 𝐹 ∈ ( ( 0 [,) +∞ ) ↑m 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) ) ) ↔ ( 𝐹 : 𝐵 ⟶ ( 0 [,) +∞ ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
27	22 26	bitri	⊢ ( 𝐹 ∈ { 𝑓 ∈ ( ( 0 [,) +∞ ) ↑m 𝐵 ) ∣ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ) } ↔ ( 𝐹 : 𝐵 ⟶ ( 0 [,) +∞ ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
28	7 27	bitrdi	⊢ ( 𝑅 ∈ Ring → ( 𝐹 ∈ 𝐴 ↔ ( 𝐹 : 𝐵 ⟶ ( 0 [,) +∞ ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) ) ) ) )