# 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 ffvelrnda
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 ) )`
` |-  ( ( 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`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( F ` ( 0g ` R ) ) = 0 )`
` |-  ( ( ( 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 ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> F : ( Base ` R ) --> RR )`
66 65 55 ffvelrnd
` |-  ( ( 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 )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( ( 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 ffvelrnd
` |-  ( ( 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 )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( 0 <_ ( F ` x ) <-> ( F ` y ) <_ ( ( F ` x ) + ( F ` y ) ) ) )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( 0 <_ ( F ` y ) <-> ( F ` x ) <_ ( ( F ` x ) + ( F ` y ) ) ) )`
` |-  ( ( ( 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 )`