Metamath Proof Explorer


Theorem ecopover

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 an equivalence relation. (Contributed by NM, 16-Feb-1996) (Revised by Mario Carneiro, 12-Aug-2015) (Proof shortened by AV, 1-May-2021)

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

Proof

Step Hyp Ref Expression
1 ecopopr.1 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑆 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑆 × 𝑆 ) ) ∧ ∃ 𝑧𝑤𝑣𝑢 ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ ( 𝑧 + 𝑢 ) = ( 𝑤 + 𝑣 ) ) ) }
2 ecopopr.com ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 )
3 ecopopr.cl ( ( 𝑥𝑆𝑦𝑆 ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
4 ecopopr.ass ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) )
5 ecopopr.can ( ( 𝑥𝑆𝑦𝑆 ) → ( ( 𝑥 + 𝑦 ) = ( 𝑥 + 𝑧 ) → 𝑦 = 𝑧 ) )
6 1 relopabiv Rel
7 1 2 ecopovsym ( 𝑓 𝑔𝑔 𝑓 )
8 1 2 3 4 5 ecopovtrn ( ( 𝑓 𝑔𝑔 ) → 𝑓 )
9 vex 𝑔 ∈ V
10 vex ∈ V
11 9 10 2 caovcom ( 𝑔 + ) = ( + 𝑔 )
12 1 ecopoveq ( ( ( 𝑔𝑆𝑆 ) ∧ ( 𝑔𝑆𝑆 ) ) → ( ⟨ 𝑔 , 𝑔 , ⟩ ↔ ( 𝑔 + ) = ( + 𝑔 ) ) )
13 11 12 mpbiri ( ( ( 𝑔𝑆𝑆 ) ∧ ( 𝑔𝑆𝑆 ) ) → ⟨ 𝑔 , 𝑔 , ⟩ )
14 13 anidms ( ( 𝑔𝑆𝑆 ) → ⟨ 𝑔 , 𝑔 , ⟩ )
15 14 rgen2 𝑔𝑆𝑆𝑔 , 𝑔 ,
16 breq12 ( ( 𝑓 = ⟨ 𝑔 , ⟩ ∧ 𝑓 = ⟨ 𝑔 , ⟩ ) → ( 𝑓 𝑓 ↔ ⟨ 𝑔 , 𝑔 , ⟩ ) )
17 16 anidms ( 𝑓 = ⟨ 𝑔 , ⟩ → ( 𝑓 𝑓 ↔ ⟨ 𝑔 , 𝑔 , ⟩ ) )
18 17 ralxp ( ∀ 𝑓 ∈ ( 𝑆 × 𝑆 ) 𝑓 𝑓 ↔ ∀ 𝑔𝑆𝑆𝑔 , 𝑔 , ⟩ )
19 15 18 mpbir 𝑓 ∈ ( 𝑆 × 𝑆 ) 𝑓 𝑓
20 19 rspec ( 𝑓 ∈ ( 𝑆 × 𝑆 ) → 𝑓 𝑓 )
21 opabssxp { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑆 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑆 × 𝑆 ) ) ∧ ∃ 𝑧𝑤𝑣𝑢 ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ ( 𝑧 + 𝑢 ) = ( 𝑤 + 𝑣 ) ) ) } ⊆ ( ( 𝑆 × 𝑆 ) × ( 𝑆 × 𝑆 ) )
22 1 21 eqsstri ⊆ ( ( 𝑆 × 𝑆 ) × ( 𝑆 × 𝑆 ) )
23 22 ssbri ( 𝑓 𝑓𝑓 ( ( 𝑆 × 𝑆 ) × ( 𝑆 × 𝑆 ) ) 𝑓 )
24 brxp ( 𝑓 ( ( 𝑆 × 𝑆 ) × ( 𝑆 × 𝑆 ) ) 𝑓 ↔ ( 𝑓 ∈ ( 𝑆 × 𝑆 ) ∧ 𝑓 ∈ ( 𝑆 × 𝑆 ) ) )
25 24 simplbi ( 𝑓 ( ( 𝑆 × 𝑆 ) × ( 𝑆 × 𝑆 ) ) 𝑓𝑓 ∈ ( 𝑆 × 𝑆 ) )
26 23 25 syl ( 𝑓 𝑓𝑓 ∈ ( 𝑆 × 𝑆 ) )
27 20 26 impbii ( 𝑓 ∈ ( 𝑆 × 𝑆 ) ↔ 𝑓 𝑓 )
28 6 7 8 27 iseri Er ( 𝑆 × 𝑆 )