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

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )