Theorem ecopovtrn 8861

Description: Assuming that operation 𝐹 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.)

Hypotheses

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

Assertion

Ref	Expression
ecopovtrn	⊢ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → 𝐴 ∼ 𝐶)

Distinct variable groups:   𝑥,𝑦,𝑧,𝑤,𝑣,𝑢, +   𝑥,𝑆,𝑦,𝑧,𝑤,𝑣,𝑢

Allowed substitution hints:   𝐴(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢)   𝐵(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢)   𝐶(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢)   ∼ (𝑥,𝑦,𝑧,𝑤,𝑣,𝑢)

Proof of Theorem ecopovtrn

Dummy variables 𝑓 𝑔 ℎ 𝑡 𝑠 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ecopopr.1	. . . . . . 7 ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))}
2		opabssxp 5777	. . . . . . 7 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆))
3	1, 2	eqsstri 4029	. . . . . 6 ⊢ ∼ ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆))
4	3	brel 5749	. . . . 5 ⊢ (𝐴 ∼ 𝐵 → (𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆)))
5	4	simpld 494	. . . 4 ⊢ (𝐴 ∼ 𝐵 → 𝐴 ∈ (𝑆 × 𝑆))
6	3	brel 5749	. . . 4 ⊢ (𝐵 ∼ 𝐶 → (𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)))
7	5, 6	anim12i 613	. . 3 ⊢ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → (𝐴 ∈ (𝑆 × 𝑆) ∧ (𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆))))
8		3anass 1094	. . 3 ⊢ ((𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)) ↔ (𝐴 ∈ (𝑆 × 𝑆) ∧ (𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆))))
9	7, 8	sylibr 234	. 2 ⊢ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → (𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)))
10		eqid 2736	. . 3 ⊢ (𝑆 × 𝑆) = (𝑆 × 𝑆)
11		breq1 5145	. . . . 5 ⊢ (⟨𝑓, 𝑔⟩ = 𝐴 → (⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ↔ 𝐴 ∼ ⟨ℎ, 𝑡⟩))
12	11	anbi1d 631	. . . 4 ⊢ (⟨𝑓, 𝑔⟩ = 𝐴 → ((⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) ↔ (𝐴 ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩)))
13		breq1 5145	. . . 4 ⊢ (⟨𝑓, 𝑔⟩ = 𝐴 → (⟨𝑓, 𝑔⟩ ∼ ⟨𝑠, 𝑟⟩ ↔ 𝐴 ∼ ⟨𝑠, 𝑟⟩))
14	12, 13	imbi12d 344	. . 3 ⊢ (⟨𝑓, 𝑔⟩ = 𝐴 → (((⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) → ⟨𝑓, 𝑔⟩ ∼ ⟨𝑠, 𝑟⟩) ↔ ((𝐴 ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) → 𝐴 ∼ ⟨𝑠, 𝑟⟩)))
15		breq2 5146	. . . . 5 ⊢ (⟨ℎ, 𝑡⟩ = 𝐵 → (𝐴 ∼ ⟨ℎ, 𝑡⟩ ↔ 𝐴 ∼ 𝐵))
16		breq1 5145	. . . . 5 ⊢ (⟨ℎ, 𝑡⟩ = 𝐵 → (⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩ ↔ 𝐵 ∼ ⟨𝑠, 𝑟⟩))
17	15, 16	anbi12d 632	. . . 4 ⊢ (⟨ℎ, 𝑡⟩ = 𝐵 → ((𝐴 ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) ↔ (𝐴 ∼ 𝐵 ∧ 𝐵 ∼ ⟨𝑠, 𝑟⟩)))
18	17	imbi1d 341	. . 3 ⊢ (⟨ℎ, 𝑡⟩ = 𝐵 → (((𝐴 ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) → 𝐴 ∼ ⟨𝑠, 𝑟⟩) ↔ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ ⟨𝑠, 𝑟⟩) → 𝐴 ∼ ⟨𝑠, 𝑟⟩)))
19		breq2 5146	. . . . 5 ⊢ (⟨𝑠, 𝑟⟩ = 𝐶 → (𝐵 ∼ ⟨𝑠, 𝑟⟩ ↔ 𝐵 ∼ 𝐶))
20	19	anbi2d 630	. . . 4 ⊢ (⟨𝑠, 𝑟⟩ = 𝐶 → ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ ⟨𝑠, 𝑟⟩) ↔ (𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶)))
21		breq2 5146	. . . 4 ⊢ (⟨𝑠, 𝑟⟩ = 𝐶 → (𝐴 ∼ ⟨𝑠, 𝑟⟩ ↔ 𝐴 ∼ 𝐶))
22	20, 21	imbi12d 344	. . 3 ⊢ (⟨𝑠, 𝑟⟩ = 𝐶 → (((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ ⟨𝑠, 𝑟⟩) → 𝐴 ∼ ⟨𝑠, 𝑟⟩) ↔ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → 𝐴 ∼ 𝐶)))
23	1	ecopoveq 8859	. . . . . . . 8 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) → (⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ↔ (𝑓 + 𝑡) = (𝑔 + ℎ)))
24	23	3adant3 1132	. . . . . . 7 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ↔ (𝑓 + 𝑡) = (𝑔 + ℎ)))
25	1	ecopoveq 8859	. . . . . . . 8 ⊢ (((ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩ ↔ (ℎ + 𝑟) = (𝑡 + 𝑠)))
26	25	3adant1 1130	. . . . . . 7 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩ ↔ (ℎ + 𝑟) = (𝑡 + 𝑠)))
27	24, 26	anbi12d 632	. . . . . 6 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) ↔ ((𝑓 + 𝑡) = (𝑔 + ℎ) ∧ (ℎ + 𝑟) = (𝑡 + 𝑠))))
28		oveq12 7441	. . . . . . 7 ⊢ (((𝑓 + 𝑡) = (𝑔 + ℎ) ∧ (ℎ + 𝑟) = (𝑡 + 𝑠)) → ((𝑓 + 𝑡) + (ℎ + 𝑟)) = ((𝑔 + ℎ) + (𝑡 + 𝑠)))
29		vex 3483	. . . . . . . 8 ⊢ ℎ ∈ V
30		vex 3483	. . . . . . . 8 ⊢ 𝑡 ∈ V
31		vex 3483	. . . . . . . 8 ⊢ 𝑓 ∈ V
32		ecopopr.com	. . . . . . . 8 ⊢ (𝑥 + 𝑦) = (𝑦 + 𝑥)
33		ecopopr.ass	. . . . . . . 8 ⊢ ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))
34		vex 3483	. . . . . . . 8 ⊢ 𝑟 ∈ V
35	29, 30, 31, 32, 33, 34	caov411 7666	. . . . . . 7 ⊢ ((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((𝑓 + 𝑡) + (ℎ + 𝑟))
36		vex 3483	. . . . . . . . 9 ⊢ 𝑔 ∈ V
37		vex 3483	. . . . . . . . 9 ⊢ 𝑠 ∈ V
38	36, 30, 29, 32, 33, 37	caov411 7666	. . . . . . . 8 ⊢ ((𝑔 + 𝑡) + (ℎ + 𝑠)) = ((ℎ + 𝑡) + (𝑔 + 𝑠))
39	36, 30, 29, 32, 33, 37	caov4 7665	. . . . . . . 8 ⊢ ((𝑔 + 𝑡) + (ℎ + 𝑠)) = ((𝑔 + ℎ) + (𝑡 + 𝑠))
40	38, 39	eqtr3i 2766	. . . . . . 7 ⊢ ((ℎ + 𝑡) + (𝑔 + 𝑠)) = ((𝑔 + ℎ) + (𝑡 + 𝑠))
41	28, 35, 40	3eqtr4g 2801	. . . . . 6 ⊢ (((𝑓 + 𝑡) = (𝑔 + ℎ) ∧ (ℎ + 𝑟) = (𝑡 + 𝑠)) → ((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)))
42	27, 41	biimtrdi 253	. . . . 5 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) → ((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠))))
43		ecopopr.cl	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)
44	43	caovcl 7628	. . . . . . . . . 10 ⊢ ((ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) → (ℎ + 𝑡) ∈ 𝑆)
45	43	caovcl 7628	. . . . . . . . . 10 ⊢ ((𝑓 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆) → (𝑓 + 𝑟) ∈ 𝑆)
46		ovex 7465	. . . . . . . . . . 11 ⊢ (𝑔 + 𝑠) ∈ V
47		ecopopr.can	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧))
48	46, 47	caovcan 7638	. . . . . . . . . 10 ⊢ (((ℎ + 𝑡) ∈ 𝑆 ∧ (𝑓 + 𝑟) ∈ 𝑆) → (((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
49	44, 45, 48	syl2an 596	. . . . . . . . 9 ⊢ (((ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑓 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
50	49	3impb 1114	. . . . . . . 8 ⊢ (((ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ 𝑓 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆) → (((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
51	50	3com12 1123	. . . . . . 7 ⊢ ((𝑓 ∈ 𝑆 ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ 𝑟 ∈ 𝑆) → (((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
52	51	3adant3l 1180	. . . . . 6 ⊢ ((𝑓 ∈ 𝑆 ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
53	52	3adant1r 1177	. . . . 5 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
54	42, 53	syld 47	. . . 4 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
55	1	ecopoveq 8859	. . . . 5 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (⟨𝑓, 𝑔⟩ ∼ ⟨𝑠, 𝑟⟩ ↔ (𝑓 + 𝑟) = (𝑔 + 𝑠)))
56	55	3adant2 1131	. . . 4 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (⟨𝑓, 𝑔⟩ ∼ ⟨𝑠, 𝑟⟩ ↔ (𝑓 + 𝑟) = (𝑔 + 𝑠)))
57	54, 56	sylibrd 259	. . 3 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) → ⟨𝑓, 𝑔⟩ ∼ ⟨𝑠, 𝑟⟩))
58	10, 14, 18, 22, 57	3optocl 5781	. 2 ⊢ ((𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)) → ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → 𝐴 ∼ 𝐶))
59	9, 58	mpcom 38	1 ⊢ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → 𝐴 ∼ 𝐶)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1539  ∃wex 1778   ∈ wcel 2107  ⟨cop 4631   class class class wbr 5142  {copab 5204   × cxp 5682  (class class class)co 7432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-opab 5205  df-xp 5690  df-iota 6513  df-fv 6568  df-ov 7435

This theorem is referenced by:  ecopover  8862