Theorem ecopovtrn 8878

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 5792	. . . . . . 7 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆))
3	1, 2	eqsstri 4043	. . . . . 6 ⊢ ∼ ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆))
4	3	brel 5765	. . . . 5 ⊢ (𝐴 ∼ 𝐵 → (𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆)))
5	4	simpld 494	. . . 4 ⊢ (𝐴 ∼ 𝐵 → 𝐴 ∈ (𝑆 × 𝑆))
6	3	brel 5765	. . . 4 ⊢ (𝐵 ∼ 𝐶 → (𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)))
7	5, 6	anim12i 612	. . 3 ⊢ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → (𝐴 ∈ (𝑆 × 𝑆) ∧ (𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆))))
8		3anass 1095	. . 3 ⊢ ((𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)) ↔ (𝐴 ∈ (𝑆 × 𝑆) ∧ (𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆))))
9	7, 8	sylibr 234	. 2 ⊢ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → (𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)))
10		eqid 2740	. . 3 ⊢ (𝑆 × 𝑆) = (𝑆 × 𝑆)
11		breq1 5169	. . . . 5 ⊢ (⟨𝑓, 𝑔⟩ = 𝐴 → (⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ↔ 𝐴 ∼ ⟨ℎ, 𝑡⟩))
12	11	anbi1d 630	. . . 4 ⊢ (⟨𝑓, 𝑔⟩ = 𝐴 → ((⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) ↔ (𝐴 ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩)))
13		breq1 5169	. . . 4 ⊢ (⟨𝑓, 𝑔⟩ = 𝐴 → (⟨𝑓, 𝑔⟩ ∼ ⟨𝑠, 𝑟⟩ ↔ 𝐴 ∼ ⟨𝑠, 𝑟⟩))
14	12, 13	imbi12d 344	. . 3 ⊢ (⟨𝑓, 𝑔⟩ = 𝐴 → (((⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) → ⟨𝑓, 𝑔⟩ ∼ ⟨𝑠, 𝑟⟩) ↔ ((𝐴 ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) → 𝐴 ∼ ⟨𝑠, 𝑟⟩)))
15		breq2 5170	. . . . 5 ⊢ (⟨ℎ, 𝑡⟩ = 𝐵 → (𝐴 ∼ ⟨ℎ, 𝑡⟩ ↔ 𝐴 ∼ 𝐵))
16		breq1 5169	. . . . 5 ⊢ (⟨ℎ, 𝑡⟩ = 𝐵 → (⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩ ↔ 𝐵 ∼ ⟨𝑠, 𝑟⟩))
17	15, 16	anbi12d 631	. . . 4 ⊢ (⟨ℎ, 𝑡⟩ = 𝐵 → ((𝐴 ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) ↔ (𝐴 ∼ 𝐵 ∧ 𝐵 ∼ ⟨𝑠, 𝑟⟩)))
18	17	imbi1d 341	. . 3 ⊢ (⟨ℎ, 𝑡⟩ = 𝐵 → (((𝐴 ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) → 𝐴 ∼ ⟨𝑠, 𝑟⟩) ↔ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ ⟨𝑠, 𝑟⟩) → 𝐴 ∼ ⟨𝑠, 𝑟⟩)))
19		breq2 5170	. . . . 5 ⊢ (⟨𝑠, 𝑟⟩ = 𝐶 → (𝐵 ∼ ⟨𝑠, 𝑟⟩ ↔ 𝐵 ∼ 𝐶))
20	19	anbi2d 629	. . . 4 ⊢ (⟨𝑠, 𝑟⟩ = 𝐶 → ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ ⟨𝑠, 𝑟⟩) ↔ (𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶)))
21		breq2 5170	. . . 4 ⊢ (⟨𝑠, 𝑟⟩ = 𝐶 → (𝐴 ∼ ⟨𝑠, 𝑟⟩ ↔ 𝐴 ∼ 𝐶))
22	20, 21	imbi12d 344	. . 3 ⊢ (⟨𝑠, 𝑟⟩ = 𝐶 → (((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ ⟨𝑠, 𝑟⟩) → 𝐴 ∼ ⟨𝑠, 𝑟⟩) ↔ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → 𝐴 ∼ 𝐶)))
23	1	ecopoveq 8876	. . . . . . . 8 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) → (⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ↔ (𝑓 + 𝑡) = (𝑔 + ℎ)))
24	23	3adant3 1132	. . . . . . 7 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ↔ (𝑓 + 𝑡) = (𝑔 + ℎ)))
25	1	ecopoveq 8876	. . . . . . . 8 ⊢ (((ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩ ↔ (ℎ + 𝑟) = (𝑡 + 𝑠)))
26	25	3adant1 1130	. . . . . . 7 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩ ↔ (ℎ + 𝑟) = (𝑡 + 𝑠)))
27	24, 26	anbi12d 631	. . . . . 6 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) ↔ ((𝑓 + 𝑡) = (𝑔 + ℎ) ∧ (ℎ + 𝑟) = (𝑡 + 𝑠))))
28		oveq12 7457	. . . . . . 7 ⊢ (((𝑓 + 𝑡) = (𝑔 + ℎ) ∧ (ℎ + 𝑟) = (𝑡 + 𝑠)) → ((𝑓 + 𝑡) + (ℎ + 𝑟)) = ((𝑔 + ℎ) + (𝑡 + 𝑠)))
29		vex 3492	. . . . . . . 8 ⊢ ℎ ∈ V
30		vex 3492	. . . . . . . 8 ⊢ 𝑡 ∈ V
31		vex 3492	. . . . . . . 8 ⊢ 𝑓 ∈ V
32		ecopopr.com	. . . . . . . 8 ⊢ (𝑥 + 𝑦) = (𝑦 + 𝑥)
33		ecopopr.ass	. . . . . . . 8 ⊢ ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))
34		vex 3492	. . . . . . . 8 ⊢ 𝑟 ∈ V
35	29, 30, 31, 32, 33, 34	caov411 7682	. . . . . . 7 ⊢ ((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((𝑓 + 𝑡) + (ℎ + 𝑟))
36		vex 3492	. . . . . . . . 9 ⊢ 𝑔 ∈ V
37		vex 3492	. . . . . . . . 9 ⊢ 𝑠 ∈ V
38	36, 30, 29, 32, 33, 37	caov411 7682	. . . . . . . 8 ⊢ ((𝑔 + 𝑡) + (ℎ + 𝑠)) = ((ℎ + 𝑡) + (𝑔 + 𝑠))
39	36, 30, 29, 32, 33, 37	caov4 7681	. . . . . . . 8 ⊢ ((𝑔 + 𝑡) + (ℎ + 𝑠)) = ((𝑔 + ℎ) + (𝑡 + 𝑠))
40	38, 39	eqtr3i 2770	. . . . . . 7 ⊢ ((ℎ + 𝑡) + (𝑔 + 𝑠)) = ((𝑔 + ℎ) + (𝑡 + 𝑠))
41	28, 35, 40	3eqtr4g 2805	. . . . . 6 ⊢ (((𝑓 + 𝑡) = (𝑔 + ℎ) ∧ (ℎ + 𝑟) = (𝑡 + 𝑠)) → ((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)))
42	27, 41	biimtrdi 253	. . . . 5 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) → ((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠))))
43		ecopopr.cl	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)
44	43	caovcl 7644	. . . . . . . . . 10 ⊢ ((ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) → (ℎ + 𝑡) ∈ 𝑆)
45	43	caovcl 7644	. . . . . . . . . 10 ⊢ ((𝑓 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆) → (𝑓 + 𝑟) ∈ 𝑆)
46		ovex 7481	. . . . . . . . . . 11 ⊢ (𝑔 + 𝑠) ∈ V
47		ecopopr.can	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧))
48	46, 47	caovcan 7654	. . . . . . . . . 10 ⊢ (((ℎ + 𝑡) ∈ 𝑆 ∧ (𝑓 + 𝑟) ∈ 𝑆) → (((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
49	44, 45, 48	syl2an 595	. . . . . . . . 9 ⊢ (((ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑓 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
50	49	3impb 1115	. . . . . . . 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 8876	. . . . 5 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (⟨𝑓, 𝑔⟩ ∼ ⟨𝑠, 𝑟⟩ ↔ (𝑓 + 𝑟) = (𝑔 + 𝑠)))
56	55	3adant2 1131	. . . 4 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (⟨𝑓, 𝑔⟩ ∼ ⟨𝑠, 𝑟⟩ ↔ (𝑓 + 𝑟) = (𝑔 + 𝑠)))
57	54, 56	sylibrd 259	. . 3 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) → ⟨𝑓, 𝑔⟩ ∼ ⟨𝑠, 𝑟⟩))
58	10, 14, 18, 22, 57	3optocl 5796	. 2 ⊢ ((𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)) → ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → 𝐴 ∼ 𝐶))
59	9, 58	mpcom 38	1 ⊢ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → 𝐴 ∼ 𝐶)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1537  ∃wex 1777   ∈ wcel 2108  ⟨cop 4654   class class class wbr 5166  {copab 5228   × cxp 5698  (class class class)co 7448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-xp 5706  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  ecopover  8879