Theorem addcompr

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

	Ref	Expression
Assertion	addcompr	$$⊢A{+}_{𝑷}B=B{+}_{𝑷}A$$

Proof

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