Theorem ecopovtrn 8567

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 5669	. . . . . . 7 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆))
3	1, 2	eqsstri 3951	. . . . . 6 ⊢ ∼ ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆))
4	3	brel 5643	. . . . 5 ⊢ (𝐴 ∼ 𝐵 → (𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆)))
5	4	simpld 494	. . . 4 ⊢ (𝐴 ∼ 𝐵 → 𝐴 ∈ (𝑆 × 𝑆))
6	3	brel 5643	. . . 4 ⊢ (𝐵 ∼ 𝐶 → (𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)))
7	5, 6	anim12i 612	. . 3 ⊢ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → (𝐴 ∈ (𝑆 × 𝑆) ∧ (𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆))))
8		3anass 1093	. . 3 ⊢ ((𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)) ↔ (𝐴 ∈ (𝑆 × 𝑆) ∧ (𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆))))
9	7, 8	sylibr 233	. 2 ⊢ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → (𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)))
10		eqid 2738	. . 3 ⊢ (𝑆 × 𝑆) = (𝑆 × 𝑆)
11		breq1 5073	. . . . 5 ⊢ (⟨𝑓, 𝑔⟩ = 𝐴 → (⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ↔ 𝐴 ∼ ⟨ℎ, 𝑡⟩))
12	11	anbi1d 629	. . . 4 ⊢ (⟨𝑓, 𝑔⟩ = 𝐴 → ((⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) ↔ (𝐴 ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩)))
13		breq1 5073	. . . 4 ⊢ (⟨𝑓, 𝑔⟩ = 𝐴 → (⟨𝑓, 𝑔⟩ ∼ ⟨𝑠, 𝑟⟩ ↔ 𝐴 ∼ ⟨𝑠, 𝑟⟩))
14	12, 13	imbi12d 344	. . 3 ⊢ (⟨𝑓, 𝑔⟩ = 𝐴 → (((⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) → ⟨𝑓, 𝑔⟩ ∼ ⟨𝑠, 𝑟⟩) ↔ ((𝐴 ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) → 𝐴 ∼ ⟨𝑠, 𝑟⟩)))
15		breq2 5074	. . . . 5 ⊢ (⟨ℎ, 𝑡⟩ = 𝐵 → (𝐴 ∼ ⟨ℎ, 𝑡⟩ ↔ 𝐴 ∼ 𝐵))
16		breq1 5073	. . . . 5 ⊢ (⟨ℎ, 𝑡⟩ = 𝐵 → (⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩ ↔ 𝐵 ∼ ⟨𝑠, 𝑟⟩))
17	15, 16	anbi12d 630	. . . 4 ⊢ (⟨ℎ, 𝑡⟩ = 𝐵 → ((𝐴 ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) ↔ (𝐴 ∼ 𝐵 ∧ 𝐵 ∼ ⟨𝑠, 𝑟⟩)))
18	17	imbi1d 341	. . 3 ⊢ (⟨ℎ, 𝑡⟩ = 𝐵 → (((𝐴 ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) → 𝐴 ∼ ⟨𝑠, 𝑟⟩) ↔ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ ⟨𝑠, 𝑟⟩) → 𝐴 ∼ ⟨𝑠, 𝑟⟩)))
19		breq2 5074	. . . . 5 ⊢ (⟨𝑠, 𝑟⟩ = 𝐶 → (𝐵 ∼ ⟨𝑠, 𝑟⟩ ↔ 𝐵 ∼ 𝐶))
20	19	anbi2d 628	. . . 4 ⊢ (⟨𝑠, 𝑟⟩ = 𝐶 → ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ ⟨𝑠, 𝑟⟩) ↔ (𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶)))
21		breq2 5074	. . . 4 ⊢ (⟨𝑠, 𝑟⟩ = 𝐶 → (𝐴 ∼ ⟨𝑠, 𝑟⟩ ↔ 𝐴 ∼ 𝐶))
22	20, 21	imbi12d 344	. . 3 ⊢ (⟨𝑠, 𝑟⟩ = 𝐶 → (((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ ⟨𝑠, 𝑟⟩) → 𝐴 ∼ ⟨𝑠, 𝑟⟩) ↔ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → 𝐴 ∼ 𝐶)))
23	1	ecopoveq 8565	. . . . . . . 8 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) → (⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ↔ (𝑓 + 𝑡) = (𝑔 + ℎ)))
24	23	3adant3 1130	. . . . . . 7 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ↔ (𝑓 + 𝑡) = (𝑔 + ℎ)))
25	1	ecopoveq 8565	. . . . . . . 8 ⊢ (((ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩ ↔ (ℎ + 𝑟) = (𝑡 + 𝑠)))
26	25	3adant1 1128	. . . . . . 7 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩ ↔ (ℎ + 𝑟) = (𝑡 + 𝑠)))
27	24, 26	anbi12d 630	. . . . . 6 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) ↔ ((𝑓 + 𝑡) = (𝑔 + ℎ) ∧ (ℎ + 𝑟) = (𝑡 + 𝑠))))
28		oveq12 7264	. . . . . . 7 ⊢ (((𝑓 + 𝑡) = (𝑔 + ℎ) ∧ (ℎ + 𝑟) = (𝑡 + 𝑠)) → ((𝑓 + 𝑡) + (ℎ + 𝑟)) = ((𝑔 + ℎ) + (𝑡 + 𝑠)))
29		vex 3426	. . . . . . . 8 ⊢ ℎ ∈ V
30		vex 3426	. . . . . . . 8 ⊢ 𝑡 ∈ V
31		vex 3426	. . . . . . . 8 ⊢ 𝑓 ∈ V
32		ecopopr.com	. . . . . . . 8 ⊢ (𝑥 + 𝑦) = (𝑦 + 𝑥)
33		ecopopr.ass	. . . . . . . 8 ⊢ ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))
34		vex 3426	. . . . . . . 8 ⊢ 𝑟 ∈ V
35	29, 30, 31, 32, 33, 34	caov411 7482	. . . . . . 7 ⊢ ((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((𝑓 + 𝑡) + (ℎ + 𝑟))
36		vex 3426	. . . . . . . . 9 ⊢ 𝑔 ∈ V
37		vex 3426	. . . . . . . . 9 ⊢ 𝑠 ∈ V
38	36, 30, 29, 32, 33, 37	caov411 7482	. . . . . . . 8 ⊢ ((𝑔 + 𝑡) + (ℎ + 𝑠)) = ((ℎ + 𝑡) + (𝑔 + 𝑠))
39	36, 30, 29, 32, 33, 37	caov4 7481	. . . . . . . 8 ⊢ ((𝑔 + 𝑡) + (ℎ + 𝑠)) = ((𝑔 + ℎ) + (𝑡 + 𝑠))
40	38, 39	eqtr3i 2768	. . . . . . 7 ⊢ ((ℎ + 𝑡) + (𝑔 + 𝑠)) = ((𝑔 + ℎ) + (𝑡 + 𝑠))
41	28, 35, 40	3eqtr4g 2804	. . . . . 6 ⊢ (((𝑓 + 𝑡) = (𝑔 + ℎ) ∧ (ℎ + 𝑟) = (𝑡 + 𝑠)) → ((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)))
42	27, 41	syl6bi 252	. . . . 5 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) → ((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠))))
43		ecopopr.cl	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)
44	43	caovcl 7444	. . . . . . . . . 10 ⊢ ((ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) → (ℎ + 𝑡) ∈ 𝑆)
45	43	caovcl 7444	. . . . . . . . . 10 ⊢ ((𝑓 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆) → (𝑓 + 𝑟) ∈ 𝑆)
46		ovex 7288	. . . . . . . . . . 11 ⊢ (𝑔 + 𝑠) ∈ V
47		ecopopr.can	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧))
48	46, 47	caovcan 7454	. . . . . . . . . 10 ⊢ (((ℎ + 𝑡) ∈ 𝑆 ∧ (𝑓 + 𝑟) ∈ 𝑆) → (((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
49	44, 45, 48	syl2an 595	. . . . . . . . 9 ⊢ (((ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑓 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
50	49	3impb 1113	. . . . . . . 8 ⊢ (((ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ 𝑓 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆) → (((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
51	50	3com12 1121	. . . . . . 7 ⊢ ((𝑓 ∈ 𝑆 ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ 𝑟 ∈ 𝑆) → (((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
52	51	3adant3l 1178	. . . . . 6 ⊢ ((𝑓 ∈ 𝑆 ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
53	52	3adant1r 1175	. . . . 5 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
54	42, 53	syld 47	. . . 4 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
55	1	ecopoveq 8565	. . . . 5 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (⟨𝑓, 𝑔⟩ ∼ ⟨𝑠, 𝑟⟩ ↔ (𝑓 + 𝑟) = (𝑔 + 𝑠)))
56	55	3adant2 1129	. . . 4 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (⟨𝑓, 𝑔⟩ ∼ ⟨𝑠, 𝑟⟩ ↔ (𝑓 + 𝑟) = (𝑔 + 𝑠)))
57	54, 56	sylibrd 258	. . 3 ⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((⟨𝑓, 𝑔⟩ ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) → ⟨𝑓, 𝑔⟩ ∼ ⟨𝑠, 𝑟⟩))
58	10, 14, 18, 22, 57	3optocl 5673	. 2 ⊢ ((𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)) → ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → 𝐴 ∼ 𝐶))
59	9, 58	mpcom 38	1 ⊢ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → 𝐴 ∼ 𝐶)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1539  ∃wex 1783   ∈ wcel 2108  ⟨cop 4564   class class class wbr 5070  {copab 5132   × cxp 5578  (class class class)co 7255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-xp 5586  df-iota 6376  df-fv 6426  df-ov 7258

This theorem is referenced by:  ecopover  8568