MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-abv Structured version   Visualization version   GIF version

Definition df-abv 20292
Description: Define the set of absolute values on a ring. An absolute value is a generalization of the usual absolute value function df-abs 15128 to arbitrary rings. (Contributed by Mario Carneiro, 8-Sep-2014.)
Assertion
Ref Expression
df-abv AbsVal = (๐‘Ÿ โˆˆ Ring โ†ฆ {๐‘“ โˆˆ ((0[,)+โˆž) โ†‘m (Baseโ€˜๐‘Ÿ)) โˆฃ โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘Ÿ)(((๐‘“โ€˜๐‘ฅ) = 0 โ†” ๐‘ฅ = (0gโ€˜๐‘Ÿ)) โˆง โˆ€๐‘ฆ โˆˆ (Baseโ€˜๐‘Ÿ)((๐‘“โ€˜(๐‘ฅ(.rโ€˜๐‘Ÿ)๐‘ฆ)) = ((๐‘“โ€˜๐‘ฅ) ยท (๐‘“โ€˜๐‘ฆ)) โˆง (๐‘“โ€˜(๐‘ฅ(+gโ€˜๐‘Ÿ)๐‘ฆ)) โ‰ค ((๐‘“โ€˜๐‘ฅ) + (๐‘“โ€˜๐‘ฆ))))})
Distinct variable group:   ๐‘“,๐‘Ÿ,๐‘ฅ,๐‘ฆ

