Theorem ecovcom

Description: Lemma used to transfer a commutative law via an equivalence relation. (Contributed by NM, 29-Aug-1995) (Revised by David Abernethy, 4-Jun-2013)

	Ref	Expression
Hypotheses	ecovcom.1	⊢ 𝐶 = ( ( 𝑆 × 𝑆 ) / ∼ )
	ecovcom.2	⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) = [ ⟨ 𝐷 , 𝐺 ⟩ ] ∼ )
	ecovcom.3	⊢ ( ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ ) = [ ⟨ 𝐻 , 𝐽 ⟩ ] ∼ )
	ecovcom.4	⊢ 𝐷 = 𝐻
	ecovcom.5	⊢ 𝐺 = 𝐽
Assertion	ecovcom	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ecovcom.1	⊢ 𝐶 = ( ( 𝑆 × 𝑆 ) / ∼ )
2		ecovcom.2	⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) = [ ⟨ 𝐷 , 𝐺 ⟩ ] ∼ )
3		ecovcom.3	⊢ ( ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ ) = [ ⟨ 𝐻 , 𝐽 ⟩ ] ∼ )
4		ecovcom.4	⊢ 𝐷 = 𝐻
5		ecovcom.5	⊢ 𝐺 = 𝐽
6		oveq1	⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ = 𝐴 → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) = ( 𝐴 + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) )
7		oveq2	⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ = 𝐴 → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ ) = ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + 𝐴 ) )
8	6 7	eqeq12d	⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ = 𝐴 → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) = ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ ) ↔ ( 𝐴 + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) = ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + 𝐴 ) ) )
9		oveq2	⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = 𝐵 → ( 𝐴 + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) = ( 𝐴 + 𝐵 ) )
10		oveq1	⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = 𝐵 → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + 𝐴 ) = ( 𝐵 + 𝐴 ) )
11	9 10	eqeq12d	⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = 𝐵 → ( ( 𝐴 + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) = ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + 𝐴 ) ↔ ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) ) )
12		opeq12	⊢ ( ( 𝐷 = 𝐻 ∧ 𝐺 = 𝐽 ) → ⟨ 𝐷 , 𝐺 ⟩ = ⟨ 𝐻 , 𝐽 ⟩ )
13	12	eceq1d	⊢ ( ( 𝐷 = 𝐻 ∧ 𝐺 = 𝐽 ) → [ ⟨ 𝐷 , 𝐺 ⟩ ] ∼ = [ ⟨ 𝐻 , 𝐽 ⟩ ] ∼ )
14	4 5 13	mp2an	⊢ [ ⟨ 𝐷 , 𝐺 ⟩ ] ∼ = [ ⟨ 𝐻 , 𝐽 ⟩ ] ∼
15	3	ancoms	⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ ) = [ ⟨ 𝐻 , 𝐽 ⟩ ] ∼ )
16	14 2 15	3eqtr4a	⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) = ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ ) )
17	1 8 11 16	2ecoptocl	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )