# Metamath Proof Explorer

## Theorem abvpropd

Description: If two structures have the same ring components, they have the same collection of absolute values. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses abvpropd.1 ( 𝜑𝐵 = ( Base ‘ 𝐾 ) )
abvpropd.2 ( 𝜑𝐵 = ( Base ‘ 𝐿 ) )
abvpropd.3 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 ) )
abvpropd.4 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( .r𝐿 ) 𝑦 ) )
Assertion abvpropd ( 𝜑 → ( AbsVal ‘ 𝐾 ) = ( AbsVal ‘ 𝐿 ) )

### Proof

Step Hyp Ref Expression
1 abvpropd.1 ( 𝜑𝐵 = ( Base ‘ 𝐾 ) )
2 abvpropd.2 ( 𝜑𝐵 = ( Base ‘ 𝐿 ) )
3 abvpropd.3 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 ) )
4 abvpropd.4 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( .r𝐿 ) 𝑦 ) )
5 1 2 3 4 ringpropd ( 𝜑 → ( 𝐾 ∈ Ring ↔ 𝐿 ∈ Ring ) )
6 1 2 eqtr3d ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
7 6 feq2d ( 𝜑 → ( 𝑓 : ( Base ‘ 𝐾 ) ⟶ ( 0 [,) +∞ ) ↔ 𝑓 : ( Base ‘ 𝐿 ) ⟶ ( 0 [,) +∞ ) ) )
8 1 2 3 grpidpropd ( 𝜑 → ( 0g𝐾 ) = ( 0g𝐿 ) )
9 8 adantr ( ( 𝜑𝑥𝐵 ) → ( 0g𝐾 ) = ( 0g𝐿 ) )
10 9 eqeq2d ( ( 𝜑𝑥𝐵 ) → ( 𝑥 = ( 0g𝐾 ) ↔ 𝑥 = ( 0g𝐿 ) ) )
11 10 bibi2d ( ( 𝜑𝑥𝐵 ) → ( ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝐾 ) ) ↔ ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝐿 ) ) ) )
12 4 fveqeq2d ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝑓 ‘ ( 𝑥 ( .r𝐾 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ↔ ( 𝑓 ‘ ( 𝑥 ( .r𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ) )
13 3 fveq2d ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑓 ‘ ( 𝑥 ( +g𝐾 ) 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) )
14 13 breq1d ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝑓 ‘ ( 𝑥 ( +g𝐾 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ↔ ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) )
15 12 14 anbi12d ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( ( 𝑓 ‘ ( 𝑥 ( .r𝐾 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐾 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ↔ ( ( 𝑓 ‘ ( 𝑥 ( .r𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) )
16 15 anassrs ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑦𝐵 ) → ( ( ( 𝑓 ‘ ( 𝑥 ( .r𝐾 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐾 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ↔ ( ( 𝑓 ‘ ( 𝑥 ( .r𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) )
17 16 ralbidva ( ( 𝜑𝑥𝐵 ) → ( ∀ 𝑦𝐵 ( ( 𝑓 ‘ ( 𝑥 ( .r𝐾 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐾 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ↔ ∀ 𝑦𝐵 ( ( 𝑓 ‘ ( 𝑥 ( .r𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) )
18 11 17 anbi12d ( ( 𝜑𝑥𝐵 ) → ( ( ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝐾 ) ) ∧ ∀ 𝑦𝐵 ( ( 𝑓 ‘ ( 𝑥 ( .r𝐾 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐾 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) ↔ ( ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝐿 ) ) ∧ ∀ 𝑦𝐵 ( ( 𝑓 ‘ ( 𝑥 ( .r𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) ) )
19 18 ralbidva ( 𝜑 → ( ∀ 𝑥𝐵 ( ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝐾 ) ) ∧ ∀ 𝑦𝐵 ( ( 𝑓 ‘ ( 𝑥 ( .r𝐾 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐾 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) ↔ ∀ 𝑥𝐵 ( ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝐿 ) ) ∧ ∀ 𝑦𝐵 ( ( 𝑓 ‘ ( 𝑥 ( .r𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) ) )
20 1 raleqdv ( 𝜑 → ( ∀ 𝑦𝐵 ( ( 𝑓 ‘ ( 𝑥 ( .r𝐾 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐾 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( ( 𝑓 ‘ ( 𝑥 ( .r𝐾 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐾 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) )
21 20 anbi2d ( 𝜑 → ( ( ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝐾 ) ) ∧ ∀ 𝑦𝐵 ( ( 𝑓 ‘ ( 𝑥 ( .r𝐾 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐾 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) ↔ ( ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝐾 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( ( 𝑓 ‘ ( 𝑥 ( .r𝐾 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐾 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) ) )
22 1 21 raleqbidv ( 𝜑 → ( ∀ 𝑥𝐵 ( ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝐾 ) ) ∧ ∀ 𝑦𝐵 ( ( 𝑓 ‘ ( 𝑥 ( .r𝐾 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐾 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝐾 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( ( 𝑓 ‘ ( 𝑥 ( .r𝐾 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐾 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) ) )
23 2 raleqdv ( 𝜑 → ( ∀ 𝑦𝐵 ( ( 𝑓 ‘ ( 𝑥 ( .r𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( ( 𝑓 ‘ ( 𝑥 ( .r𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) )
24 23 anbi2d ( 𝜑 → ( ( ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝐿 ) ) ∧ ∀ 𝑦𝐵 ( ( 𝑓 ‘ ( 𝑥 ( .r𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) ↔ ( ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝐿 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( ( 𝑓 ‘ ( 𝑥 ( .r𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) ) )
25 2 24 raleqbidv ( 𝜑 → ( ∀ 𝑥𝐵 ( ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝐿 ) ) ∧ ∀ 𝑦𝐵 ( ( 𝑓 ‘ ( 𝑥 ( .r𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝐿 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( ( 𝑓 ‘ ( 𝑥 ( .r𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) ) )
26 19 22 25 3bitr3d ( 𝜑 → ( ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝐾 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( ( 𝑓 ‘ ( 𝑥 ( .r𝐾 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐾 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝐿 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( ( 𝑓 ‘ ( 𝑥 ( .r𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) ) )
27 7 26 anbi12d ( 𝜑 → ( ( 𝑓 : ( Base ‘ 𝐾 ) ⟶ ( 0 [,) +∞ ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝐾 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( ( 𝑓 ‘ ( 𝑥 ( .r𝐾 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐾 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) ) ↔ ( 𝑓 : ( Base ‘ 𝐿 ) ⟶ ( 0 [,) +∞ ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝐿 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( ( 𝑓 ‘ ( 𝑥 ( .r𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) ) ) )
28 5 27 anbi12d ( 𝜑 → ( ( 𝐾 ∈ Ring ∧ ( 𝑓 : ( Base ‘ 𝐾 ) ⟶ ( 0 [,) +∞ ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝐾 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( ( 𝑓 ‘ ( 𝑥 ( .r𝐾 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐾 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) ) ) ↔ ( 𝐿 ∈ Ring ∧ ( 𝑓 : ( Base ‘ 𝐿 ) ⟶ ( 0 [,) +∞ ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝐿 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( ( 𝑓 ‘ ( 𝑥 ( .r𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) ) ) ) )
29 eqid ( AbsVal ‘ 𝐾 ) = ( AbsVal ‘ 𝐾 )
30 29 abvrcl ( 𝑓 ∈ ( AbsVal ‘ 𝐾 ) → 𝐾 ∈ Ring )
31 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
32 eqid ( +g𝐾 ) = ( +g𝐾 )
33 eqid ( .r𝐾 ) = ( .r𝐾 )
34 eqid ( 0g𝐾 ) = ( 0g𝐾 )
35 29 31 32 33 34 isabv ( 𝐾 ∈ Ring → ( 𝑓 ∈ ( AbsVal ‘ 𝐾 ) ↔ ( 𝑓 : ( Base ‘ 𝐾 ) ⟶ ( 0 [,) +∞ ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝐾 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( ( 𝑓 ‘ ( 𝑥 ( .r𝐾 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐾 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) ) ) )
36 30 35 biadanii ( 𝑓 ∈ ( AbsVal ‘ 𝐾 ) ↔ ( 𝐾 ∈ Ring ∧ ( 𝑓 : ( Base ‘ 𝐾 ) ⟶ ( 0 [,) +∞ ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝐾 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( ( 𝑓 ‘ ( 𝑥 ( .r𝐾 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐾 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) ) ) )
37 eqid ( AbsVal ‘ 𝐿 ) = ( AbsVal ‘ 𝐿 )
38 37 abvrcl ( 𝑓 ∈ ( AbsVal ‘ 𝐿 ) → 𝐿 ∈ Ring )
39 eqid ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
40 eqid ( +g𝐿 ) = ( +g𝐿 )
41 eqid ( .r𝐿 ) = ( .r𝐿 )
42 eqid ( 0g𝐿 ) = ( 0g𝐿 )
43 37 39 40 41 42 isabv ( 𝐿 ∈ Ring → ( 𝑓 ∈ ( AbsVal ‘ 𝐿 ) ↔ ( 𝑓 : ( Base ‘ 𝐿 ) ⟶ ( 0 [,) +∞ ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝐿 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( ( 𝑓 ‘ ( 𝑥 ( .r𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) ) ) )
44 38 43 biadanii ( 𝑓 ∈ ( AbsVal ‘ 𝐿 ) ↔ ( 𝐿 ∈ Ring ∧ ( 𝑓 : ( Base ‘ 𝐿 ) ⟶ ( 0 [,) +∞ ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝐿 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( ( 𝑓 ‘ ( 𝑥 ( .r𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) ) ) )
45 28 36 44 3bitr4g ( 𝜑 → ( 𝑓 ∈ ( AbsVal ‘ 𝐾 ) ↔ 𝑓 ∈ ( AbsVal ‘ 𝐿 ) ) )
46 45 eqrdv ( 𝜑 → ( AbsVal ‘ 𝐾 ) = ( AbsVal ‘ 𝐿 ) )