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