Theorem abvpropd2

Description: Weaker version of abvpropd . (Contributed by Thierry Arnoux, 8-Nov-2017)

	Ref	Expression
Hypotheses	abvpropd2.1	|- ( ph -> ( Base ` K ) = ( Base ` L ) )
	abvpropd2.2	|- ( ph -> ( +g ` K ) = ( +g ` L ) )
	abvpropd2.3	|- ( ph -> ( .r ` K ) = ( .r ` L ) )
Assertion	abvpropd2	|- ( ph -> ( AbsVal ` K ) = ( AbsVal ` L ) )

Proof

Step	Hyp	Ref	Expression
1		abvpropd2.1	|- ( ph -> ( Base ` K ) = ( Base ` L ) )
2		abvpropd2.2	|- ( ph -> ( +g ` K ) = ( +g ` L ) )
3		abvpropd2.3	|- ( ph -> ( .r ` K ) = ( .r ` L ) )
4		eqidd	|- ( ph -> ( Base ` K ) = ( Base ` K ) )
5	2	oveqdr	|- ( ( ph /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
6	3	oveqdr	|- ( ( ph /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
7	4 1 5 6	abvpropd	|- ( ph -> ( AbsVal ` K ) = ( AbsVal ` L ) )