Metamath Proof Explorer

Theorem isabvd

Description: Properties that determine an absolute value. (Contributed by Mario Carneiro, 8-Sep-2014) (Revised by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses isabvd.a 
|- ( ph -> A = ( AbsVal ` R ) )
isabvd.b 
|- ( ph -> B = ( Base ` R ) )
isabvd.p 
|- ( ph -> .+ = ( +g ` R ) )
isabvd.t 
|- ( ph -> .x. = ( .r ` R ) )
isabvd.z 
|- ( ph -> .0. = ( 0g ` R ) )
isabvd.1 
|- ( ph -> R e. Ring )
isabvd.2 
|- ( ph -> F : B --> RR )
isabvd.3 
|- ( ph -> ( F ` .0. ) = 0 )
isabvd.4 
|- ( ( ph /\ x e. B /\ x =/= .0. ) -> 0 < ( F ` x ) )
isabvd.5 
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) -> ( F ` ( x .x. y ) ) = ( ( F ` x ) x. ( F ` y ) ) )
isabvd.6 
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) -> ( F ` ( x .+ y ) ) <_ ( ( F ` x ) + ( F ` y ) ) )
Assertion isabvd 
|- ( ph -> F e. A )

Proof

Step Hyp Ref Expression
1 isabvd.a 
 |-  ( ph -> A = ( AbsVal ` R ) )
2 isabvd.b 
 |-  ( ph -> B = ( Base ` R ) )
3 isabvd.p 
 |-  ( ph -> .+ = ( +g ` R ) )
4 isabvd.t 
 |-  ( ph -> .x. = ( .r ` R ) )
5 isabvd.z 
 |-  ( ph -> .0. = ( 0g ` R ) )
6 isabvd.1 
 |-  ( ph -> R e. Ring )
7 isabvd.2 
 |-  ( ph -> F : B --> RR )
8 isabvd.3 
 |-  ( ph -> ( F ` .0. ) = 0 )
9 isabvd.4 
 |-  ( ( ph /\ x e. B /\ x =/= .0. ) -> 0 < ( F ` x ) )
10 isabvd.5 
 |-  ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) -> ( F ` ( x .x. y ) ) = ( ( F ` x ) x. ( F ` y ) ) )
11 isabvd.6 
 |-  ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) -> ( F ` ( x .+ y ) ) <_ ( ( F ` x ) + ( F ` y ) ) )
12 2 feq2d 
 |-  ( ph -> ( F : B --> RR <-> F : ( Base ` R ) --> RR ) )
13 7 12 mpbid 
 |-  ( ph -> F : ( Base ` R ) --> RR )
14 13 ffnd 
 |-  ( ph -> F Fn ( Base ` R ) )
15 13 ffvelcdmda 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( F ` x ) e. RR )
16 0le0 
 |-  0 <_ 0
17 5 fveq2d 
 |-  ( ph -> ( F ` .0. ) = ( F ` ( 0g ` R ) ) )
18 17 8 eqtr3d 
 |-  ( ph -> ( F ` ( 0g ` R ) ) = 0 )
19 16 18 breqtrrid 
 |-  ( ph -> 0 <_ ( F ` ( 0g ` R ) ) )
20 19 adantr 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> 0 <_ ( F ` ( 0g ` R ) ) )
21 fveq2 
 |-  ( x = ( 0g ` R ) -> ( F ` x ) = ( F ` ( 0g ` R ) ) )
22 21 breq2d 
 |-  ( x = ( 0g ` R ) -> ( 0 <_ ( F ` x ) <-> 0 <_ ( F ` ( 0g ` R ) ) ) )
23 20 22 syl5ibrcom 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( x = ( 0g ` R ) -> 0 <_ ( F ` x ) ) )
24 simp1 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ x =/= ( 0g ` R ) ) -> ph )
25 simp2 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ x =/= ( 0g ` R ) ) -> x e. ( Base ` R ) )
26 2 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ x =/= ( 0g ` R ) ) -> B = ( Base ` R ) )
27 25 26 eleqtrrd 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ x =/= ( 0g ` R ) ) -> x e. B )
28 simp3 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ x =/= ( 0g ` R ) ) -> x =/= ( 0g ` R ) )
29 5 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ x =/= ( 0g ` R ) ) -> .0. = ( 0g ` R ) )
30 28 29 neeqtrrd 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ x =/= ( 0g ` R ) ) -> x =/= .0. )
31 24 27 30 9 syl3anc 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ x =/= ( 0g ` R ) ) -> 0 < ( F ` x ) )
32 0re 
 |-  0 e. RR
33 15 3adant3 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ x =/= ( 0g ` R ) ) -> ( F ` x ) e. RR )
34 ltle 
 |-  ( ( 0 e. RR /\ ( F ` x ) e. RR ) -> ( 0 < ( F ` x ) -> 0 <_ ( F ` x ) ) )
35 32 33 34 sylancr 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ x =/= ( 0g ` R ) ) -> ( 0 < ( F ` x ) -> 0 <_ ( F ` x ) ) )
36 31 35 mpd 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ x =/= ( 0g ` R ) ) -> 0 <_ ( F ` x ) )
37 36 3expia 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( x =/= ( 0g ` R ) -> 0 <_ ( F ` x ) ) )
38 23 37 pm2.61dne 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> 0 <_ ( F ` x ) )
39 elrege0 
 |-  ( ( F ` x ) e. ( 0 [,) +oo ) <-> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
40 15 38 39 sylanbrc 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( F ` x ) e. ( 0 [,) +oo ) )
41 40 ralrimiva 
 |-  ( ph -> A. x e. ( Base ` R ) ( F ` x ) e. ( 0 [,) +oo ) )
42 ffnfv 
 |-  ( F : ( Base ` R ) --> ( 0 [,) +oo ) <-> ( F Fn ( Base ` R ) /\ A. x e. ( Base ` R ) ( F ` x ) e. ( 0 [,) +oo ) ) )
43 14 41 42 sylanbrc 
 |-  ( ph -> F : ( Base ` R ) --> ( 0 [,) +oo ) )
44 31 gt0ne0d 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ x =/= ( 0g ` R ) ) -> ( F ` x ) =/= 0 )
45 44 3expia 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( x =/= ( 0g ` R ) -> ( F ` x ) =/= 0 ) )
46 45 necon4d 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( ( F ` x ) = 0 -> x = ( 0g ` R ) ) )
47 18 adantr 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( F ` ( 0g ` R ) ) = 0 )
48 fveqeq2 
 |-  ( x = ( 0g ` R ) -> ( ( F ` x ) = 0 <-> ( F ` ( 0g ` R ) ) = 0 ) )
49 47 48 syl5ibrcom 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( x = ( 0g ` R ) -> ( F ` x ) = 0 ) )
50 46 49 impbid 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( ( F ` x ) = 0 <-> x = ( 0g ` R ) ) )
51 18 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( F ` ( 0g ` R ) ) = 0 )
52 51 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ x = ( 0g ` R ) ) -> ( F ` ( 0g ` R ) ) = 0 )
53 oveq1 
 |-  ( x = ( 0g ` R ) -> ( x ( .r ` R ) y ) = ( ( 0g ` R ) ( .r ` R ) y ) )
54 6 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> R e. Ring )
55 simp3 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> y e. ( Base ` R ) )
56 eqid 
 |-  ( Base ` R ) = ( Base ` R )
57 eqid 
 |-  ( .r ` R ) = ( .r ` R )
58 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
59 56 57 58 ringlz 
 |-  ( ( R e. Ring /\ y e. ( Base ` R ) ) -> ( ( 0g ` R ) ( .r ` R ) y ) = ( 0g ` R ) )
60 54 55 59 syl2anc 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( ( 0g ` R ) ( .r ` R ) y ) = ( 0g ` R ) )
61 53 60 sylan9eqr 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ x = ( 0g ` R ) ) -> ( x ( .r ` R ) y ) = ( 0g ` R ) )
62 61 fveq2d 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ x = ( 0g ` R ) ) -> ( F ` ( x ( .r ` R ) y ) ) = ( F ` ( 0g ` R ) ) )
63 21 51 sylan9eqr 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ x = ( 0g ` R ) ) -> ( F ` x ) = 0 )
64 63 oveq1d 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ x = ( 0g ` R ) ) -> ( ( F ` x ) x. ( F ` y ) ) = ( 0 x. ( F ` y ) ) )
65 13 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> F : ( Base ` R ) --> RR )
66 65 55 ffvelcdmd 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( F ` y ) e. RR )
67 66 recnd 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( F ` y ) e. CC )
68 67 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ x = ( 0g ` R ) ) -> ( F ` y ) e. CC )
69 68 mul02d 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ x = ( 0g ` R ) ) -> ( 0 x. ( F ` y ) ) = 0 )
70 64 69 eqtrd 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ x = ( 0g ` R ) ) -> ( ( F ` x ) x. ( F ` y ) ) = 0 )
71 52 62 70 3eqtr4d 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ x = ( 0g ` R ) ) -> ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) x. ( F ` y ) ) )
72 51 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ y = ( 0g ` R ) ) -> ( F ` ( 0g ` R ) ) = 0 )
73 oveq2 
 |-  ( y = ( 0g ` R ) -> ( x ( .r ` R ) y ) = ( x ( .r ` R ) ( 0g ` R ) ) )
