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	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in (S \times S) \land y \in (S \times S)) \land \exists z \exists w \exists v \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land z \underset{˙}{+} u = w \underset{˙}{+} v))\}$
	ecopopr.com	$⊢ x \underset{˙}{+} y = y \underset{˙}{+} x$
	ecopopr.cl	$⊢ (x \in S \land y \in S) \to x \underset{˙}{+} y \in S$
	ecopopr.ass	$⊢ (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
	ecopopr.can	$⊢ (x \in S \land y \in S) \to (x \underset{˙}{+} y = x \underset{˙}{+} z \to y = z)$
Assertion	ecopovtrn	$⊢ (A \underset{˙}{\sim} B \land B \underset{˙}{\sim} C) \to A \underset{˙}{\sim} C$

Proof

Step	Hyp	Ref	Expression
1		ecopopr.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in (S \times S) \land y \in (S \times S)) \land \exists z \exists w \exists v \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land z \underset{˙}{+} u = w \underset{˙}{+} v))\}$
2		ecopopr.com	$⊢ x \underset{˙}{+} y = y \underset{˙}{+} x$
3		ecopopr.cl	$⊢ (x \in S \land y \in S) \to x \underset{˙}{+} y \in S$
4		ecopopr.ass	$⊢ (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
5		ecopopr.can	$⊢ (x \in S \land y \in S) \to (x \underset{˙}{+} y = x \underset{˙}{+} z \to y = z)$
6		opabssxp	$⊢ \{⟨x, y⟩ \| ((x \in (S \times S) \land y \in (S \times S)) \land \exists z \exists w \exists v \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land z \underset{˙}{+} u = w \underset{˙}{+} v))\} \subseteq (S \times S) \times (S \times S)$
7	1 6	eqsstri	$⊢ \underset{˙}{\sim} \subseteq (S \times S) \times (S \times S)$
8	7	brel	$⊢ A \underset{˙}{\sim} B \to (A \in (S \times S) \land B \in (S \times S))$
9	8	simpld	$⊢ A \underset{˙}{\sim} B \to A \in (S \times S)$
10	7	brel	$⊢ B \underset{˙}{\sim} C \to (B \in (S \times S) \land C \in (S \times S))$
11	9 10	anim12i	$⊢ (A \underset{˙}{\sim} B \land B \underset{˙}{\sim} C) \to (A \in (S \times S) \land (B \in (S \times S) \land C \in (S \times S)))$
12		3anass	$⊢ (A \in (S \times S) \land B \in (S \times S) \land C \in (S \times S)) \leftrightarrow (A \in (S \times S) \land (B \in (S \times S) \land C \in (S \times S)))$
13	11 12	sylibr	$⊢ (A \underset{˙}{\sim} B \land B \underset{˙}{\sim} C) \to (A \in (S \times S) \land B \in (S \times S) \land C \in (S \times S))$
14		eqid	$⊢ S \times S = S \times S$
15		breq1	$⊢ ⟨f, g⟩ = A \to (⟨f, g⟩ \underset{˙}{\sim} ⟨h, t⟩ \leftrightarrow A \underset{˙}{\sim} ⟨h, t⟩)$
16	15	anbi1d	$⊢ ⟨f, g⟩ = A \to ((⟨f, g⟩ \underset{˙}{\sim} ⟨h, t⟩ \land ⟨h, t⟩ \underset{˙}{\sim} ⟨s, r⟩) \leftrightarrow (A \underset{˙}{\sim} ⟨h, t⟩ \land ⟨h, t⟩ \underset{˙}{\sim} ⟨s, r⟩))$
17		breq1	$⊢ ⟨f, g⟩ = A \to (⟨f, g⟩ \underset{˙}{\sim} ⟨s, r⟩ \leftrightarrow A \underset{˙}{\sim} ⟨s, r⟩)$
18	16 17	imbi12d	$⊢ ⟨f, g⟩ = A \to (((⟨f, g⟩ \underset{˙}{\sim} ⟨h, t⟩ \land ⟨h, t⟩ \underset{˙}{\sim} ⟨s, r⟩) \to ⟨f, g⟩ \underset{˙}{\sim} ⟨s, r⟩) \leftrightarrow ((A \underset{˙}{\sim} ⟨h, t⟩ \land ⟨h, t⟩ \underset{˙}{\sim} ⟨s, r⟩) \to A \underset{˙}{\sim} ⟨s, r⟩))$
19		breq2	$⊢ ⟨h, t⟩ = B \to (A \underset{˙}{\sim} ⟨h, t⟩ \leftrightarrow A \underset{˙}{\sim} B)$
20		breq1	$⊢ ⟨h, t⟩ = B \to (⟨h, t⟩ \underset{˙}{\sim} ⟨s, r⟩ \leftrightarrow B \underset{˙}{\sim} ⟨s, r⟩)$
21	19 20	anbi12d	$⊢ ⟨h, t⟩ = B \to ((A \underset{˙}{\sim} ⟨h, t⟩ \land ⟨h, t⟩ \underset{˙}{\sim} ⟨s, r⟩) \leftrightarrow (A \underset{˙}{\sim} B \land B \underset{˙}{\sim} ⟨s, r⟩))$
22	21	imbi1d	$⊢ ⟨h, t⟩ = B \to (((A \underset{˙}{\sim} ⟨h, t⟩ \land ⟨h, t⟩ \underset{˙}{\sim} ⟨s, r⟩) \to A \underset{˙}{\sim} ⟨s, r⟩) \leftrightarrow ((A \underset{˙}{\sim} B \land B \underset{˙}{\sim} ⟨s, r⟩) \to A \underset{˙}{\sim} ⟨s, r⟩))$
23		breq2	$⊢ ⟨s, r⟩ = C \to (B \underset{˙}{\sim} ⟨s, r⟩ \leftrightarrow B \underset{˙}{\sim} C)$
24	23	anbi2d	$⊢ ⟨s, r⟩ = C \to ((A \underset{˙}{\sim} B \land B \underset{˙}{\sim} ⟨s, r⟩) \leftrightarrow (A \underset{˙}{\sim} B \land B \underset{˙}{\sim} C))$
25		breq2	$⊢ ⟨s, r⟩ = C \to (A \underset{˙}{\sim} ⟨s, r⟩ \leftrightarrow A \underset{˙}{\sim} C)$
26	24 25	imbi12d	$⊢ ⟨s, r⟩ = C \to (((A \underset{˙}{\sim} B \land B \underset{˙}{\sim} ⟨s, r⟩) \to A \underset{˙}{\sim} ⟨s, r⟩) \leftrightarrow ((A \underset{˙}{\sim} B \land B \underset{˙}{\sim} C) \to A \underset{˙}{\sim} C))$
27	1	ecopoveq	$⊢ ((f \in S \land g \in S) \land (h \in S \land t \in S)) \to (⟨f, g⟩ \underset{˙}{\sim} ⟨h, t⟩ \leftrightarrow f \underset{˙}{+} t = g \underset{˙}{+} h)$
28	27	3adant3	$⊢ ((f \in S \land g \in S) \land (h \in S \land t \in S) \land (s \in S \land r \in S)) \to (⟨f, g⟩ \underset{˙}{\sim} ⟨h, t⟩ \leftrightarrow f \underset{˙}{+} t = g \underset{˙}{+} h)$
29	1	ecopoveq	$⊢ ((h \in S \land t \in S) \land (s \in S \land r \in S)) \to (⟨h, t⟩ \underset{˙}{\sim} ⟨s, r⟩ \leftrightarrow h \underset{˙}{+} r = t \underset{˙}{+} s)$
30	29	3adant1	$⊢ ((f \in S \land g \in S) \land (h \in S \land t \in S) \land (s \in S \land r \in S)) \to (⟨h, t⟩ \underset{˙}{\sim} ⟨s, r⟩ \leftrightarrow h \underset{˙}{+} r = t \underset{˙}{+} s)$
31	28 30	anbi12d	$⊢ ((f \in S \land g \in S) \land (h \in S \land t \in S) \land (s \in S \land r \in S)) \to ((⟨f, g⟩ \underset{˙}{\sim} ⟨h, t⟩ \land ⟨h, t⟩ \underset{˙}{\sim} ⟨s, r⟩) \leftrightarrow (f \underset{˙}{+} t = g \underset{˙}{+} h \land h \underset{˙}{+} r = t \underset{˙}{+} s))$
32		oveq12	$⊢ (f \underset{˙}{+} t = g \underset{˙}{+} h \land h \underset{˙}{+} r = t \underset{˙}{+} s) \to (f \underset{˙}{+} t) \underset{˙}{+} (h \underset{˙}{+} r) = (g \underset{˙}{+} h) \underset{˙}{+} (t \underset{˙}{+} s)$
33		vex	$⊢ h \in V$
34		vex	$⊢ t \in V$
35		vex	$⊢ f \in V$
36		vex	$⊢ r \in V$
37	33 34 35 2 4 36	caov411	$⊢ (h \underset{˙}{+} t) \underset{˙}{+} (f \underset{˙}{+} r) = (f \underset{˙}{+} t) \underset{˙}{+} (h \underset{˙}{+} r)$
38		vex	$⊢ g \in V$
39		vex	$⊢ s \in V$
40	38 34 33 2 4 39	caov411	$⊢ (g \underset{˙}{+} t) \underset{˙}{+} (h \underset{˙}{+} s) = (h \underset{˙}{+} t) \underset{˙}{+} (g \underset{˙}{+} s)$
41	38 34 33 2 4 39	caov4	$⊢ (g \underset{˙}{+} t) \underset{˙}{+} (h \underset{˙}{+} s) = (g \underset{˙}{+} h) \underset{˙}{+} (t \underset{˙}{+} s)$
42	40 41	eqtr3i	$⊢ (h \underset{˙}{+} t) \underset{˙}{+} (g \underset{˙}{+} s) = (g \underset{˙}{+} h) \underset{˙}{+} (t \underset{˙}{+} s)$
43	32 37 42	3eqtr4g	$⊢ (f \underset{˙}{+} t = g \underset{˙}{+} h \land h \underset{˙}{+} r = t \underset{˙}{+} s) \to (h \underset{˙}{+} t) \underset{˙}{+} (f \underset{˙}{+} r) = (h \underset{˙}{+} t) \underset{˙}{+} (g \underset{˙}{+} s)$
44	31 43	syl6bi	$⊢ ((f \in S \land g \in S) \land (h \in S \land t \in S) \land (s \in S \land r \in S)) \to ((⟨f, g⟩ \underset{˙}{\sim} ⟨h, t⟩ \land ⟨h, t⟩ \underset{˙}{\sim} ⟨s, r⟩) \to (h \underset{˙}{+} t) \underset{˙}{+} (f \underset{˙}{+} r) = (h \underset{˙}{+} t) \underset{˙}{+} (g \underset{˙}{+} s))$
45	3	caovcl	$⊢ (h \in S \land t \in S) \to h \underset{˙}{+} t \in S$
46	3	caovcl	$⊢ (f \in S \land r \in S) \to f \underset{˙}{+} r \in S$
47		ovex	$⊢ g \underset{˙}{+} s \in V$
48	47 5	caovcan	$⊢ (h \underset{˙}{+} t \in S \land f \underset{˙}{+} r \in S) \to ((h \underset{˙}{+} t) \underset{˙}{+} (f \underset{˙}{+} r) = (h \underset{˙}{+} t) \underset{˙}{+} (g \underset{˙}{+} s) \to f \underset{˙}{+} r = g \underset{˙}{+} s)$
49	45 46 48	syl2an	$⊢ ((h \in S \land t \in S) \land (f \in S \land r \in S)) \to ((h \underset{˙}{+} t) \underset{˙}{+} (f \underset{˙}{+} r) = (h \underset{˙}{+} t) \underset{˙}{+} (g \underset{˙}{+} s) \to f \underset{˙}{+} r = g \underset{˙}{+} s)$
50	49	3impb	$⊢ ((h \in S \land t \in S) \land f \in S \land r \in S) \to ((h \underset{˙}{+} t) \underset{˙}{+} (f \underset{˙}{+} r) = (h \underset{˙}{+} t) \underset{˙}{+} (g \underset{˙}{+} s) \to f \underset{˙}{+} r = g \underset{˙}{+} s)$
51	50	3com12	$⊢ (f \in S \land (h \in S \land t \in S) \land r \in S) \to ((h \underset{˙}{+} t) \underset{˙}{+} (f \underset{˙}{+} r) = (h \underset{˙}{+} t) \underset{˙}{+} (g \underset{˙}{+} s) \to f \underset{˙}{+} r = g \underset{˙}{+} s)$
52	51	3adant3l	$⊢ (f \in S \land (h \in S \land t \in S) \land (s \in S \land r \in S)) \to ((h \underset{˙}{+} t) \underset{˙}{+} (f \underset{˙}{+} r) = (h \underset{˙}{+} t) \underset{˙}{+} (g \underset{˙}{+} s) \to f \underset{˙}{+} r = g \underset{˙}{+} s)$
53	52	3adant1r	$⊢ ((f \in S \land g \in S) \land (h \in S \land t \in S) \land (s \in S \land r \in S)) \to ((h \underset{˙}{+} t) \underset{˙}{+} (f \underset{˙}{+} r) = (h \underset{˙}{+} t) \underset{˙}{+} (g \underset{˙}{+} s) \to f \underset{˙}{+} r = g \underset{˙}{+} s)$
54	44 53	syld	$⊢ ((f \in S \land g \in S) \land (h \in S \land t \in S) \land (s \in S \land r \in S)) \to ((⟨f, g⟩ \underset{˙}{\sim} ⟨h, t⟩ \land ⟨h, t⟩ \underset{˙}{\sim} ⟨s, r⟩) \to f \underset{˙}{+} r = g \underset{˙}{+} s)$
55	1	ecopoveq	$⊢ ((f \in S \land g \in S) \land (s \in S \land r \in S)) \to (⟨f, g⟩ \underset{˙}{\sim} ⟨s, r⟩ \leftrightarrow f \underset{˙}{+} r = g \underset{˙}{+} s)$
56	55	3adant2	$⊢ ((f \in S \land g \in S) \land (h \in S \land t \in S) \land (s \in S \land r \in S)) \to (⟨f, g⟩ \underset{˙}{\sim} ⟨s, r⟩ \leftrightarrow f \underset{˙}{+} r = g \underset{˙}{+} s)$
57	54 56	sylibrd	$⊢ ((f \in S \land g \in S) \land (h \in S \land t \in S) \land (s \in S \land r \in S)) \to ((⟨f, g⟩ \underset{˙}{\sim} ⟨h, t⟩ \land ⟨h, t⟩ \underset{˙}{\sim} ⟨s, r⟩) \to ⟨f, g⟩ \underset{˙}{\sim} ⟨s, r⟩)$
58	14 18 22 26 57	3optocl	$⊢ (A \in (S \times S) \land B \in (S \times S) \land C \in (S \times S)) \to ((A \underset{˙}{\sim} B \land B \underset{˙}{\sim} C) \to A \underset{˙}{\sim} C)$
59	13 58	mpcom	$⊢ (A \underset{˙}{\sim} B \land B \underset{˙}{\sim} C) \to A \underset{˙}{\sim} C$

Metamath Proof Explorer

Theorem ecopovtrn

Proof