Metamath Proof Explorer

Theorem addcompq

Description: Addition of positive fractions is commutative. (Contributed by NM, 30-Aug-1995) (Revised by Mario Carneiro, 28-Apr-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	addcompq	⊢ ( 𝐴 +_pQ 𝐵 ) = ( 𝐵 +_pQ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		addcompi	⊢ ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) +_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) = ( ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) +_N ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) )
2		mulcompi	⊢ ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) = ( ( 2^nd ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) )
3	1 2	opeq12i	⊢ ⟨ ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) +_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) , ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ⟩ = ⟨ ( ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) +_N ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ) , ( ( 2^nd ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ⟩
4		addpipq2	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 +_pQ 𝐵 ) = ⟨ ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) +_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) , ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ⟩ )
5		addpipq2	⊢ ( ( 𝐵 ∈ ( N × N ) ∧ 𝐴 ∈ ( N × N ) ) → ( 𝐵 +_pQ 𝐴 ) = ⟨ ( ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) +_N ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ) , ( ( 2^nd ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ⟩ )
6	5	ancoms	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐵 +_pQ 𝐴 ) = ⟨ ( ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) +_N ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ) , ( ( 2^nd ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ⟩ )
7	3 4 6	3eqtr4a	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 +_pQ 𝐵 ) = ( 𝐵 +_pQ 𝐴 ) )
8		addpqf	⊢ +_pQ : ( ( N × N ) × ( N × N ) ) ⟶ ( N × N )
9	8	fdmi	⊢ dom +_pQ = ( ( N × N ) × ( N × N ) )
10	9	ndmovcom	⊢ ( ¬ ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 +_pQ 𝐵 ) = ( 𝐵 +_pQ 𝐴 ) )
11	7 10	pm2.61i	⊢ ( 𝐴 +_pQ 𝐵 ) = ( 𝐵 +_pQ 𝐴 )