74 simp2 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> x e. ( Base ` R ) )
75 56 57 58 ringrz 
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) ) -> ( x ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
76 54 74 75 syl2anc 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
77 73 76 sylan9eqr 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ y = ( 0g ` R ) ) -> ( x ( .r ` R ) y ) = ( 0g ` R ) )
78 77 fveq2d 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ y = ( 0g ` R ) ) -> ( F ` ( x ( .r ` R ) y ) ) = ( F ` ( 0g ` R ) ) )
79 fveq2 
 |-  ( y = ( 0g ` R ) -> ( F ` y ) = ( F ` ( 0g ` R ) ) )
80 79 51 sylan9eqr 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ y = ( 0g ` R ) ) -> ( F ` y ) = 0 )
81 80 oveq2d 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ y = ( 0g ` R ) ) -> ( ( F ` x ) x. ( F ` y ) ) = ( ( F ` x ) x. 0 ) )
82 65 74 ffvelcdmd 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( F ` x ) e. RR )
83 82 recnd 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( F ` x ) e. CC )
84 83 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ y = ( 0g ` R ) ) -> ( F ` x ) e. CC )
85 84 mul01d 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ y = ( 0g ` R ) ) -> ( ( F ` x ) x. 0 ) = 0 )
86 81 85 eqtrd 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ y = ( 0g ` R ) ) -> ( ( F ` x ) x. ( F ` y ) ) = 0 )
87 72 78 86 3eqtr4d 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ y = ( 0g ` R ) ) -> ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) x. ( F ` y ) ) )
88 simpl1 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ ( x =/= ( 0g ` R ) /\ y =/= ( 0g ` R ) ) ) -> ph )
89 88 4 syl 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ ( x =/= ( 0g ` R ) /\ y =/= ( 0g ` R ) ) ) -> .x. = ( .r ` R ) )
90 89 oveqd 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ ( x =/= ( 0g ` R ) /\ y =/= ( 0g ` R ) ) ) -> ( x .x. y ) = ( x ( .r ` R ) y ) )
91 90 fveq2d 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ ( x =/= ( 0g ` R ) /\ y =/= ( 0g ` R ) ) ) -> ( F ` ( x .x. y ) ) = ( F ` ( x ( .r ` R ) y ) ) )
92 simpl2 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ ( x =/= ( 0g ` R ) /\ y =/= ( 0g ` R ) ) ) -> x e. ( Base ` R ) )
93 88 2 syl 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ ( x =/= ( 0g ` R ) /\ y =/= ( 0g ` R ) ) ) -> B = ( Base ` R ) )
94 92 93 eleqtrrd 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ ( x =/= ( 0g ` R ) /\ y =/= ( 0g ` R ) ) ) -> x e. B )
95 simprl 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ ( x =/= ( 0g ` R ) /\ y =/= ( 0g ` R ) ) ) -> x =/= ( 0g ` R ) )
96 88 5 syl 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ ( x =/= ( 0g ` R ) /\ y =/= ( 0g ` R ) ) ) -> .0. = ( 0g ` R ) )
97 95 96 neeqtrrd 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ ( x =/= ( 0g ` R ) /\ y =/= ( 0g ` R ) ) ) -> x =/= .0. )
98 simpl3 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ ( x =/= ( 0g ` R ) /\ y =/= ( 0g ` R ) ) ) -> y e. ( Base ` R ) )
99 98 93 eleqtrrd 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ ( x =/= ( 0g ` R ) /\ y =/= ( 0g ` R ) ) ) -> y e. B )
100 simprr 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ ( x =/= ( 0g ` R ) /\ y =/= ( 0g ` R ) ) ) -> y =/= ( 0g ` R ) )
101 100 96 neeqtrrd 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ ( x =/= ( 0g ` R ) /\ y =/= ( 0g ` R ) ) ) -> y =/= .0. )
102 88 94 97 99 101 10 syl122anc 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ ( x =/= ( 0g ` R ) /\ y =/= ( 0g ` R ) ) ) -> ( F ` ( x .x. y ) ) = ( ( F ` x ) x. ( F ` y ) ) )
103 91 102 eqtr3d 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ ( x =/= ( 0g ` R ) /\ y =/= ( 0g ` R ) ) ) -> ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) x. ( F ` y ) ) )
104 71 87 103 pm2.61da2ne 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) x. ( F ` y ) ) )
105 oveq1 
 |-  ( x = ( 0g ` R ) -> ( x ( +g ` R ) y ) = ( ( 0g ` R ) ( +g ` R ) y ) )
