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

Metamath Proof Explorer

Theorem ecopovtrn

Description: Assuming that operation F is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation .~ , specified by the first hypothesis, is transitive. (Contributed by NM, 11-Feb-1996) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Hypotheses ecopopr.1 ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑆 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑆 × 𝑆 ) ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ ( 𝑧 + 𝑢 ) = ( 𝑤 + 𝑣 ) ) ) }
ecopopr.com ⊢ ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 )
ecopopr.cl ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
ecopopr.ass ⊢ ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) )
ecopopr.can ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑥 + 𝑦 ) = ( 𝑥 + 𝑧 ) → 𝑦 = 𝑧 ) )
Assertion ecopovtrn ( ( 𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶 ) → 𝐴 ∼ 𝐶 )

Proof

Step Hyp Ref Expression
1 ecopopr.1 ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑆 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑆 × 𝑆 ) ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ ( 𝑧 + 𝑢 ) = ( 𝑤 + 𝑣 ) ) ) }
2 ecopopr.com ⊢ ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 )
3 ecopopr.cl ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
4 ecopopr.ass ⊢ ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) )
5 ecopopr.can ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑥 + 𝑦 ) = ( 𝑥 + 𝑧 ) → 𝑦 = 𝑧 ) )
6 opabssxp ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑆 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑆 × 𝑆 ) ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ ( 𝑧 + 𝑢 ) = ( 𝑤 + 𝑣 ) ) ) } ⊆ ( ( 𝑆 × 𝑆 ) × ( 𝑆 × 𝑆 ) )
7 1 6 eqsstri ⊢ ∼ ⊆ ( ( 𝑆 × 𝑆 ) × ( 𝑆 × 𝑆 ) )
8 7 brel ⊢ ( 𝐴 ∼ 𝐵 → ( 𝐴 ∈ ( 𝑆 × 𝑆 ) ∧ 𝐵 ∈ ( 𝑆 × 𝑆 ) ) )
9 8 simpld ⊢ ( 𝐴 ∼ 𝐵 → 𝐴 ∈ ( 𝑆 × 𝑆 ) )
10 7 brel ⊢ ( 𝐵 ∼ 𝐶 → ( 𝐵 ∈ ( 𝑆 × 𝑆 ) ∧ 𝐶 ∈ ( 𝑆 × 𝑆 ) ) )
11 9 10 anim12i ⊢ ( ( 𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶 ) → ( 𝐴 ∈ ( 𝑆 × 𝑆 ) ∧ ( 𝐵 ∈ ( 𝑆 × 𝑆 ) ∧ 𝐶 ∈ ( 𝑆 × 𝑆 ) ) ) )
12 3anass ⊢ ( ( 𝐴 ∈ ( 𝑆 × 𝑆 ) ∧ 𝐵 ∈ ( 𝑆 × 𝑆 ) ∧ 𝐶 ∈ ( 𝑆 × 𝑆 ) ) ↔ ( 𝐴 ∈ ( 𝑆 × 𝑆 ) ∧ ( 𝐵 ∈ ( 𝑆 × 𝑆 ) ∧ 𝐶 ∈ ( 𝑆 × 𝑆 ) ) ) )
13 11 12 sylibr ⊢ ( ( 𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶 ) → ( 𝐴 ∈ ( 𝑆 × 𝑆 ) ∧ 𝐵 ∈ ( 𝑆 × 𝑆 ) ∧ 𝐶 ∈ ( 𝑆 × 𝑆 ) ) )
14 eqid ⊢ ( 𝑆 × 𝑆 ) = ( 𝑆 × 𝑆 )
15 breq1 ⊢ ( ⟨ 𝑓 , 𝑔 ⟩ = 𝐴 → ( ⟨ 𝑓 , 𝑔 ⟩ ∼ ⟨ ℎ , 𝑡 ⟩ ↔ 𝐴 ∼ ⟨ ℎ , 𝑡 ⟩ ) )
16 15 anbi1d ⊢ ( ⟨ 𝑓 , 𝑔 ⟩ = 𝐴 → ( ( ⟨ 𝑓 , 𝑔 ⟩ ∼ ⟨ ℎ , 𝑡 ⟩ ∧ ⟨ ℎ , 𝑡 ⟩ ∼ ⟨ 𝑠 , 𝑟 ⟩ ) ↔ ( 𝐴 ∼ ⟨ ℎ , 𝑡 ⟩ ∧ ⟨ ℎ , 𝑡 ⟩ ∼ ⟨ 𝑠 , 𝑟 ⟩ ) ) )
17 breq1 ⊢ ( ⟨ 𝑓 , 𝑔 ⟩ = 𝐴 → ( ⟨ 𝑓 , 𝑔 ⟩ ∼ ⟨ 𝑠 , 𝑟 ⟩ ↔ 𝐴 ∼ ⟨ 𝑠 , 𝑟 ⟩ ) )
18 16 17 imbi12d ⊢ ( ⟨ 𝑓 , 𝑔 ⟩ = 𝐴 → ( ( ( ⟨ 𝑓 , 𝑔 ⟩ ∼ ⟨ ℎ , 𝑡 ⟩ ∧ ⟨ ℎ , 𝑡 ⟩ ∼ ⟨ 𝑠 , 𝑟 ⟩ ) → ⟨ 𝑓 , 𝑔 ⟩ ∼ ⟨ 𝑠 , 𝑟 ⟩ ) ↔ ( ( 𝐴 ∼ ⟨ ℎ , 𝑡 ⟩ ∧ ⟨ ℎ , 𝑡 ⟩ ∼ ⟨ 𝑠 , 𝑟 ⟩ ) → 𝐴 ∼ ⟨ 𝑠 , 𝑟 ⟩ ) ) )
19 breq2 ⊢ ( ⟨ ℎ , 𝑡 ⟩ = 𝐵 → ( 𝐴 ∼ ⟨ ℎ , 𝑡 ⟩ ↔ 𝐴 ∼ 𝐵 ) )
20 breq1 ⊢ ( ⟨ ℎ , 𝑡 ⟩ = 𝐵 → ( ⟨ ℎ , 𝑡 ⟩ ∼ ⟨ 𝑠 , 𝑟 ⟩ ↔ 𝐵 ∼ ⟨ 𝑠 , 𝑟 ⟩ ) )
21 19 20 anbi12d ⊢ ( ⟨ ℎ , 𝑡 ⟩ = 𝐵 → ( ( 𝐴 ∼ ⟨ ℎ , 𝑡 ⟩ ∧ ⟨ ℎ , 𝑡 ⟩ ∼ ⟨ 𝑠 , 𝑟 ⟩ ) ↔ ( 𝐴 ∼ 𝐵 ∧ 𝐵 ∼ ⟨ 𝑠 , 𝑟 ⟩ ) ) )
22 21 imbi1d ⊢ ( ⟨ ℎ , 𝑡 ⟩ = 𝐵 → ( ( ( 𝐴 ∼ ⟨ ℎ , 𝑡 ⟩ ∧ ⟨ ℎ , 𝑡 ⟩ ∼ ⟨ 𝑠 , 𝑟 ⟩ ) → 𝐴 ∼ ⟨ 𝑠 , 𝑟 ⟩ ) ↔ ( ( 𝐴 ∼ 𝐵 ∧ 𝐵 ∼ ⟨ 𝑠 , 𝑟 ⟩ ) → 𝐴 ∼ ⟨ 𝑠 , 𝑟 ⟩ ) ) )
23 breq2 ⊢ ( ⟨ 𝑠 , 𝑟 ⟩ = 𝐶 → ( 𝐵 ∼ ⟨ 𝑠 , 𝑟 ⟩ ↔ 𝐵 ∼ 𝐶 ) )
24 23 anbi2d ⊢ ( ⟨ 𝑠 , 𝑟 ⟩ = 𝐶 → ( ( 𝐴 ∼ 𝐵 ∧ 𝐵 ∼ ⟨ 𝑠 , 𝑟 ⟩ ) ↔ ( 𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶 ) ) )
25 breq2 ⊢ ( ⟨ 𝑠 , 𝑟 ⟩ = 𝐶 → ( 𝐴 ∼ ⟨ 𝑠 , 𝑟 ⟩ ↔ 𝐴 ∼ 𝐶 ) )
26 24 25 imbi12d ⊢ ( ⟨ 𝑠 , 𝑟 ⟩ = 𝐶 → ( ( ( 𝐴 ∼ 𝐵 ∧ 𝐵 ∼ ⟨ 𝑠 , 𝑟 ⟩ ) → 𝐴 ∼ ⟨ 𝑠 , 𝑟 ⟩ ) ↔ ( ( 𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶 ) → 𝐴 ∼ 𝐶 ) ) )
27 1 ecopoveq ⊢ ( ( ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆 ) ∧ ( ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆 ) ) → ( ⟨ 𝑓 , 𝑔 ⟩ ∼ ⟨ ℎ , 𝑡 ⟩ ↔ ( 𝑓 + 𝑡 ) = ( 𝑔 + ℎ ) ) )
28 27 3adant3 ⊢ ( ( ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆 ) ∧ ( ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆 ) ) → ( ⟨ 𝑓 , 𝑔 ⟩ ∼ ⟨ ℎ , 𝑡 ⟩ ↔ ( 𝑓 + 𝑡 ) = ( 𝑔 + ℎ ) ) )
29 1 ecopoveq ⊢ ( ( ( ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆 ) ) → ( ⟨ ℎ , 𝑡 ⟩ ∼ ⟨ 𝑠 , 𝑟 ⟩ ↔ ( ℎ + 𝑟 ) = ( 𝑡 + 𝑠 ) ) )
30 29 3adant1 ⊢ ( ( ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆 ) ∧ ( ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆 ) ) → ( ⟨ ℎ , 𝑡 ⟩ ∼ ⟨ 𝑠 , 𝑟 ⟩ ↔ ( ℎ + 𝑟 ) = ( 𝑡 + 𝑠 ) ) )
31 28 30 anbi12d ⊢ ( ( ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆 ) ∧ ( ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆 ) ) → ( ( ⟨ 𝑓 , 𝑔 ⟩ ∼ ⟨ ℎ , 𝑡 ⟩ ∧ ⟨ ℎ , 𝑡 ⟩ ∼ ⟨ 𝑠 , 𝑟 ⟩ ) ↔ ( ( 𝑓 + 𝑡 ) = ( 𝑔 + ℎ ) ∧ ( ℎ + 𝑟 ) = ( 𝑡 + 𝑠 ) ) ) )
32 oveq12 ⊢ ( ( ( 𝑓 + 𝑡 ) = ( 𝑔 + ℎ ) ∧ ( ℎ + 𝑟 ) = ( 𝑡 + 𝑠 ) ) → ( ( 𝑓 + 𝑡 ) + ( ℎ + 𝑟 ) ) = ( ( 𝑔 + ℎ ) + ( 𝑡 + 𝑠 ) ) )
33 vex ⊢ ℎ ∈ V
34 vex ⊢ 𝑡 ∈ V
35 vex ⊢ 𝑓 ∈ V
36 vex ⊢ 𝑟 ∈ V
37 33 34 35 2 4 36 caov411 ⊢ ( ( ℎ + 𝑡 ) + ( 𝑓 + 𝑟 ) ) = ( ( 𝑓 + 𝑡 ) + ( ℎ + 𝑟 ) )
38 vex ⊢ 𝑔 ∈ V
39 vex ⊢ 𝑠 ∈ V
40 38 34 33 2 4 39 caov411 ⊢ ( ( 𝑔 + 𝑡 ) + ( ℎ + 𝑠 ) ) = ( ( ℎ + 𝑡 ) + ( 𝑔 + 𝑠 ) )
41 38 34 33 2 4 39 caov4 ⊢ ( ( 𝑔 + 𝑡 ) + ( ℎ + 𝑠 ) ) = ( ( 𝑔 + ℎ ) + ( 𝑡 + 𝑠 ) )
42 40 41 eqtr3i ⊢ ( ( ℎ + 𝑡 ) + ( 𝑔 + 𝑠 ) ) = ( ( 𝑔 + ℎ ) + ( 𝑡 + 𝑠 ) )
43 32 37 42 3eqtr4g ⊢ ( ( ( 𝑓 + 𝑡 ) = ( 𝑔 + ℎ ) ∧ ( ℎ + 𝑟 ) = ( 𝑡 + 𝑠 ) ) → ( ( ℎ + 𝑡 ) + ( 𝑓 + 𝑟 ) ) = ( ( ℎ + 𝑡 ) + ( 𝑔 + 𝑠 ) ) )
44 31 43 biimtrdi ⊢ ( ( ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆 ) ∧ ( ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆 ) ) → ( ( ⟨ 𝑓 , 𝑔 ⟩ ∼ ⟨ ℎ , 𝑡 ⟩ ∧ ⟨ ℎ , 𝑡 ⟩ ∼ ⟨ 𝑠 , 𝑟 ⟩ ) → ( ( ℎ + 𝑡 ) + ( 𝑓 + 𝑟 ) ) = ( ( ℎ + 𝑡 ) + ( 𝑔 + 𝑠 ) ) ) )
45 3 caovcl ⊢ ( ( ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆 ) → ( ℎ + 𝑡 ) ∈ 𝑆 )
46 3 caovcl ⊢ ( ( 𝑓 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆 ) → ( 𝑓 + 𝑟 ) ∈ 𝑆 )
47 ovex ⊢ ( 𝑔 + 𝑠 ) ∈ V
48 47 5 caovcan ⊢ ( ( ( ℎ + 𝑡 ) ∈ 𝑆 ∧ ( 𝑓 + 𝑟 ) ∈ 𝑆 ) → ( ( ( ℎ + 𝑡 ) + ( 𝑓 + 𝑟 ) ) = ( ( ℎ + 𝑡 ) + ( 𝑔 + 𝑠 ) ) → ( 𝑓 + 𝑟 ) = ( 𝑔 + 𝑠 ) ) )
49 45 46 48 syl2an ⊢ ( ( ( ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆 ) ) → ( ( ( ℎ + 𝑡 ) + ( 𝑓 + 𝑟 ) ) = ( ( ℎ + 𝑡 ) + ( 𝑔 + 𝑠 ) ) → ( 𝑓 + 𝑟 ) = ( 𝑔 + 𝑠 ) ) )
50 49 3impb ⊢ ( ( ( ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆 ) → ( ( ( ℎ + 𝑡 ) + ( 𝑓 + 𝑟 ) ) = ( ( ℎ + 𝑡 ) + ( 𝑔 + 𝑠 ) ) → ( 𝑓 + 𝑟 ) = ( 𝑔 + 𝑠 ) ) )
51 50 3com12 ⊢ ( ( 𝑓 ∈ 𝑆 ∧ ( ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆 ) ∧ 𝑟 ∈ 𝑆 ) → ( ( ( ℎ + 𝑡 ) + ( 𝑓 + 𝑟 ) ) = ( ( ℎ + 𝑡 ) + ( 𝑔 + 𝑠 ) ) → ( 𝑓 + 𝑟 ) = ( 𝑔 + 𝑠 ) ) )
52 51 3adant3l ⊢ ( ( 𝑓 ∈ 𝑆 ∧ ( ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆 ) ) → ( ( ( ℎ + 𝑡 ) + ( 𝑓 + 𝑟 ) ) = ( ( ℎ + 𝑡 ) + ( 𝑔 + 𝑠 ) ) → ( 𝑓 + 𝑟 ) = ( 𝑔 + 𝑠 ) ) )
53 52 3adant1r ⊢ ( ( ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆 ) ∧ ( ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆 ) ) → ( ( ( ℎ + 𝑡 ) + ( 𝑓 + 𝑟 ) ) = ( ( ℎ + 𝑡 ) + ( 𝑔 + 𝑠 ) ) → ( 𝑓 + 𝑟 ) = ( 𝑔 + 𝑠 ) ) )
54 44 53 syld ⊢ ( ( ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆 ) ∧ ( ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆 ) ) → ( ( ⟨ 𝑓 , 𝑔 ⟩ ∼ ⟨ ℎ , 𝑡 ⟩ ∧ ⟨ ℎ , 𝑡 ⟩ ∼ ⟨ 𝑠 , 𝑟 ⟩ ) → ( 𝑓 + 𝑟 ) = ( 𝑔 + 𝑠 ) ) )
55 1 ecopoveq ⊢ ( ( ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆 ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆 ) ) → ( ⟨ 𝑓 , 𝑔 ⟩ ∼ ⟨ 𝑠 , 𝑟 ⟩ ↔ ( 𝑓 + 𝑟 ) = ( 𝑔 + 𝑠 ) ) )
56 55 3adant2 ⊢ ( ( ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆 ) ∧ ( ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆 ) ) → ( ⟨ 𝑓 , 𝑔 ⟩ ∼ ⟨ 𝑠 , 𝑟 ⟩ ↔ ( 𝑓 + 𝑟 ) = ( 𝑔 + 𝑠 ) ) )
57 54 56 sylibrd ⊢ ( ( ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆 ) ∧ ( ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆 ) ) → ( ( ⟨ 𝑓 , 𝑔 ⟩ ∼ ⟨ ℎ , 𝑡 ⟩ ∧ ⟨ ℎ , 𝑡 ⟩ ∼ ⟨ 𝑠 , 𝑟 ⟩ ) → ⟨ 𝑓 , 𝑔 ⟩ ∼ ⟨ 𝑠 , 𝑟 ⟩ ) )
58 14 18 22 26 57 3optocl ⊢ ( ( 𝐴 ∈ ( 𝑆 × 𝑆 ) ∧ 𝐵 ∈ ( 𝑆 × 𝑆 ) ∧ 𝐶 ∈ ( 𝑆 × 𝑆 ) ) → ( ( 𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶 ) → 𝐴 ∼ 𝐶 ) )
59 13 58 mpcom ⊢ ( ( 𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶 ) → 𝐴 ∼ 𝐶 )