This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐴 )