Theorem abvmul

Description: An absolute value distributes under multiplication. (Contributed by Mario Carneiro, 8-Sep-2014)

	Ref	Expression
Hypotheses	abvf.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
	abvf.b	$$⊢B={\mathrm{Base}}_R$$
	abvmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	abvmul	$$⊢\left(F\in A\wedge X\in B\wedge Y\in B\right)\to F\left(X\underset{\dot{}}{·}Y\right)=F\left(X\right)F\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		abvf.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
2		abvf.b	$$⊢B={\mathrm{Base}}_R$$
3		abvmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4	1	abvrcl	$$⊢F\in A\to R\in \mathrm{Ring}$$
5		eqid	$$⊢{+}_R={+}_R$$
6		eqid	$$⊢0_R=0_R$$
7	1 2 5 3 6	isabv	$$⊢R\in \mathrm{Ring}\to \left(F\in A\leftrightarrow \left(F:B⟶\left[0,\mathrm{+\infty }\right)\wedge \forall x\in B\left(\left(F\left(x\right)=0\leftrightarrow x=0_R\right)\wedge \forall y\in B\left(F\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)F\left(y\right)\wedge F\left(x{+}_{R}y\right)\le F\left(x\right)+F\left(y\right)\right)\right)\right)\right)$$
8	4 7	syl	$$⊢F\in A\to \left(F\in A\leftrightarrow \left(F:B⟶\left[0,\mathrm{+\infty }\right)\wedge \forall x\in B\left(\left(F\left(x\right)=0\leftrightarrow x=0_R\right)\wedge \forall y\in B\left(F\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)F\left(y\right)\wedge F\left(x{+}_{R}y\right)\le F\left(x\right)+F\left(y\right)\right)\right)\right)\right)$$
9	8	ibi	$$⊢F\in A\to \left(F:B⟶\left[0,\mathrm{+\infty }\right)\wedge \forall x\in B\left(\left(F\left(x\right)=0\leftrightarrow x=0_R\right)\wedge \forall y\in B\left(F\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)F\left(y\right)\wedge F\left(x{+}_{R}y\right)\le F\left(x\right)+F\left(y\right)\right)\right)\right)$$
10		simpl	$$⊢\left(F\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)F\left(y\right)\wedge F\left(x{+}_{R}y\right)\le F\left(x\right)+F\left(y\right)\right)\to F\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)F\left(y\right)$$
11	10	ralimi	$$⊢\forall y\in B\left(F\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)F\left(y\right)\wedge F\left(x{+}_{R}y\right)\le F\left(x\right)+F\left(y\right)\right)\to \forall y\in BF\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)F\left(y\right)$$
12	11	adantl	$$⊢\left(\left(F\left(x\right)=0\leftrightarrow x=0_R\right)\wedge \forall y\in B\left(F\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)F\left(y\right)\wedge F\left(x{+}_{R}y\right)\le F\left(x\right)+F\left(y\right)\right)\right)\to \forall y\in BF\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)F\left(y\right)$$
13	12	ralimi	$$⊢\forall x\in B\left(\left(F\left(x\right)=0\leftrightarrow x=0_R\right)\wedge \forall y\in B\left(F\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)F\left(y\right)\wedge F\left(x{+}_{R}y\right)\le F\left(x\right)+F\left(y\right)\right)\right)\to \forall x\in B\forall y\in BF\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)F\left(y\right)$$
14	9 13	simpl2im	$$⊢F\in A\to \forall x\in B\forall y\in BF\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)F\left(y\right)$$
15		fvoveq1	$$⊢x=X\to F\left(x\underset{\dot{}}{·}y\right)=F\left(X\underset{\dot{}}{·}y\right)$$
16		fveq2	$$⊢x=X\to F\left(x\right)=F\left(X\right)$$
17	16	oveq1d	$$⊢x=X\to F\left(x\right)F\left(y\right)=F\left(X\right)F\left(y\right)$$
18	15 17	eqeq12d	$$⊢x=X\to \left(F\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)F\left(y\right)\leftrightarrow F\left(X\underset{\dot{}}{·}y\right)=F\left(X\right)F\left(y\right)\right)$$
19		oveq2	$$⊢y=Y\to X\underset{\dot{}}{·}y=X\underset{\dot{}}{·}Y$$
20	19	fveq2d	$$⊢y=Y\to F\left(X\underset{\dot{}}{·}y\right)=F\left(X\underset{\dot{}}{·}Y\right)$$
21		fveq2	$$⊢y=Y\to F\left(y\right)=F\left(Y\right)$$
22	21	oveq2d	$$⊢y=Y\to F\left(X\right)F\left(y\right)=F\left(X\right)F\left(Y\right)$$
23	20 22	eqeq12d	$$⊢y=Y\to \left(F\left(X\underset{\dot{}}{·}y\right)=F\left(X\right)F\left(y\right)\leftrightarrow F\left(X\underset{\dot{}}{·}Y\right)=F\left(X\right)F\left(Y\right)\right)$$
24	18 23	rspc2v	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\forall x\in B\forall y\in BF\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)F\left(y\right)\to F\left(X\underset{\dot{}}{·}Y\right)=F\left(X\right)F\left(Y\right)\right)$$
25	14 24	syl5com	$$⊢F\in A\to \left(\left(X\in B\wedge Y\in B\right)\to F\left(X\underset{\dot{}}{·}Y\right)=F\left(X\right)F\left(Y\right)\right)$$
26	25	3impib	$$⊢\left(F\in A\wedge X\in B\wedge Y\in B\right)\to F\left(X\underset{\dot{}}{·}Y\right)=F\left(X\right)F\left(Y\right)$$