Metamath Proof Explorer

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)$