Metamath Proof Explorer

Theorem ecovass

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

Ref Expression
Hypotheses ecovass.1 ⊢ 𝐷 = ( ( 𝑆 × 𝑆 ) / ∼ )
ecovass.2 ⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) = [ ⟨ 𝐺 , 𝐻 ⟩ ] ∼ )
ecovass.3 ⊢ ( ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = [ ⟨ 𝑁 , 𝑄 ⟩ ] ∼ )
ecovass.4 ⊢ ( ( ( 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( [ ⟨ 𝐺 , 𝐻 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = [ ⟨ 𝐽 , 𝐾 ⟩ ] ∼ )
ecovass.5 ⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑁 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆 ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + [ ⟨ 𝑁 , 𝑄 ⟩ ] ∼ ) = [ ⟨ 𝐿 , 𝑀 ⟩ ] ∼ )
ecovass.6 ⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) )
ecovass.7 ⊢ ( ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝑁 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆 ) )
ecovass.8 ⊢ 𝐽 = 𝐿
ecovass.9 ⊢ 𝐾 = 𝑀
Assertion ecovass ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷 ) → ( ( 𝐴 + 𝐵 ) + 𝐶 ) = ( 𝐴 + ( 𝐵 + 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 ecovass.1 ⊢ 𝐷 = ( ( 𝑆 × 𝑆 ) / ∼ )
2 ecovass.2 ⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) = [ ⟨ 𝐺 , 𝐻 ⟩ ] ∼ )
3 ecovass.3 ⊢ ( ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = [ ⟨ 𝑁 , 𝑄 ⟩ ] ∼ )
4 ecovass.4 ⊢ ( ( ( 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( [ ⟨ 𝐺 , 𝐻 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = [ ⟨ 𝐽 , 𝐾 ⟩ ] ∼ )
5 ecovass.5 ⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑁 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆 ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + [ ⟨ 𝑁 , 𝑄 ⟩ ] ∼ ) = [ ⟨ 𝐿 , 𝑀 ⟩ ] ∼ )
6 ecovass.6 ⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) )
7 ecovass.7 ⊢ ( ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝑁 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆 ) )
8 ecovass.8 ⊢ 𝐽 = 𝐿
9 ecovass.9 ⊢ 𝐾 = 𝑀
10 oveq1 ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ = 𝐴 → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) = ( 𝐴 + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) )
11 10 oveq1d ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ = 𝐴 → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = ( ( 𝐴 + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) )
12 oveq1 ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ = 𝐴 → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = ( 𝐴 + ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) )
13 11 12 eqeq12d ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ = 𝐴 → ( ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) ↔ ( ( 𝐴 + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = ( 𝐴 + ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) ) )
14 oveq2 ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = 𝐵 → ( 𝐴 + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) = ( 𝐴 + 𝐵 ) )
15 14 oveq1d ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = 𝐵 → ( ( 𝐴 + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = ( ( 𝐴 + 𝐵 ) + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) )
16 oveq1 ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = 𝐵 → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = ( 𝐵 + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) )
17 16 oveq2d ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = 𝐵 → ( 𝐴 + ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = ( 𝐴 + ( 𝐵 + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) )
18 15 17 eqeq12d ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = 𝐵 → ( ( ( 𝐴 + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = ( 𝐴 + ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) ↔ ( ( 𝐴 + 𝐵 ) + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = ( 𝐴 + ( 𝐵 + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) ) )
19 oveq2 ⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = 𝐶 → ( ( 𝐴 + 𝐵 ) + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = ( ( 𝐴 + 𝐵 ) + 𝐶 ) )
20 oveq2 ⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = 𝐶 → ( 𝐵 + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = ( 𝐵 + 𝐶 ) )
21 20 oveq2d ⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = 𝐶 → ( 𝐴 + ( 𝐵 + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = ( 𝐴 + ( 𝐵 + 𝐶 ) ) )
22 19 21 eqeq12d ⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = 𝐶 → ( ( ( 𝐴 + 𝐵 ) + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = ( 𝐴 + ( 𝐵 + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) ↔ ( ( 𝐴 + 𝐵 ) + 𝐶 ) = ( 𝐴 + ( 𝐵 + 𝐶 ) ) ) )
23 opeq12 ⊢ ( ( 𝐽 = 𝐿 ∧ 𝐾 = 𝑀 ) → ⟨ 𝐽 , 𝐾 ⟩ = ⟨ 𝐿 , 𝑀 ⟩ )
24 23 eceq1d ⊢ ( ( 𝐽 = 𝐿 ∧ 𝐾 = 𝑀 ) → [ ⟨ 𝐽 , 𝐾 ⟩ ] ∼ = [ ⟨ 𝐿 , 𝑀 ⟩ ] ∼ )
25 8 9 24 mp2an ⊢ [ ⟨ 𝐽 , 𝐾 ⟩ ] ∼ = [ ⟨ 𝐿 , 𝑀 ⟩ ] ∼
26 2 oveq1d ⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = ( [ ⟨ 𝐺 , 𝐻 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) )
27 26 adantr ⊢ ( ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = ( [ ⟨ 𝐺 , 𝐻 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) )
28 6 4 sylan ⊢ ( ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( [ ⟨ 𝐺 , 𝐻 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = [ ⟨ 𝐽 , 𝐾 ⟩ ] ∼ )
29 27 28 eqtrd ⊢ ( ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = [ ⟨ 𝐽 , 𝐾 ⟩ ] ∼ )
30 29 3impa ⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = [ ⟨ 𝐽 , 𝐾 ⟩ ] ∼ )
31 3 oveq2d ⊢ ( ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + [ ⟨ 𝑁 , 𝑄 ⟩ ] ∼ ) )
32 31 adantl ⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + [ ⟨ 𝑁 , 𝑄 ⟩ ] ∼ ) )
33 7 5 sylan2 ⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + [ ⟨ 𝑁 , 𝑄 ⟩ ] ∼ ) = [ ⟨ 𝐿 , 𝑀 ⟩ ] ∼ )
34 32 33 eqtrd ⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = [ ⟨ 𝐿 , 𝑀 ⟩ ] ∼ )
35 34 3impb ⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = [ ⟨ 𝐿 , 𝑀 ⟩ ] ∼ )
36 25 30 35 3eqtr4a ⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ + ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) )
37 1 13 18 22 36 3ecoptocl ⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷 ) → ( ( 𝐴 + 𝐵 ) + 𝐶 ) = ( 𝐴 + ( 𝐵 + 𝐶 ) ) )