This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem abvtrivd

Description: The trivial absolute value. (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses abvtriv.a 
|- A = ( AbsVal ` R )
abvtriv.b 
|- B = ( Base ` R )
abvtriv.z 
|- .0. = ( 0g ` R )
abvtriv.f 
|- F = ( x e. B |-> if ( x = .0. , 0 , 1 ) )
abvtrivd.1 
|- .x. = ( .r ` R )
abvtrivd.2 
|- ( ph -> R e. Ring )
abvtrivd.3 
|- ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( y .x. z ) =/= .0. )
Assertion abvtrivd 
|- ( ph -> F e. A )

Proof

Step Hyp Ref Expression
1 abvtriv.a 
 |-  A = ( AbsVal ` R )
2 abvtriv.b 
 |-  B = ( Base ` R )
3 abvtriv.z 
 |-  .0. = ( 0g ` R )
4 abvtriv.f 
 |-  F = ( x e. B |-> if ( x = .0. , 0 , 1 ) )
5 abvtrivd.1 
 |-  .x. = ( .r ` R )
6 abvtrivd.2 
 |-  ( ph -> R e. Ring )
7 abvtrivd.3 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( y .x. z ) =/= .0. )
8 1 a1i 
 |-  ( ph -> A = ( AbsVal ` R ) )
9 2 a1i 
 |-  ( ph -> B = ( Base ` R ) )
10 eqidd 
 |-  ( ph -> ( +g ` R ) = ( +g ` R ) )
11 5 a1i 
 |-  ( ph -> .x. = ( .r ` R ) )
12 3 a1i 
 |-  ( ph -> .0. = ( 0g ` R ) )
13 0re 
 |-  0 e. RR
14 1re 
 |-  1 e. RR
15 13 14 ifcli 
 |-  if ( x = .0. , 0 , 1 ) e. RR
16 15 a1i 
 |-  ( ( ph /\ x e. B ) -> if ( x = .0. , 0 , 1 ) e. RR )
17 16 4 fmptd 
 |-  ( ph -> F : B --> RR )
18 2 3 ring0cl 
 |-  ( R e. Ring -> .0. e. B )
19 iftrue 
 |-  ( x = .0. -> if ( x = .0. , 0 , 1 ) = 0 )
20 c0ex 
 |-  0 e. _V
21 19 4 20 fvmpt 
 |-  ( .0. e. B -> ( F ` .0. ) = 0 )
22 6 18 21 3syl 
 |-  ( ph -> ( F ` .0. ) = 0 )
23 0lt1 
 |-  0 < 1
24 eqeq1 
 |-  ( x = y -> ( x = .0. <-> y = .0. ) )
25 24 ifbid 
 |-  ( x = y -> if ( x = .0. , 0 , 1 ) = if ( y = .0. , 0 , 1 ) )
26 1ex 
 |-  1 e. _V
27 20 26 ifex 
 |-  if ( y = .0. , 0 , 1 ) e. _V
28 25 4 27 fvmpt 
 |-  ( y e. B -> ( F ` y ) = if ( y = .0. , 0 , 1 ) )
29 ifnefalse 
 |-  ( y =/= .0. -> if ( y = .0. , 0 , 1 ) = 1 )
30 28 29 sylan9eq 
 |-  ( ( y e. B /\ y =/= .0. ) -> ( F ` y ) = 1 )
31 30 3adant1 
 |-  ( ( ph /\ y e. B /\ y =/= .0. ) -> ( F ` y ) = 1 )
32 23 31 breqtrrid 
 |-  ( ( ph /\ y e. B /\ y =/= .0. ) -> 0 < ( F ` y ) )
33 1t1e1 
 |-  ( 1 x. 1 ) = 1
34 33 eqcomi 
 |-  1 = ( 1 x. 1 )
35 6 3ad2ant1 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> R e. Ring )
36 simp2l 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> y e. B )
37 simp3l 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> z e. B )
38 2 5 ringcl 
 |-  ( ( R e. Ring /\ y e. B /\ z e. B ) -> ( y .x. z ) e. B )
39 35 36 37 38 syl3anc 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( y .x. z ) e. B )
40 eqeq1 
 |-  ( x = ( y .x. z ) -> ( x = .0. <-> ( y .x. z ) = .0. ) )
41 40 ifbid 
 |-  ( x = ( y .x. z ) -> if ( x = .0. , 0 , 1 ) = if ( ( y .x. z ) = .0. , 0 , 1 ) )
42 20 26 ifex 
 |-  if ( ( y .x. z ) = .0. , 0 , 1 ) e. _V