Detailed syntax breakdown of Definition df-abv
StepHypRef Expression
1 cabv 20291 . 2 class AbsVal
2 vr . . 3 setvar ๐‘Ÿ
3 crg 19971 . . 3 class Ring
4 vx . . . . . . . . . 10 setvar ๐‘ฅ
54cv 1541 . . . . . . . . 9 class ๐‘ฅ
6 vf . . . . . . . . . 10 setvar ๐‘“
76cv 1541 . . . . . . . . 9 class ๐‘“
85, 7cfv 6501 . . . . . . . 8 class (๐‘“โ€˜๐‘ฅ)
9 cc0 11058 . . . . . . . 8 class 0
108, 9wceq 1542 . . . . . . 7 wff (๐‘“โ€˜๐‘ฅ) = 0
112cv 1541 . . . . . . . . 9 class ๐‘Ÿ
12 c0g 17328 . . . . . . . . 9 class 0g
1311, 12cfv 6501 . . . . . . . 8 class (0gโ€˜๐‘Ÿ)
145, 13wceq 1542 . . . . . . 7 wff ๐‘ฅ = (0gโ€˜๐‘Ÿ)
1510, 14wb 205 . . . . . 6 wff ((๐‘“โ€˜๐‘ฅ) = 0 โ†” ๐‘ฅ = (0gโ€˜๐‘Ÿ))
16 vy . . . . . . . . . . . 12 setvar ๐‘ฆ
1716cv 1541 . . . . . . . . . . 11 class ๐‘ฆ
18 cmulr 17141 . . . . . . . . . . . 12 class .r
1911, 18cfv 6501 . . . . . . . . . . 11 class (.rโ€˜๐‘Ÿ)
205, 17, 19co 7362 . . . . . . . . . 10 class (๐‘ฅ(.rโ€˜๐‘Ÿ)๐‘ฆ)
2120, 7cfv 6501 . . . . . . . . 9 class (๐‘“โ€˜(๐‘ฅ(.rโ€˜๐‘Ÿ)๐‘ฆ))
2217, 7cfv 6501 . . . . . . . . . 10 class (๐‘“โ€˜๐‘ฆ)
23 cmul 11063 . . . . . . . . . 10 class ยท
248, 22, 23co 7362 . . . . . . . . 9 class ((๐‘“โ€˜๐‘ฅ) ยท (๐‘“โ€˜๐‘ฆ))
2521, 24wceq 1542 . . . . . . . 8 wff (๐‘“โ€˜(๐‘ฅ(.rโ€˜๐‘Ÿ)๐‘ฆ)) = ((๐‘“โ€˜๐‘ฅ) ยท (๐‘“โ€˜๐‘ฆ))
26 cplusg 17140 . . . . . . . . . . . 12 class +g
2711, 26cfv 6501 . . . . . . . . . . 11 class (+gโ€˜๐‘Ÿ)
285, 17, 27co 7362 . . . . . . . . . 10 class (๐‘ฅ(+gโ€˜๐‘Ÿ)๐‘ฆ)
2928, 7cfv 6501 . . . . . . . . 9 class (๐‘“โ€˜(๐‘ฅ(+gโ€˜๐‘Ÿ)๐‘ฆ))
30 caddc 11061 . . . . . . . . . 10 class +
318, 22, 30co 7362 . . . . . . . . 9 class ((๐‘“โ€˜๐‘ฅ) + (๐‘“โ€˜๐‘ฆ))
32 cle 11197 . . . . . . . . 9 class โ‰ค
3329, 31, 32wbr 5110 . . . . . . . 8 wff (๐‘“โ€˜(๐‘ฅ(+gโ€˜๐‘Ÿ)๐‘ฆ)) โ‰ค ((๐‘“โ€˜๐‘ฅ) + (๐‘“โ€˜๐‘ฆ))
3425, 33wa 397 . . . . . . 7 wff ((๐‘“โ€˜(๐‘ฅ(.rโ€˜๐‘Ÿ)๐‘ฆ)) = ((๐‘“โ€˜๐‘ฅ) ยท (๐‘“โ€˜๐‘ฆ)) โˆง (๐‘“โ€˜(๐‘ฅ(+gโ€˜๐‘Ÿ)๐‘ฆ)) โ‰ค ((๐‘“โ€˜๐‘ฅ) + (๐‘“โ€˜๐‘ฆ)))
35 cbs 17090 . . . . . . . 8 class Base
3611, 35cfv 6501 . . . . . . 7 class (Baseโ€˜๐‘Ÿ)
3734, 16, 36wral 3065 . . . . . 6 wff โˆ€๐‘ฆ โˆˆ (Baseโ€˜๐‘Ÿ)((๐‘“โ€˜(๐‘ฅ(.rโ€˜๐‘Ÿ)๐‘ฆ)) = ((๐‘“โ€˜๐‘ฅ) ยท (๐‘“โ€˜๐‘ฆ)) โˆง (๐‘“โ€˜(๐‘ฅ(+gโ€˜๐‘Ÿ)๐‘ฆ)) โ‰ค ((๐‘“โ€˜๐‘ฅ) + (๐‘“โ€˜๐‘ฆ)))
3815, 37wa 397 . . . . 5 wff (((๐‘“โ€˜๐‘ฅ) = 0 โ†” ๐‘ฅ = (0gโ€˜๐‘Ÿ)) โˆง โˆ€๐‘ฆ โˆˆ (Baseโ€˜๐‘Ÿ)((๐‘“โ€˜(๐‘ฅ(.rโ€˜๐‘Ÿ)๐‘ฆ)) = ((๐‘“โ€˜๐‘ฅ) ยท (๐‘“โ€˜๐‘ฆ)) โˆง (๐‘“โ€˜(๐‘ฅ(+gโ€˜๐‘Ÿ)๐‘ฆ)) โ‰ค ((๐‘“โ€˜๐‘ฅ) + (๐‘“โ€˜๐‘ฆ))))
3938, 4, 36wral 3065 . . . 4 wff โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘Ÿ)(((๐‘“โ€˜๐‘ฅ) = 0 โ†” ๐‘ฅ = (0gโ€˜๐‘Ÿ)) โˆง โˆ€๐‘ฆ โˆˆ (Baseโ€˜๐‘Ÿ)((๐‘“โ€˜(๐‘ฅ(.rโ€˜๐‘Ÿ)๐‘ฆ)) = ((๐‘“โ€˜๐‘ฅ) ยท (๐‘“โ€˜๐‘ฆ)) โˆง (๐‘“โ€˜(๐‘ฅ(+gโ€˜๐‘Ÿ)๐‘ฆ)) โ‰ค ((๐‘“โ€˜๐‘ฅ) + (๐‘“โ€˜๐‘ฆ))))
40 cpnf 11193 . . . . . 6 class +โˆž
41 cico 13273 . . . . . 6 class [,)
429, 40, 41co 7362 . . . . 5 class (0[,)+โˆž)
43 cmap 8772 . . . . 5 class โ†‘m
4442, 36, 43co 7362 . . . 4 class ((0[,)+โˆž) โ†‘m (Baseโ€˜๐‘Ÿ))
4539, 6, 44crab 3410 . . 3 class {๐‘“ โˆˆ ((0[,)+โˆž) โ†‘m (Baseโ€˜๐‘Ÿ)) โˆฃ โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘Ÿ)(((๐‘“โ€˜๐‘ฅ) = 0 โ†” ๐‘ฅ = (0gโ€˜๐‘Ÿ)) โˆง โˆ€๐‘ฆ โˆˆ (Baseโ€˜๐‘Ÿ)((๐‘“โ€˜(๐‘ฅ(.rโ€˜๐‘Ÿ)๐‘ฆ)) = ((๐‘“โ€˜๐‘ฅ) ยท (๐‘“โ€˜๐‘ฆ)) โˆง (๐‘“โ€˜(๐‘ฅ(+gโ€˜๐‘Ÿ)๐‘ฆ)) โ‰ค ((๐‘“โ€˜๐‘ฅ) + (๐‘“โ€˜๐‘ฆ))))}
462, 3, 45cmpt 5193 . 2 class (๐‘Ÿ โˆˆ Ring โ†ฆ {๐‘“ โˆˆ ((0[,)+โˆž) โ†‘m (Baseโ€˜๐‘Ÿ)) โˆฃ โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘Ÿ)(((๐‘“โ€˜๐‘ฅ) = 0 โ†” ๐‘ฅ = (0gโ€˜๐‘Ÿ)) โˆง โˆ€๐‘ฆ โˆˆ (Baseโ€˜๐‘Ÿ)((๐‘“โ€˜(๐‘ฅ(.rโ€˜๐‘Ÿ)๐‘ฆ)) = ((๐‘“โ€˜๐‘ฅ) ยท (๐‘“โ€˜๐‘ฆ)) โˆง (๐‘“โ€˜(๐‘ฅ(+gโ€˜๐‘Ÿ)๐‘ฆ)) โ‰ค ((๐‘“โ€˜๐‘ฅ) + (๐‘“โ€˜๐‘ฆ))))})
471, 46wceq 1542 1 wff AbsVal = (๐‘Ÿ โˆˆ Ring โ†ฆ {๐‘“ โˆˆ ((0[,)+โˆž) โ†‘m (Baseโ€˜๐‘Ÿ)) โˆฃ โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘Ÿ)(((๐‘“โ€˜๐‘ฅ) = 0 โ†” ๐‘ฅ = (0gโ€˜๐‘Ÿ)) โˆง โˆ€๐‘ฆ โˆˆ (Baseโ€˜๐‘Ÿ)((๐‘“โ€˜(๐‘ฅ(.rโ€˜๐‘Ÿ)๐‘ฆ)) = ((๐‘“โ€˜๐‘ฅ) ยท (๐‘“โ€˜๐‘ฆ)) โˆง (๐‘“โ€˜(๐‘ฅ(+gโ€˜๐‘Ÿ)๐‘ฆ)) โ‰ค ((๐‘“โ€˜๐‘ฅ) + (๐‘“โ€˜๐‘ฆ))))})
Colors of variables: wff setvar class
This definition is referenced by:  abvfval  20293  abvrcl  20296
  Copyright terms: Public domain W3C validator