Theorem mulcompr

Description: Multiplication of positive reals is commutative. Proposition 9-3.7(ii) of Gleason p. 124. (Contributed by NM, 19-Nov-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	mulcompr	$$⊢A{\cdot }_{𝑷}B=B{\cdot }_{𝑷}A$$

Proof

Step	Hyp	Ref	Expression
1		mpv	$$⊢\left(A\in 𝑷\wedge B\in 𝑷\right)\to A{\cdot }_{𝑷}B=\left\{x|\exists z\in A\exists y\in Bx=z{\cdot }_{𝑸}y\right\}$$
2		mpv	$$⊢\left(B\in 𝑷\wedge A\in 𝑷\right)\to B{\cdot }_{𝑷}A=\left\{x|\exists y\in B\exists z\in Ax=y{\cdot }_{𝑸}z\right\}$$
3		mulcomnq	$$⊢y{\cdot }_{𝑸}z=z{\cdot }_{𝑸}y$$
4	3	eqeq2i	$$⊢x=y{\cdot }_{𝑸}z\leftrightarrow x=z{\cdot }_{𝑸}y$$
5	4	2rexbii	$$⊢\exists y\in B\exists z\in Ax=y{\cdot }_{𝑸}z\leftrightarrow \exists y\in B\exists z\in Ax=z{\cdot }_{𝑸}y$$
6		rexcom	$$⊢\exists y\in B\exists z\in Ax=z{\cdot }_{𝑸}y\leftrightarrow \exists z\in A\exists y\in Bx=z{\cdot }_{𝑸}y$$
7	5 6	bitri	$$⊢\exists y\in B\exists z\in Ax=y{\cdot }_{𝑸}z\leftrightarrow \exists z\in A\exists y\in Bx=z{\cdot }_{𝑸}y$$
8	7	abbii	$$⊢\left\{x|\exists y\in B\exists z\in Ax=y{\cdot }_{𝑸}z\right\}=\left\{x|\exists z\in A\exists y\in Bx=z{\cdot }_{𝑸}y\right\}$$
9	2 8	eqtrdi	$$⊢\left(B\in 𝑷\wedge A\in 𝑷\right)\to B{\cdot }_{𝑷}A=\left\{x|\exists z\in A\exists y\in Bx=z{\cdot }_{𝑸}y\right\}$$
10	9	ancoms	$$⊢\left(A\in 𝑷\wedge B\in 𝑷\right)\to B{\cdot }_{𝑷}A=\left\{x|\exists z\in A\exists y\in Bx=z{\cdot }_{𝑸}y\right\}$$
11	1 10	eqtr4d	$$⊢\left(A\in 𝑷\wedge B\in 𝑷\right)\to A{\cdot }_{𝑷}B=B{\cdot }_{𝑷}A$$
12		dmmp	$$⊢\mathrm{dom}{\cdot }_{𝑷}=𝑷\times 𝑷$$
13	12	ndmovcom	$$⊢\neg \left(A\in 𝑷\wedge B\in 𝑷\right)\to A{\cdot }_{𝑷}B=B{\cdot }_{𝑷}A$$
14	11 13	pm2.61i	$$⊢A{\cdot }_{𝑷}B=B{\cdot }_{𝑷}A$$