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