Theorem abvpropd

Description: If two structures have the same ring components, they have the same collection of absolute values. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	abvpropd.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
	abvpropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
	abvpropd.3	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
	abvpropd.4	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y$$
Assertion	abvpropd	$$⊢\phi \to \mathrm{AbsVal}\left(K\right)=\mathrm{AbsVal}\left(L\right)$$

Proof

Step	Hyp	Ref	Expression
1		abvpropd.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
2		abvpropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
3		abvpropd.3	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
4		abvpropd.4	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y$$
5	1 2 3 4	ringpropd	$$⊢\phi \to \left(K\in \mathrm{Ring}\leftrightarrow L\in \mathrm{Ring}\right)$$
6	1 2	eqtr3d	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_L$$
7	6	feq2d	$$⊢\phi \to \left(f:{\mathrm{Base}}_K⟶\left[0,\mathrm{+\infty }\right)\leftrightarrow f:{\mathrm{Base}}_L⟶\left[0,\mathrm{+\infty }\right)\right)$$
8	1 2 3	grpidpropd	$$⊢\phi \to 0_K=0_L$$
9	8	adantr	$$⊢\left(\phi \wedge x\in B\right)\to 0_K=0_L$$
10	9	eqeq2d	$$⊢\left(\phi \wedge x\in B\right)\to \left(x=0_K\leftrightarrow x=0_L\right)$$
11	10	bibi2d	$$⊢\left(\phi \wedge x\in B\right)\to \left(\left(f\left(x\right)=0\leftrightarrow x=0_K\right)\leftrightarrow \left(f\left(x\right)=0\leftrightarrow x=0_L\right)\right)$$
12	4	fveqeq2d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(f\left(x{\cdot }_{K}y\right)=f\left(x\right)f\left(y\right)\leftrightarrow f\left(x{\cdot }_{L}y\right)=f\left(x\right)f\left(y\right)\right)$$
13	3	fveq2d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to f\left(x{+}_{K}y\right)=f\left(x{+}_{L}y\right)$$
14	13	breq1d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(f\left(x{+}_{K}y\right)\le f\left(x\right)+f\left(y\right)\leftrightarrow f\left(x{+}_{L}y\right)\le f\left(x\right)+f\left(y\right)\right)$$
15	12 14	anbi12d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(\left(f\left(x{\cdot }_{K}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{K}y\right)\le f\left(x\right)+f\left(y\right)\right)\leftrightarrow \left(f\left(x{\cdot }_{L}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{L}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)$$
16	15	anassrs	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge y\in B\right)\to \left(\left(f\left(x{\cdot }_{K}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{K}y\right)\le f\left(x\right)+f\left(y\right)\right)\leftrightarrow \left(f\left(x{\cdot }_{L}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{L}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)$$
17	16	ralbidva	$$⊢\left(\phi \wedge x\in B\right)\to \left(\forall y\in B\left(f\left(x{\cdot }_{K}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{K}y\right)\le f\left(x\right)+f\left(y\right)\right)\leftrightarrow \forall y\in B\left(f\left(x{\cdot }_{L}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{L}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)$$
18	11 17	anbi12d	$$⊢\left(\phi \wedge x\in B\right)\to \left(\left(\left(f\left(x\right)=0\leftrightarrow x=0_K\right)\wedge \forall y\in B\left(f\left(x{\cdot }_{K}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{K}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\leftrightarrow \left(\left(f\left(x\right)=0\leftrightarrow x=0_L\right)\wedge \forall y\in B\left(f\left(x{\cdot }_{L}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{L}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right)$$
19	18	ralbidva	$$⊢\phi \to \left(\forall x\in B\left(\left(f\left(x\right)=0\leftrightarrow x=0_K\right)\wedge \forall y\in B\left(f\left(x{\cdot }_{K}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{K}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\leftrightarrow \forall x\in B\left(\left(f\left(x\right)=0\leftrightarrow x=0_L\right)\wedge \forall y\in B\left(f\left(x{\cdot }_{L}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{L}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right)$$
20	1	raleqdv	$$⊢\phi \to \left(\forall y\in B\left(f\left(x{\cdot }_{K}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{K}y\right)\le f\left(x\right)+f\left(y\right)\right)\leftrightarrow \forall y\in {\mathrm{Base}}_K\left(f\left(x{\cdot }_{K}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{K}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)$$
21	20	anbi2d	$$⊢\phi \to \left(\left(\left(f\left(x\right)=0\leftrightarrow x=0_K\right)\wedge \forall y\in B\left(f\left(x{\cdot }_{K}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{K}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\leftrightarrow \left(\left(f\left(x\right)=0\leftrightarrow x=0_K\right)\wedge \forall y\in {\mathrm{Base}}_K\left(f\left(x{\cdot }_{K}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{K}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right)$$
22	1 21	raleqbidv	$$⊢\phi \to \left(\forall x\in B\left(\left(f\left(x\right)=0\leftrightarrow x=0_K\right)\wedge \forall y\in B\left(f\left(x{\cdot }_{K}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{K}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\leftrightarrow \forall x\in {\mathrm{Base}}_K\left(\left(f\left(x\right)=0\leftrightarrow x=0_K\right)\wedge \forall y\in {\mathrm{Base}}_K\left(f\left(x{\cdot }_{K}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{K}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right)$$
23	2	raleqdv	$$⊢\phi \to \left(\forall y\in B\left(f\left(x{\cdot }_{L}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{L}y\right)\le f\left(x\right)+f\left(y\right)\right)\leftrightarrow \forall y\in {\mathrm{Base}}_L\left(f\left(x{\cdot }_{L}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{L}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)$$
24	23	anbi2d	$$⊢\phi \to \left(\left(\left(f\left(x\right)=0\leftrightarrow x=0_L\right)\wedge \forall y\in B\left(f\left(x{\cdot }_{L}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{L}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\leftrightarrow \left(\left(f\left(x\right)=0\leftrightarrow x=0_L\right)\wedge \forall y\in {\mathrm{Base}}_L\left(f\left(x{\cdot }_{L}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{L}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right)$$
25	2 24	raleqbidv	$$⊢\phi \to \left(\forall x\in B\left(\left(f\left(x\right)=0\leftrightarrow x=0_L\right)\wedge \forall y\in B\left(f\left(x{\cdot }_{L}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{L}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\leftrightarrow \forall x\in {\mathrm{Base}}_L\left(\left(f\left(x\right)=0\leftrightarrow x=0_L\right)\wedge \forall y\in {\mathrm{Base}}_L\left(f\left(x{\cdot }_{L}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{L}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right)$$
26	19 22 25	3bitr3d	$$⊢\phi \to \left(\forall x\in {\mathrm{Base}}_K\left(\left(f\left(x\right)=0\leftrightarrow x=0_K\right)\wedge \forall y\in {\mathrm{Base}}_K\left(f\left(x{\cdot }_{K}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{K}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\leftrightarrow \forall x\in {\mathrm{Base}}_L\left(\left(f\left(x\right)=0\leftrightarrow x=0_L\right)\wedge \forall y\in {\mathrm{Base}}_L\left(f\left(x{\cdot }_{L}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{L}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right)$$
27	7 26	anbi12d	$$⊢\phi \to \left(\left(f:{\mathrm{Base}}_K⟶\left[0,\mathrm{+\infty }\right)\wedge \forall x\in {\mathrm{Base}}_K\left(\left(f\left(x\right)=0\leftrightarrow x=0_K\right)\wedge \forall y\in {\mathrm{Base}}_K\left(f\left(x{\cdot }_{K}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{K}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right)\leftrightarrow \left(f:{\mathrm{Base}}_L⟶\left[0,\mathrm{+\infty }\right)\wedge \forall x\in {\mathrm{Base}}_L\left(\left(f\left(x\right)=0\leftrightarrow x=0_L\right)\wedge \forall y\in {\mathrm{Base}}_L\left(f\left(x{\cdot }_{L}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{L}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right)\right)$$
28	5 27	anbi12d	$$⊢\phi \to \left(\left(K\in \mathrm{Ring}\wedge \left(f:{\mathrm{Base}}_K⟶\left[0,\mathrm{+\infty }\right)\wedge \forall x\in {\mathrm{Base}}_K\left(\left(f\left(x\right)=0\leftrightarrow x=0_K\right)\wedge \forall y\in {\mathrm{Base}}_K\left(f\left(x{\cdot }_{K}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{K}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right)\right)\leftrightarrow \left(L\in \mathrm{Ring}\wedge \left(f:{\mathrm{Base}}_L⟶\left[0,\mathrm{+\infty }\right)\wedge \forall x\in {\mathrm{Base}}_L\left(\left(f\left(x\right)=0\leftrightarrow x=0_L\right)\wedge \forall y\in {\mathrm{Base}}_L\left(f\left(x{\cdot }_{L}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{L}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right)\right)\right)$$
29		eqid	$$⊢\mathrm{AbsVal}\left(K\right)=\mathrm{AbsVal}\left(K\right)$$
30	29	abvrcl	$$⊢f\in \mathrm{AbsVal}\left(K\right)\to K\in \mathrm{Ring}$$
31		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
32		eqid	$$⊢{+}_K={+}_K$$
33		eqid	$$⊢{\cdot }_K={\cdot }_K$$
34		eqid	$$⊢0_K=0_K$$
35	29 31 32 33 34	isabv	$$⊢K\in \mathrm{Ring}\to \left(f\in \mathrm{AbsVal}\left(K\right)\leftrightarrow \left(f:{\mathrm{Base}}_K⟶\left[0,\mathrm{+\infty }\right)\wedge \forall x\in {\mathrm{Base}}_K\left(\left(f\left(x\right)=0\leftrightarrow x=0_K\right)\wedge \forall y\in {\mathrm{Base}}_K\left(f\left(x{\cdot }_{K}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{K}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right)\right)$$
36	30 35	biadanii	$$⊢f\in \mathrm{AbsVal}\left(K\right)\leftrightarrow \left(K\in \mathrm{Ring}\wedge \left(f:{\mathrm{Base}}_K⟶\left[0,\mathrm{+\infty }\right)\wedge \forall x\in {\mathrm{Base}}_K\left(\left(f\left(x\right)=0\leftrightarrow x=0_K\right)\wedge \forall y\in {\mathrm{Base}}_K\left(f\left(x{\cdot }_{K}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{K}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right)\right)$$
37		eqid	$$⊢\mathrm{AbsVal}\left(L\right)=\mathrm{AbsVal}\left(L\right)$$
38	37	abvrcl	$$⊢f\in \mathrm{AbsVal}\left(L\right)\to L\in \mathrm{Ring}$$
39		eqid	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_L$$
40		eqid	$$⊢{+}_L={+}_L$$
41		eqid	$$⊢{\cdot }_L={\cdot }_L$$
42		eqid	$$⊢0_L=0_L$$
43	37 39 40 41 42	isabv	$$⊢L\in \mathrm{Ring}\to \left(f\in \mathrm{AbsVal}\left(L\right)\leftrightarrow \left(f:{\mathrm{Base}}_L⟶\left[0,\mathrm{+\infty }\right)\wedge \forall x\in {\mathrm{Base}}_L\left(\left(f\left(x\right)=0\leftrightarrow x=0_L\right)\wedge \forall y\in {\mathrm{Base}}_L\left(f\left(x{\cdot }_{L}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{L}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right)\right)$$
44	38 43	biadanii	$$⊢f\in \mathrm{AbsVal}\left(L\right)\leftrightarrow \left(L\in \mathrm{Ring}\wedge \left(f:{\mathrm{Base}}_L⟶\left[0,\mathrm{+\infty }\right)\wedge \forall x\in {\mathrm{Base}}_L\left(\left(f\left(x\right)=0\leftrightarrow x=0_L\right)\wedge \forall y\in {\mathrm{Base}}_L\left(f\left(x{\cdot }_{L}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{L}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right)\right)$$
45	28 36 44	3bitr4g	$$⊢\phi \to \left(f\in \mathrm{AbsVal}\left(K\right)\leftrightarrow f\in \mathrm{AbsVal}\left(L\right)\right)$$
46	45	eqrdv	$$⊢\phi \to \mathrm{AbsVal}\left(K\right)=\mathrm{AbsVal}\left(L\right)$$