106 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
107 54 106 syl 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> R e. Grp )
108 eqid 
 |-  ( +g ` R ) = ( +g ` R )
109 56 108 58 grplid 
 |-  ( ( R e. Grp /\ y e. ( Base ` R ) ) -> ( ( 0g ` R ) ( +g ` R ) y ) = y )
110 107 55 109 syl2anc 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( ( 0g ` R ) ( +g ` R ) y ) = y )
111 105 110 sylan9eqr 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ x = ( 0g ` R ) ) -> ( x ( +g ` R ) y ) = y )
112 111 fveq2d 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ x = ( 0g ` R ) ) -> ( F ` ( x ( +g ` R ) y ) ) = ( F ` y ) )
113 16 63 breqtrrid 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ x = ( 0g ` R ) ) -> 0 <_ ( F ` x ) )
114 66 82 addge02d 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( 0 <_ ( F ` x ) <-> ( F ` y ) <_ ( ( F ` x ) + ( F ` y ) ) ) )
115 114 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ x = ( 0g ` R ) ) -> ( 0 <_ ( F ` x ) <-> ( F ` y ) <_ ( ( F ` x ) + ( F ` y ) ) ) )
116 113 115 mpbid 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ x = ( 0g ` R ) ) -> ( F ` y ) <_ ( ( F ` x ) + ( F ` y ) ) )
117 112 116 eqbrtrd 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ x = ( 0g ` R ) ) -> ( F ` ( x ( +g ` R ) y ) ) <_ ( ( F ` x ) + ( F ` y ) ) )
118 oveq2 
 |-  ( y = ( 0g ` R ) -> ( x ( +g ` R ) y ) = ( x ( +g ` R ) ( 0g ` R ) ) )
119 56 108 58 grprid 
 |-  ( ( R e. Grp /\ x e. ( Base ` R ) ) -> ( x ( +g ` R ) ( 0g ` R ) ) = x )
120 107 74 119 syl2anc 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x ( +g ` R ) ( 0g ` R ) ) = x )
121 118 120 sylan9eqr 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ y = ( 0g ` R ) ) -> ( x ( +g ` R ) y ) = x )
122 121 fveq2d 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ y = ( 0g ` R ) ) -> ( F ` ( x ( +g ` R ) y ) ) = ( F ` x ) )
123 16 80 breqtrrid 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ y = ( 0g ` R ) ) -> 0 <_ ( F ` y ) )
124 82 66 addge01d 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( 0 <_ ( F ` y ) <-> ( F ` x ) <_ ( ( F ` x ) + ( F ` y ) ) ) )
125 124 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ y = ( 0g ` R ) ) -> ( 0 <_ ( F ` y ) <-> ( F ` x ) <_ ( ( F ` x ) + ( F ` y ) ) ) )
126 123 125 mpbid 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ y = ( 0g ` R ) ) -> ( F ` x ) <_ ( ( F ` x ) + ( F ` y ) ) )
127 122 126 eqbrtrd 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ y = ( 0g ` R ) ) -> ( F ` ( x ( +g ` R ) y ) ) <_ ( ( F ` x ) + ( F ` y ) ) )
128 88 3 syl 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ ( x =/= ( 0g ` R ) /\ y =/= ( 0g ` R ) ) ) -> .+ = ( +g ` R ) )
129 128 oveqd 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ ( x =/= ( 0g ` R ) /\ y =/= ( 0g ` R ) ) ) -> ( x .+ y ) = ( x ( +g ` R ) y ) )
130 129 fveq2d 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ ( x =/= ( 0g ` R ) /\ y =/= ( 0g ` R ) ) ) -> ( F ` ( x .+ y ) ) = ( F ` ( x ( +g ` R ) y ) ) )
131 88 94 97 99 101 11 syl122anc 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ ( x =/= ( 0g ` R ) /\ y =/= ( 0g ` R ) ) ) -> ( F ` ( x .+ y ) ) <_ ( ( F ` x ) + ( F ` y ) ) )
132 130 131 eqbrtrrd 
 |-  ( ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) /\ ( x =/= ( 0g ` R ) /\ y =/= ( 0g ` R ) ) ) -> ( F ` ( x ( +g ` R ) y ) ) <_ ( ( F ` x ) + ( F ` y ) ) )
