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 A = AbsVal R
abvfval.b B = Base R
abvfval.p + ˙ = + R
abvfval.t · ˙ = R
abvfval.z 0 ˙ = 0 R
Assertion isabv R Ring F A F : B 0 +∞ x B F x = 0 x = 0 ˙ y B F x · ˙ y = F x F y F x + ˙ y F x + F y

Proof

Step Hyp Ref Expression
1 abvfval.a A = AbsVal R
2 abvfval.b B = Base R
3 abvfval.p + ˙ = + R
4 abvfval.t · ˙ = R
5 abvfval.z 0 ˙ = 0 R
6 1 2 3 4 5 abvfval R Ring A = f 0 +∞ B | x B f x = 0 x = 0 ˙ y B f x · ˙ y = f x f y f x + ˙ y f x + f y
7 6 eleq2d R Ring F A F f 0 +∞ B | x B f x = 0 x = 0 ˙ y B f x · ˙ y = f x f y f x + ˙ y f x + f y
8 fveq1 f = F f x = F x
9 8 eqeq1d f = F f x = 0 F x = 0
10 9 bibi1d f = F f x = 0 x = 0 ˙ F x = 0 x = 0 ˙
11 fveq1 f = F f x · ˙ y = F x · ˙ y
12 fveq1 f = F f y = F y
13 8 12 oveq12d f = F f x f y = F x F y
14 11 13 eqeq12d f = F f x · ˙ y = f x f y F x · ˙ y = F x F y
15 fveq1 f = F f x + ˙ y = F x + ˙ y
16 8 12 oveq12d f = F f x + f y = F x + F y
17 15 16 breq12d f = F f x + ˙ y f x + f y F x + ˙ y F x + F y
18 14 17 anbi12d f = F f x · ˙ y = f x f y f x + ˙ y f x + f y F x · ˙ y = F x F y F x + ˙ y F x + F y
19 18 ralbidv f = F y B f x · ˙ y = f x f y f x + ˙ y f x + f y y B F x · ˙ y = F x F y F x + ˙ y F x + F y
20 10 19 anbi12d f = F f x = 0 x = 0 ˙ y B f x · ˙ y = f x f y f x + ˙ y f x + f y F x = 0 x = 0 ˙ y B F x · ˙ y = F x F y F x + ˙ y F x + F y
21 20 ralbidv f = F x B f x = 0 x = 0 ˙ y B f x · ˙ y = f x f y f x + ˙ y f x + f y x B F x = 0 x = 0 ˙ y B F x · ˙ y = F x F y F x + ˙ y F x + F y
22 21 elrab F f 0 +∞ B | x B f x = 0 x = 0 ˙ y B f x · ˙ y = f x f y f x + ˙ y f x + f y F 0 +∞ B x B F x = 0 x = 0 ˙ y B F x · ˙ y = F x F y F x + ˙ y F x + F y
23 ovex 0 +∞ V
24 2 fvexi B V
25 23 24 elmap F 0 +∞ B F : B 0 +∞
26 25 anbi1i F 0 +∞ B x B F x = 0 x = 0 ˙ y B F x · ˙ y = F x F y F x + ˙ y F x + F y F : B 0 +∞ x B F x = 0 x = 0 ˙ y B F x · ˙ y = F x F y F x + ˙ y F x + F y
27 22 26 bitri F f 0 +∞ B | x B f x = 0 x = 0 ˙ y B f x · ˙ y = f x f y f x + ˙ y f x + f y F : B 0 +∞ x B F x = 0 x = 0 ˙ y B F x · ˙ y = F x F y F x + ˙ y F x + F y
28 7 27 bitrdi R Ring F A F : B 0 +∞ x B F x = 0 x = 0 ˙ y B F x · ˙ y = F x F y F x + ˙ y F x + F y