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

Metamath Proof Explorer

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 ⋅ 𝑷 B = B ⋅ 𝑷 A

Proof

Step Hyp Ref Expression
1 mpv ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → A ⋅ 𝑷 B = x | ∃ z ∈ A ∃ y ∈ B x = z ⋅ 𝑸 y
2 mpv ⊢ B ∈ 𝑷 ∧ A ∈ 𝑷 → B ⋅ 𝑷 A = x | ∃ y ∈ B ∃ z ∈ A x = y ⋅ 𝑸 z
3 mulcomnq ⊢ y ⋅ 𝑸 z = z ⋅ 𝑸 y
4 3 eqeq2i ⊢ x = y ⋅ 𝑸 z ↔ x = z ⋅ 𝑸 y
5 4 2rexbii ⊢ ∃ y ∈ B ∃ z ∈ A x = y ⋅ 𝑸 z ↔ ∃ y ∈ B ∃ z ∈ A x = z ⋅ 𝑸 y
6 rexcom ⊢ ∃ y ∈ B ∃ z ∈ A x = z ⋅ 𝑸 y ↔ ∃ z ∈ A ∃ y ∈ B x = z ⋅ 𝑸 y
7 5 6 bitri ⊢ ∃ y ∈ B ∃ z ∈ A x = y ⋅ 𝑸 z ↔ ∃ z ∈ A ∃ y ∈ B x = z ⋅ 𝑸 y
8 7 abbii ⊢ x | ∃ y ∈ B ∃ z ∈ A x = y ⋅ 𝑸 z = x | ∃ z ∈ A ∃ y ∈ B x = z ⋅ 𝑸 y
9 2 8 eqtrdi ⊢ B ∈ 𝑷 ∧ A ∈ 𝑷 → B ⋅ 𝑷 A = x | ∃ z ∈ A ∃ y ∈ B x = z ⋅ 𝑸 y
10 9 ancoms ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → B ⋅ 𝑷 A = x | ∃ z ∈ A ∃ y ∈ B x = z ⋅ 𝑸 y
11 1 10 eqtr4d ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → A ⋅ 𝑷 B = B ⋅ 𝑷 A
12 dmmp ⊢ dom ⁡ ⋅ 𝑷 = 𝑷 × 𝑷
13 12 ndmovcom ⊢ ¬ A ∈ 𝑷 ∧ B ∈ 𝑷 → A ⋅ 𝑷 B = B ⋅ 𝑷 A
14 11 13 pm2.61i ⊢ A ⋅ 𝑷 B = B ⋅ 𝑷 A