Step 
Hyp 
Ref 
Expression 
1 

abvf.a 
⊢ 𝐴 = ( AbsVal ‘ 𝑅 ) 
2 

abvf.b 
⊢ 𝐵 = ( Base ‘ 𝑅 ) 
3 

abvtri.p 
⊢ + = ( +_{g} ‘ 𝑅 ) 
4 
1

abvrcl 
⊢ ( 𝐹 ∈ 𝐴 → 𝑅 ∈ Ring ) 
5 

eqid 
⊢ ( ._{r} ‘ 𝑅 ) = ( ._{r} ‘ 𝑅 ) 
6 

eqid 
⊢ ( 0_{g} ‘ 𝑅 ) = ( 0_{g} ‘ 𝑅 ) 
7 
1 2 3 5 6

isabv 
⊢ ( 𝑅 ∈ Ring → ( 𝐹 ∈ 𝐴 ↔ ( 𝐹 : 𝐵 ⟶ ( 0 [,) +∞ ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0_{g} ‘ 𝑅 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 ( ._{r} ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) ) ) ) ) 
8 
4 7

syl 
⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ∈ 𝐴 ↔ ( 𝐹 : 𝐵 ⟶ ( 0 [,) +∞ ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0_{g} ‘ 𝑅 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 ( ._{r} ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) ) ) ) ) 
9 
8

ibi 
⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 : 𝐵 ⟶ ( 0 [,) +∞ ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0_{g} ‘ 𝑅 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 ( ._{r} ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) ) ) ) 
10 

simpr 
⊢ ( ( ( 𝐹 ‘ ( 𝑥 ( ._{r} ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) 
11 
10

ralimi 
⊢ ( ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 ( ._{r} ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) → ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) 
12 
11

adantl 
⊢ ( ( ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0_{g} ‘ 𝑅 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 ( ._{r} ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) ) → ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) 
13 
12

ralimi 
⊢ ( ∀ 𝑥 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0_{g} ‘ 𝑅 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 ( ._{r} ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) 
14 
9 13

simpl2im 
⊢ ( 𝐹 ∈ 𝐴 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) 
15 

fvoveq1 
⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑦 ) ) ) 
16 

fveq2 
⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) ) 
17 
16

oveq1d 
⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑦 ) ) ) 
18 
15 17

breq12d 
⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( 𝑋 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑦 ) ) ) ) 
19 

oveq2 
⊢ ( 𝑦 = 𝑌 → ( 𝑋 + 𝑦 ) = ( 𝑋 + 𝑌 ) ) 
20 
19

fveq2d 
⊢ ( 𝑦 = 𝑌 → ( 𝐹 ‘ ( 𝑋 + 𝑦 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑌 ) ) ) 
21 

fveq2 
⊢ ( 𝑦 = 𝑌 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑌 ) ) 
22 
21

oveq2d 
⊢ ( 𝑦 = 𝑌 → ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) 
23 
20 22

breq12d 
⊢ ( 𝑦 = 𝑌 → ( ( 𝐹 ‘ ( 𝑋 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( 𝑋 + 𝑌 ) ) ≤ ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) 
24 
18 23

rspc2v 
⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑌 ) ) ≤ ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) 
25 
14 24

syl5com 
⊢ ( 𝐹 ∈ 𝐴 → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑋 + 𝑌 ) ) ≤ ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) 
26 
25

3impib 
⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑋 + 𝑌 ) ) ≤ ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) 