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 ⊢ ( 𝜑 → 𝐴 = ( AbsVal ‘ 𝑅 ) )
isabvd.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
isabvd.p ⊢ ( 𝜑 → + = ( +g ‘ 𝑅 ) )
isabvd.t ⊢ ( 𝜑 → · = ( .r ‘ 𝑅 ) )
isabvd.z ⊢ ( 𝜑 → 0 = ( 0g ‘ 𝑅 ) )
isabvd.1 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
isabvd.2 ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ℝ )
isabvd.3 ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = 0 )
isabvd.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) → 0 < ( 𝐹 ‘ 𝑥 ) )
isabvd.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) )
isabvd.6 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) )
Assertion isabvd ( 𝜑 → 𝐹 ∈ 𝐴 )

Proof

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