Theorem abvpropd2

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

	Ref	Expression
Hypotheses	abvpropd2.1	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_L$$
	abvpropd2.2	$$⊢\phi \to {+}_K={+}_L$$
	abvpropd2.3	$$⊢\phi \to {\cdot }_K={\cdot }_L$$
Assertion	abvpropd2	$$⊢\phi \to \mathrm{AbsVal}\left(K\right)=\mathrm{AbsVal}\left(L\right)$$

Proof

Step	Hyp	Ref	Expression
1		abvpropd2.1	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_L$$
2		abvpropd2.2	$$⊢\phi \to {+}_K={+}_L$$
3		abvpropd2.3	$$⊢\phi \to {\cdot }_K={\cdot }_L$$
4		eqidd	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_K$$
5	2	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_K\wedge y\in {\mathrm{Base}}_K\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
6	3	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_K\wedge y\in {\mathrm{Base}}_K\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y$$
7	4 1 5 6	abvpropd	$$⊢\phi \to \mathrm{AbsVal}\left(K\right)=\mathrm{AbsVal}\left(L\right)$$