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	⊢ ( 𝐴 +P 𝐵 ) = ( 𝐵 +P 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		plpv	⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 +P 𝐵 ) = { 𝑥 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝑧 +Q 𝑦 ) } )
2		plpv	⊢ ( ( 𝐵 ∈ P ∧ 𝐴 ∈ P ) → ( 𝐵 +P 𝐴 ) = { 𝑥 ∣ ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑦 +Q 𝑧 ) } )
3		addcomnq	⊢ ( 𝑦 +Q 𝑧 ) = ( 𝑧 +Q 𝑦 )
4	3	eqeq2i	⊢ ( 𝑥 = ( 𝑦 +Q 𝑧 ) ↔ 𝑥 = ( 𝑧 +Q 𝑦 ) )
5	4	2rexbii	⊢ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑦 +Q 𝑧 ) ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑧 +Q 𝑦 ) )
6		rexcom	⊢ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑧 +Q 𝑦 ) ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝑧 +Q 𝑦 ) )
7	5 6	bitri	⊢ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑦 +Q 𝑧 ) ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝑧 +Q 𝑦 ) )
8	7	abbii	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑦 +Q 𝑧 ) } = { 𝑥 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝑧 +Q 𝑦 ) }
9	2 8	eqtrdi	⊢ ( ( 𝐵 ∈ P ∧ 𝐴 ∈ P ) → ( 𝐵 +P 𝐴 ) = { 𝑥 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝑧 +Q 𝑦 ) } )
10	9	ancoms	⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐵 +P 𝐴 ) = { 𝑥 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝑧 +Q 𝑦 ) } )
11	1 10	eqtr4d	⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 +P 𝐵 ) = ( 𝐵 +P 𝐴 ) )
12		dmplp	⊢ dom +P = ( P × P )
13	12	ndmovcom	⊢ ( ¬ ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 +P 𝐵 ) = ( 𝐵 +P 𝐴 ) )
14	11 13	pm2.61i	⊢ ( 𝐴 +P 𝐵 ) = ( 𝐵 +P 𝐴 )