43 41 4 42 fvmpt 
 |-  ( ( y .x. z ) e. B -> ( F ` ( y .x. z ) ) = if ( ( y .x. z ) = .0. , 0 , 1 ) )
44 39 43 syl 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( F ` ( y .x. z ) ) = if ( ( y .x. z ) = .0. , 0 , 1 ) )
45 7 neneqd 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> -. ( y .x. z ) = .0. )
46 45 iffalsed 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> if ( ( y .x. z ) = .0. , 0 , 1 ) = 1 )
47 44 46 eqtrd 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( F ` ( y .x. z ) ) = 1 )
48 36 28 syl 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( F ` y ) = if ( y = .0. , 0 , 1 ) )
49 simp2r 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> y =/= .0. )
50 49 neneqd 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> -. y = .0. )
51 50 iffalsed 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> if ( y = .0. , 0 , 1 ) = 1 )
52 48 51 eqtrd 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( F ` y ) = 1 )
53 eqeq1 
 |-  ( x = z -> ( x = .0. <-> z = .0. ) )
54 53 ifbid 
 |-  ( x = z -> if ( x = .0. , 0 , 1 ) = if ( z = .0. , 0 , 1 ) )
55 20 26 ifex 
 |-  if ( z = .0. , 0 , 1 ) e. _V
56 54 4 55 fvmpt 
 |-  ( z e. B -> ( F ` z ) = if ( z = .0. , 0 , 1 ) )
57 37 56 syl 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( F ` z ) = if ( z = .0. , 0 , 1 ) )
58 simp3r 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> z =/= .0. )
59 58 neneqd 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> -. z = .0. )
60 59 iffalsed 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> if ( z = .0. , 0 , 1 ) = 1 )
61 57 60 eqtrd 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( F ` z ) = 1 )
62 52 61 oveq12d 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( ( F ` y ) x. ( F ` z ) ) = ( 1 x. 1 ) )
63 34 47 62 3eqtr4a 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( F ` ( y .x. z ) ) = ( ( F ` y ) x. ( F ` z ) ) )
64 breq1 
 |-  ( 0 = if ( ( y ( +g ` R ) z ) = .0. , 0 , 1 ) -> ( 0 <_ 2 <-> if ( ( y ( +g ` R ) z ) = .0. , 0 , 1 ) <_ 2 ) )
65 breq1 
 |-  ( 1 = if ( ( y ( +g ` R ) z ) = .0. , 0 , 1 ) -> ( 1 <_ 2 <-> if ( ( y ( +g ` R ) z ) = .0. , 0 , 1 ) <_ 2 ) )
66 0le2 
 |-  0 <_ 2
67 1le2 
 |-  1 <_ 2
68 64 65 66 67 keephyp 
 |-  if ( ( y ( +g ` R ) z ) = .0. , 0 , 1 ) <_ 2
69 df-2 
 |-  2 = ( 1 + 1 )
70 68 69 breqtri 
 |-  if ( ( y ( +g ` R ) z ) = .0. , 0 , 1 ) <_ ( 1 + 1 )
71 70 a1i 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> if ( ( y ( +g ` R ) z ) = .0. , 0 , 1 ) <_ ( 1 + 1 ) )
72 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
73 6 72 syl 
 |-  ( ph -> R e. Grp )
74 73 3ad2ant1 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> R e. Grp )
75 eqid 
 |-  ( +g ` R ) = ( +g ` R )
76 2 75 grpcl 
 |-  ( ( R e. Grp /\ y e. B /\ z e. B ) -> ( y ( +g ` R ) z ) e. B )
77 74 36 37 76 syl3anc 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( y ( +g ` R ) z ) e. B )
78 eqeq1 
 |-  ( x = ( y ( +g ` R ) z ) -> ( x = .0. <-> ( y ( +g ` R ) z ) = .0. ) )
79 78 ifbid 
 |-  ( x = ( y ( +g ` R ) z ) -> if ( x = .0. , 0 , 1 ) = if ( ( y ( +g ` R ) z ) = .0. , 0 , 1 ) )
80 20 26 ifex 
 |-  if ( ( y ( +g ` R ) z ) = .0. , 0 , 1 ) e. _V
81 79 4 80 fvmpt 
 |-  ( ( y ( +g ` R ) z ) e. B -> ( F ` ( y ( +g ` R ) z ) ) = if ( ( y ( +g ` R ) z ) = .0. , 0 , 1 ) )
82 77 81 syl 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( F ` ( y ( +g ` R ) z ) ) = if ( ( y ( +g ` R ) z ) = .0. , 0 , 1 ) )
83 52 61 oveq12d 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( ( F ` y ) + ( F ` z ) ) = ( 1 + 1 ) )
84 71 82 83 3brtr4d 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( F ` ( y ( +g ` R ) z ) ) <_ ( ( F ` y ) + ( F ` z ) ) )
85 8 9 10 11 12 6 17 22 32 63 84 isabvd 
 |-  ( ph -> F e. A )