brfs

Description: Binary relation form of the general five segment predicate. (Contributed by Scott Fenton, 5-Oct-2013)

		Ref	Expression
	Assertion	brfs	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ FiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \leftrightarrow (A Colinear ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)))$

Proof

Step	Hyp	Ref	Expression
1		breq1	$⊢ a = A \to (a Colinear ⟨b, c⟩ \leftrightarrow A Colinear ⟨b, c⟩)$
2		opeq1	$⊢ a = A \to ⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨b, c⟩⟩$
3	2	breq1d	$⊢ a = A \to (⟨a, ⟨b, c⟩⟩ Cgr3 ⟨e, ⟨f, g⟩⟩ \leftrightarrow ⟨A, ⟨b, c⟩⟩ Cgr3 ⟨e, ⟨f, g⟩⟩)$
4		opeq1	$⊢ a = A \to ⟨a, d⟩ = ⟨A, d⟩$
5	4	breq1d	$⊢ a = A \to (⟨a, d⟩ Cgr ⟨e, h⟩ \leftrightarrow ⟨A, d⟩ Cgr ⟨e, h⟩)$
6	5	anbi1d	$⊢ a = A \to ((⟨a, d⟩ Cgr ⟨e, h⟩ \land ⟨b, d⟩ Cgr ⟨f, h⟩) \leftrightarrow (⟨A, d⟩ Cgr ⟨e, h⟩ \land ⟨b, d⟩ Cgr ⟨f, h⟩))$
7	1 3 6	3anbi123d	$⊢ a = A \to ((a Colinear ⟨b, c⟩ \land ⟨a, ⟨b, c⟩⟩ Cgr3 ⟨e, ⟨f, g⟩⟩ \land (⟨a, d⟩ Cgr ⟨e, h⟩ \land ⟨b, d⟩ Cgr ⟨f, h⟩)) \leftrightarrow (A Colinear ⟨b, c⟩ \land ⟨A, ⟨b, c⟩⟩ Cgr3 ⟨e, ⟨f, g⟩⟩ \land (⟨A, d⟩ Cgr ⟨e, h⟩ \land ⟨b, d⟩ Cgr ⟨f, h⟩)))$
8		opeq1	$⊢ b = B \to ⟨b, c⟩ = ⟨B, c⟩$
9	8	breq2d	$⊢ b = B \to (A Colinear ⟨b, c⟩ \leftrightarrow A Colinear ⟨B, c⟩)$
10	8	opeq2d	$⊢ b = B \to ⟨A, ⟨b, c⟩⟩ = ⟨A, ⟨B, c⟩⟩$
11	10	breq1d	$⊢ b = B \to (⟨A, ⟨b, c⟩⟩ Cgr3 ⟨e, ⟨f, g⟩⟩ \leftrightarrow ⟨A, ⟨B, c⟩⟩ Cgr3 ⟨e, ⟨f, g⟩⟩)$
12		opeq1	$⊢ b = B \to ⟨b, d⟩ = ⟨B, d⟩$
13	12	breq1d	$⊢ b = B \to (⟨b, d⟩ Cgr ⟨f, h⟩ \leftrightarrow ⟨B, d⟩ Cgr ⟨f, h⟩)$
14	13	anbi2d	$⊢ b = B \to ((⟨A, d⟩ Cgr ⟨e, h⟩ \land ⟨b, d⟩ Cgr ⟨f, h⟩) \leftrightarrow (⟨A, d⟩ Cgr ⟨e, h⟩ \land ⟨B, d⟩ Cgr ⟨f, h⟩))$
15	9 11 14	3anbi123d	$⊢ b = B \to ((A Colinear ⟨b, c⟩ \land ⟨A, ⟨b, c⟩⟩ Cgr3 ⟨e, ⟨f, g⟩⟩ \land (⟨A, d⟩ Cgr ⟨e, h⟩ \land ⟨b, d⟩ Cgr ⟨f, h⟩)) \leftrightarrow (A Colinear ⟨B, c⟩ \land ⟨A, ⟨B, c⟩⟩ Cgr3 ⟨e, ⟨f, g⟩⟩ \land (⟨A, d⟩ Cgr ⟨e, h⟩ \land ⟨B, d⟩ Cgr ⟨f, h⟩)))$
16		opeq2	$⊢ c = C \to ⟨B, c⟩ = ⟨B, C⟩$
17	16	breq2d	$⊢ c = C \to (A Colinear ⟨B, c⟩ \leftrightarrow A Colinear ⟨B, C⟩)$
18	16	opeq2d	$⊢ c = C \to ⟨A, ⟨B, c⟩⟩ = ⟨A, ⟨B, C⟩⟩$
19	18	breq1d	$⊢ c = C \to (⟨A, ⟨B, c⟩⟩ Cgr3 ⟨e, ⟨f, g⟩⟩ \leftrightarrow ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨e, ⟨f, g⟩⟩)$
20	17 19	3anbi12d	$⊢ c = C \to ((A Colinear ⟨B, c⟩ \land ⟨A, ⟨B, c⟩⟩ Cgr3 ⟨e, ⟨f, g⟩⟩ \land (⟨A, d⟩ Cgr ⟨e, h⟩ \land ⟨B, d⟩ Cgr ⟨f, h⟩)) \leftrightarrow (A Colinear ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨e, ⟨f, g⟩⟩ \land (⟨A, d⟩ Cgr ⟨e, h⟩ \land ⟨B, d⟩ Cgr ⟨f, h⟩)))$
21		opeq2	$⊢ d = D \to ⟨A, d⟩ = ⟨A, D⟩$
22	21	breq1d	$⊢ d = D \to (⟨A, d⟩ Cgr ⟨e, h⟩ \leftrightarrow ⟨A, D⟩ Cgr ⟨e, h⟩)$
23		opeq2	$⊢ d = D \to ⟨B, d⟩ = ⟨B, D⟩$
24	23	breq1d	$⊢ d = D \to (⟨B, d⟩ Cgr ⟨f, h⟩ \leftrightarrow ⟨B, D⟩ Cgr ⟨f, h⟩)$
25	22 24	anbi12d	$⊢ d = D \to ((⟨A, d⟩ Cgr ⟨e, h⟩ \land ⟨B, d⟩ Cgr ⟨f, h⟩) \leftrightarrow (⟨A, D⟩ Cgr ⟨e, h⟩ \land ⟨B, D⟩ Cgr ⟨f, h⟩))$
26	25	3anbi3d	$⊢ d = D \to ((A Colinear ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨e, ⟨f, g⟩⟩ \land (⟨A, d⟩ Cgr ⟨e, h⟩ \land ⟨B, d⟩ Cgr ⟨f, h⟩)) \leftrightarrow (A Colinear ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨e, ⟨f, g⟩⟩ \land (⟨A, D⟩ Cgr ⟨e, h⟩ \land ⟨B, D⟩ Cgr ⟨f, h⟩)))$
27		opeq1	$⊢ e = E \to ⟨e, ⟨f, g⟩⟩ = ⟨E, ⟨f, g⟩⟩$
28	27	breq2d	$⊢ e = E \to (⟨A, ⟨B, C⟩⟩ Cgr3 ⟨e, ⟨f, g⟩⟩ \leftrightarrow ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨f, g⟩⟩)$
29		opeq1	$⊢ e = E \to ⟨e, h⟩ = ⟨E, h⟩$
30	29	breq2d	$⊢ e = E \to (⟨A, D⟩ Cgr ⟨e, h⟩ \leftrightarrow ⟨A, D⟩ Cgr ⟨E, h⟩)$
31	30	anbi1d	$⊢ e = E \to ((⟨A, D⟩ Cgr ⟨e, h⟩ \land ⟨B, D⟩ Cgr ⟨f, h⟩) \leftrightarrow (⟨A, D⟩ Cgr ⟨E, h⟩ \land ⟨B, D⟩ Cgr ⟨f, h⟩))$
32	28 31	3anbi23d	$⊢ e = E \to ((A Colinear ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨e, ⟨f, g⟩⟩ \land (⟨A, D⟩ Cgr ⟨e, h⟩ \land ⟨B, D⟩ Cgr ⟨f, h⟩)) \leftrightarrow (A Colinear ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨f, g⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, h⟩ \land ⟨B, D⟩ Cgr ⟨f, h⟩)))$
33		opeq1	$⊢ f = F \to ⟨f, g⟩ = ⟨F, g⟩$
34	33	opeq2d	$⊢ f = F \to ⟨E, ⟨f, g⟩⟩ = ⟨E, ⟨F, g⟩⟩$
35	34	breq2d	$⊢ f = F \to (⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨f, g⟩⟩ \leftrightarrow ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, g⟩⟩)$
36		opeq1	$⊢ f = F \to ⟨f, h⟩ = ⟨F, h⟩$
37	36	breq2d	$⊢ f = F \to (⟨B, D⟩ Cgr ⟨f, h⟩ \leftrightarrow ⟨B, D⟩ Cgr ⟨F, h⟩)$
38	37	anbi2d	$⊢ f = F \to ((⟨A, D⟩ Cgr ⟨E, h⟩ \land ⟨B, D⟩ Cgr ⟨f, h⟩) \leftrightarrow (⟨A, D⟩ Cgr ⟨E, h⟩ \land ⟨B, D⟩ Cgr ⟨F, h⟩))$
39	35 38	3anbi23d	$⊢ f = F \to ((A Colinear ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨f, g⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, h⟩ \land ⟨B, D⟩ Cgr ⟨f, h⟩)) \leftrightarrow (A Colinear ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, g⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, h⟩ \land ⟨B, D⟩ Cgr ⟨F, h⟩)))$
40		opeq2	$⊢ g = G \to ⟨F, g⟩ = ⟨F, G⟩$
41	40	opeq2d	$⊢ g = G \to ⟨E, ⟨F, g⟩⟩ = ⟨E, ⟨F, G⟩⟩$
42	41	breq2d	$⊢ g = G \to (⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, g⟩⟩ \leftrightarrow ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩)$
43	42	3anbi2d	$⊢ g = G \to ((A Colinear ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, g⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, h⟩ \land ⟨B, D⟩ Cgr ⟨F, h⟩)) \leftrightarrow (A Colinear ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, h⟩ \land ⟨B, D⟩ Cgr ⟨F, h⟩)))$
44		opeq2	$⊢ h = H \to ⟨E, h⟩ = ⟨E, H⟩$
45	44	breq2d	$⊢ h = H \to (⟨A, D⟩ Cgr ⟨E, h⟩ \leftrightarrow ⟨A, D⟩ Cgr ⟨E, H⟩)$
46		opeq2	$⊢ h = H \to ⟨F, h⟩ = ⟨F, H⟩$
47	46	breq2d	$⊢ h = H \to (⟨B, D⟩ Cgr ⟨F, h⟩ \leftrightarrow ⟨B, D⟩ Cgr ⟨F, H⟩)$
48	45 47	anbi12d	$⊢ h = H \to ((⟨A, D⟩ Cgr ⟨E, h⟩ \land ⟨B, D⟩ Cgr ⟨F, h⟩) \leftrightarrow (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))$
49	48	3anbi3d	$⊢ h = H \to ((A Colinear ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, h⟩ \land ⟨B, D⟩ Cgr ⟨F, h⟩)) \leftrightarrow (A Colinear ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)))$
50		fveq2	$⊢ n = N \to 𝔼 (n) = 𝔼 (N)$
51		df-fs	$⊢ FiveSeg = \{⟨p, q⟩ \| \exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) \exists e \in 𝔼 (n) \exists f \in 𝔼 (n) \exists g \in 𝔼 (n) \exists h \in 𝔼 (n) (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land (a Colinear ⟨b, c⟩ \land ⟨a, ⟨b, c⟩⟩ Cgr3 ⟨e, ⟨f, g⟩⟩ \land (⟨a, d⟩ Cgr ⟨e, h⟩ \land ⟨b, d⟩ Cgr ⟨f, h⟩)))\}$
52	7 15 20 26 32 39 43 49 50 51	br8	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ FiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \leftrightarrow (A Colinear ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)))$

Metamath Proof Explorer

Theorem brfs

Proof