Theorem nmpropd

Description: Weak property deduction for a norm. (Contributed by Mario Carneiro, 4-Oct-2015)

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

Proof

Step	Hyp	Ref	Expression
1		nmpropd.1	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_L$$
2		nmpropd.2	$$⊢\phi \to {+}_K={+}_L$$
3		nmpropd.3	$$⊢\phi \to \mathrm{dist}\left(K\right)=\mathrm{dist}\left(L\right)$$
4		eqidd	$$⊢\phi \to x=x$$
5		eqidd	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_K$$
6	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$$
7	5 1 6	grpidpropd	$$⊢\phi \to 0_K=0_L$$
8	3 4 7	oveq123d	$$⊢\phi \to x\mathrm{dist}\left(K\right)0_K=x\mathrm{dist}\left(L\right)0_L$$
9	1 8	mpteq12dv	$$⊢\phi \to \left(x\in {\mathrm{Base}}_K⟼x\mathrm{dist}\left(K\right)0_K\right)=\left(x\in {\mathrm{Base}}_L⟼x\mathrm{dist}\left(L\right)0_L\right)$$
10		eqid	$$⊢\mathrm{norm}\left(K\right)=\mathrm{norm}\left(K\right)$$
11		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
12		eqid	$$⊢0_K=0_K$$
13		eqid	$$⊢\mathrm{dist}\left(K\right)=\mathrm{dist}\left(K\right)$$
14	10 11 12 13	nmfval	$$⊢\mathrm{norm}\left(K\right)=\left(x\in {\mathrm{Base}}_K⟼x\mathrm{dist}\left(K\right)0_K\right)$$
15		eqid	$$⊢\mathrm{norm}\left(L\right)=\mathrm{norm}\left(L\right)$$
16		eqid	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_L$$
17		eqid	$$⊢0_L=0_L$$
18		eqid	$$⊢\mathrm{dist}\left(L\right)=\mathrm{dist}\left(L\right)$$
19	15 16 17 18	nmfval	$$⊢\mathrm{norm}\left(L\right)=\left(x\in {\mathrm{Base}}_L⟼x\mathrm{dist}\left(L\right)0_L\right)$$
20	9 14 19	3eqtr4g	$$⊢\phi \to \mathrm{norm}\left(K\right)=\mathrm{norm}\left(L\right)$$