Description: Weaker version of abvpropd . (Contributed by Thierry Arnoux, 8-Nov-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | abvpropd2.1 | ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) ) | |
abvpropd2.2 | ⊢ ( 𝜑 → ( +g ‘ 𝐾 ) = ( +g ‘ 𝐿 ) ) | ||
abvpropd2.3 | ⊢ ( 𝜑 → ( .r ‘ 𝐾 ) = ( .r ‘ 𝐿 ) ) | ||
Assertion | abvpropd2 | ⊢ ( 𝜑 → ( AbsVal ‘ 𝐾 ) = ( AbsVal ‘ 𝐿 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abvpropd2.1 | ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) ) | |
2 | abvpropd2.2 | ⊢ ( 𝜑 → ( +g ‘ 𝐾 ) = ( +g ‘ 𝐿 ) ) | |
3 | abvpropd2.3 | ⊢ ( 𝜑 → ( .r ‘ 𝐾 ) = ( .r ‘ 𝐿 ) ) | |
4 | eqidd | ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) ) | |
5 | 2 | oveqdr | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ) |
6 | 3 | oveqdr | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) ) |
7 | 4 1 5 6 | abvpropd | ⊢ ( 𝜑 → ( AbsVal ‘ 𝐾 ) = ( AbsVal ‘ 𝐿 ) ) |