Metamath Proof Explorer

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 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) ) ) ) )