Theorem nmpropd2

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

	Ref	Expression
Hypotheses	nmpropd2.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
	nmpropd2.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
	nmpropd2.3	$$⊢\phi \to K\in \mathrm{Grp}$$
	nmpropd2.4	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
	nmpropd2.5	$$⊢\phi \to {\mathrm{dist}\left(K\right)\upharpoonright }_{\left(B\times B\right)}={\mathrm{dist}\left(L\right)\upharpoonright }_{\left(B\times B\right)}$$
Assertion	nmpropd2	$$⊢\phi \to \mathrm{norm}\left(K\right)=\mathrm{norm}\left(L\right)$$

Proof

Step	Hyp	Ref	Expression
1		nmpropd2.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
2		nmpropd2.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
3		nmpropd2.3	$$⊢\phi \to K\in \mathrm{Grp}$$
4		nmpropd2.4	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
5		nmpropd2.5	$$⊢\phi \to {\mathrm{dist}\left(K\right)\upharpoonright }_{\left(B\times B\right)}={\mathrm{dist}\left(L\right)\upharpoonright }_{\left(B\times B\right)}$$
6	1 2	eqtr3d	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_L$$
7	1	sqxpeqd	$$⊢\phi \to B\times B={\mathrm{Base}}_K\times {\mathrm{Base}}_K$$
8	7	reseq2d	$$⊢\phi \to {\mathrm{dist}\left(K\right)\upharpoonright }_{\left(B\times B\right)}={\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}$$
9	5 8	eqtr3d	$$⊢\phi \to {\mathrm{dist}\left(L\right)\upharpoonright }_{\left(B\times B\right)}={\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}$$
10	2	sqxpeqd	$$⊢\phi \to B\times B={\mathrm{Base}}_L\times {\mathrm{Base}}_L$$
11	10	reseq2d	$$⊢\phi \to {\mathrm{dist}\left(L\right)\upharpoonright }_{\left(B\times B\right)}={\mathrm{dist}\left(L\right)\upharpoonright }_{\left({\mathrm{Base}}_L\times {\mathrm{Base}}_L\right)}$$
12	9 11	eqtr3d	$$⊢\phi \to {\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}={\mathrm{dist}\left(L\right)\upharpoonright }_{\left({\mathrm{Base}}_L\times {\mathrm{Base}}_L\right)}$$
13		eqidd	$$⊢\phi \to a=a$$
14	1 2 4	grpidpropd	$$⊢\phi \to 0_K=0_L$$
15	12 13 14	oveq123d	$$⊢\phi \to a\left({\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}\right)0_K=a\left({\mathrm{dist}\left(L\right)\upharpoonright }_{\left({\mathrm{Base}}_L\times {\mathrm{Base}}_L\right)}\right)0_L$$
16	6 15	mpteq12dv	$$⊢\phi \to \left(a\in {\mathrm{Base}}_K⟼a\left({\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}\right)0_K\right)=\left(a\in {\mathrm{Base}}_L⟼a\left({\mathrm{dist}\left(L\right)\upharpoonright }_{\left({\mathrm{Base}}_L\times {\mathrm{Base}}_L\right)}\right)0_L\right)$$
17		eqid	$$⊢\mathrm{norm}\left(K\right)=\mathrm{norm}\left(K\right)$$
18		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
19		eqid	$$⊢0_K=0_K$$
20		eqid	$$⊢\mathrm{dist}\left(K\right)=\mathrm{dist}\left(K\right)$$
21		eqid	$$⊢{\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}={\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}$$
22	17 18 19 20 21	nmfval2	$$⊢K\in \mathrm{Grp}\to \mathrm{norm}\left(K\right)=\left(a\in {\mathrm{Base}}_K⟼a\left({\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}\right)0_K\right)$$
23	3 22	syl	$$⊢\phi \to \mathrm{norm}\left(K\right)=\left(a\in {\mathrm{Base}}_K⟼a\left({\mathrm{dist}\left(K\right)\upharpoonright }_{\left({\mathrm{Base}}_K\times {\mathrm{Base}}_K\right)}\right)0_K\right)$$
24	1 2 4	grppropd	$$⊢\phi \to \left(K\in \mathrm{Grp}\leftrightarrow L\in \mathrm{Grp}\right)$$
25	3 24	mpbid	$$⊢\phi \to L\in \mathrm{Grp}$$
26		eqid	$$⊢\mathrm{norm}\left(L\right)=\mathrm{norm}\left(L\right)$$
27		eqid	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_L$$
28		eqid	$$⊢0_L=0_L$$
29		eqid	$$⊢\mathrm{dist}\left(L\right)=\mathrm{dist}\left(L\right)$$
30		eqid	$$⊢{\mathrm{dist}\left(L\right)\upharpoonright }_{\left({\mathrm{Base}}_L\times {\mathrm{Base}}_L\right)}={\mathrm{dist}\left(L\right)\upharpoonright }_{\left({\mathrm{Base}}_L\times {\mathrm{Base}}_L\right)}$$
31	26 27 28 29 30	nmfval2	$$⊢L\in \mathrm{Grp}\to \mathrm{norm}\left(L\right)=\left(a\in {\mathrm{Base}}_L⟼a\left({\mathrm{dist}\left(L\right)\upharpoonright }_{\left({\mathrm{Base}}_L\times {\mathrm{Base}}_L\right)}\right)0_L\right)$$
32	25 31	syl	$$⊢\phi \to \mathrm{norm}\left(L\right)=\left(a\in {\mathrm{Base}}_L⟼a\left({\mathrm{dist}\left(L\right)\upharpoonright }_{\left({\mathrm{Base}}_L\times {\mathrm{Base}}_L\right)}\right)0_L\right)$$
33	16 23 32	3eqtr4d	$$⊢\phi \to \mathrm{norm}\left(K\right)=\mathrm{norm}\left(L\right)$$