133 117 127 132 pm2.61da2ne 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( F ` ( x ( +g ` R ) y ) ) <_ ( ( F ` x ) + ( F ` y ) ) )
134 104 133 jca 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) x. ( F ` y ) ) /\ ( F ` ( x ( +g ` R ) y ) ) <_ ( ( F ` x ) + ( F ` y ) ) ) )
135 134 3expia 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( y e. ( Base ` R ) -> ( ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) x. ( F ` y ) ) /\ ( F ` ( x ( +g ` R ) y ) ) <_ ( ( F ` x ) + ( F ` y ) ) ) ) )
136 135 ralrimiv 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> A. y e. ( Base ` R ) ( ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) x. ( F ` y ) ) /\ ( F ` ( x ( +g ` R ) y ) ) <_ ( ( F ` x ) + ( F ` y ) ) ) )
137 50 136 jca 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( ( ( F ` x ) = 0 <-> x = ( 0g ` R ) ) /\ A. y e. ( Base ` R ) ( ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) x. ( F ` y ) ) /\ ( F ` ( x ( +g ` R ) y ) ) <_ ( ( F ` x ) + ( F ` y ) ) ) ) )
138 137 ralrimiva 
 |-  ( ph -> A. x e. ( Base ` R ) ( ( ( F ` x ) = 0 <-> x = ( 0g ` R ) ) /\ A. y e. ( Base ` R ) ( ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) x. ( F ` y ) ) /\ ( F ` ( x ( +g ` R ) y ) ) <_ ( ( F ` x ) + ( F ` y ) ) ) ) )
139 eqid 
 |-  ( AbsVal ` R ) = ( AbsVal ` R )
140 139 56 108 57 58 isabv 
 |-  ( R e. Ring -> ( F e. ( AbsVal ` R ) <-> ( F : ( Base ` R ) --> ( 0 [,) +oo ) /\ A. x e. ( Base ` R ) ( ( ( F ` x ) = 0 <-> x = ( 0g ` R ) ) /\ A. y e. ( Base ` R ) ( ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) x. ( F ` y ) ) /\ ( F ` ( x ( +g ` R ) y ) ) <_ ( ( F ` x ) + ( F ` y ) ) ) ) ) ) )
141 6 140 syl 
 |-  ( ph -> ( F e. ( AbsVal ` R ) <-> ( F : ( Base ` R ) --> ( 0 [,) +oo ) /\ A. x e. ( Base ` R ) ( ( ( F ` x ) = 0 <-> x = ( 0g ` R ) ) /\ A. y e. ( Base ` R ) ( ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) x. ( F ` y ) ) /\ ( F ` ( x ( +g ` R ) y ) ) <_ ( ( F ` x ) + ( F ` y ) ) ) ) ) ) )
142 43 138 141 mpbir2and 
 |-  ( ph -> F e. ( AbsVal ` R ) )
143 142 1 eleqtrrd 
 |-  ( ph -> F e. A )