Metamath Proof Explorer


Theorem abvpropd2

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

Proof

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