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 ‘ 𝐿 ) )