iscgra

Description: Property for two angles ABC and DEF to be congruent. This is a modified version of the definition 11.3 of Schwabhauser p. 95. where the number of constructed points has been reduced to two. We chose this version rather than the textbook version because it is shorter and therefore simpler to work with. Theorem dfcgra2 shows that those definitions are indeed equivalent. (Contributed by Thierry Arnoux, 31-Jul-2020)

	Ref	Expression
Hypotheses	iscgra.p	$⊢ P = {Base}_{G}$
	iscgra.i	$⊢ I = Itv (G)$
	iscgra.k	$⊢ K = {hl}_{𝒢} (G)$
	iscgra.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	iscgra.a	$⊢ φ \to A \in P$
	iscgra.b	$⊢ φ \to B \in P$
	iscgra.c	$⊢ φ \to C \in P$
	iscgra.d	$⊢ φ \to D \in P$
	iscgra.e	$⊢ φ \to E \in P$
	iscgra.f	$⊢ φ \to F \in P$
Assertion	iscgra	$⊢ φ \to (⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \leftrightarrow \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F))$

Proof

Step	Hyp	Ref	Expression
1		iscgra.p	$⊢ P = {Base}_{G}$
2		iscgra.i	$⊢ I = Itv (G)$
3		iscgra.k	$⊢ K = {hl}_{𝒢} (G)$
4		iscgra.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		iscgra.a	$⊢ φ \to A \in P$
6		iscgra.b	$⊢ φ \to B \in P$
7		iscgra.c	$⊢ φ \to C \in P$
8		iscgra.d	$⊢ φ \to D \in P$
9		iscgra.e	$⊢ φ \to E \in P$
10		iscgra.f	$⊢ φ \to F \in P$
11		simpl	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to a = ⟨“ A B C ”⟩$
12		eqidd	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to x = x$
13		simpr	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to b = ⟨“ D E F ”⟩$
14	13	fveq1d	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to b (1) = ⟨“ D E F ”⟩ (1)$
15		eqidd	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to y = y$
16	12 14 15	s3eqd	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to ⟨“ x b (1) y ”⟩ = ⟨“ x ⟨“ D E F ”⟩ (1) y ”⟩$
17	11 16	breq12d	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \leftrightarrow ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x ⟨“ D E F ”⟩ (1) y ”⟩)$
18	14	fveq2d	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to K (b (1)) = K (⟨“ D E F ”⟩ (1))$
19	13	fveq1d	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to b (0) = ⟨“ D E F ”⟩ (0)$
20	12 18 19	breq123d	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to (x K (b (1)) b (0) \leftrightarrow x K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (0))$
21	13	fveq1d	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to b (2) = ⟨“ D E F ”⟩ (2)$
22	15 18 21	breq123d	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to (y K (b (1)) b (2) \leftrightarrow y K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (2))$
23	17 20 22	3anbi123d	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to ((a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)) \leftrightarrow (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x ⟨“ D E F ”⟩ (1) y ”⟩ \land x K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (0) \land y K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (2)))$
24	23	2rexbidv	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to (\exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)) \leftrightarrow \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x ⟨“ D E F ”⟩ (1) y ”⟩ \land x K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (0) \land y K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (2)))$
25		eqid	$⊢ \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\} = \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\}$
26	24 25	brab2a	$⊢ ⟨“ A B C ”⟩ \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\} ⟨“ D E F ”⟩ \leftrightarrow ((⟨“ A B C ”⟩ \in (P^{(0 ..^3)}) \land ⟨“ D E F ”⟩ \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x ⟨“ D E F ”⟩ (1) y ”⟩ \land x K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (0) \land y K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (2)))$
27		eqidd	$⊢ (φ \land (x \in P \land y \in P)) \to x = x$
28		s3fv1	$⊢ E \in P \to ⟨“ D E F ”⟩ (1) = E$
29	9 28	syl	$⊢ φ \to ⟨“ D E F ”⟩ (1) = E$
30	29	adantr	$⊢ (φ \land (x \in P \land y \in P)) \to ⟨“ D E F ”⟩ (1) = E$
31		eqidd	$⊢ (φ \land (x \in P \land y \in P)) \to y = y$
32	27 30 31	s3eqd	$⊢ (φ \land (x \in P \land y \in P)) \to ⟨“ x ⟨“ D E F ”⟩ (1) y ”⟩ = ⟨“ x E y ”⟩$
33	32	breq2d	$⊢ (φ \land (x \in P \land y \in P)) \to (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x ⟨“ D E F ”⟩ (1) y ”⟩ \leftrightarrow ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩)$
34	30	fveq2d	$⊢ (φ \land (x \in P \land y \in P)) \to K (⟨“ D E F ”⟩ (1)) = K (E)$
35		s3fv0	$⊢ D \in P \to ⟨“ D E F ”⟩ (0) = D$
36	8 35	syl	$⊢ φ \to ⟨“ D E F ”⟩ (0) = D$
37	36	adantr	$⊢ (φ \land (x \in P \land y \in P)) \to ⟨“ D E F ”⟩ (0) = D$
38	27 34 37	breq123d	$⊢ (φ \land (x \in P \land y \in P)) \to (x K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (0) \leftrightarrow x K (E) D)$
39		s3fv2	$⊢ F \in P \to ⟨“ D E F ”⟩ (2) = F$
40	10 39	syl	$⊢ φ \to ⟨“ D E F ”⟩ (2) = F$
41	40	adantr	$⊢ (φ \land (x \in P \land y \in P)) \to ⟨“ D E F ”⟩ (2) = F$
42	31 34 41	breq123d	$⊢ (φ \land (x \in P \land y \in P)) \to (y K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (2) \leftrightarrow y K (E) F)$
43	33 38 42	3anbi123d	$⊢ (φ \land (x \in P \land y \in P)) \to ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x ⟨“ D E F ”⟩ (1) y ”⟩ \land x K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (0) \land y K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (2)) \leftrightarrow (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F))$
44	43	2rexbidva	$⊢ φ \to (\exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x ⟨“ D E F ”⟩ (1) y ”⟩ \land x K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (0) \land y K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (2)) \leftrightarrow \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F))$
45	44	anbi2d	$⊢ φ \to (((⟨“ A B C ”⟩ \in (P^{(0 ..^3)}) \land ⟨“ D E F ”⟩ \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x ⟨“ D E F ”⟩ (1) y ”⟩ \land x K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (0) \land y K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (2))) \leftrightarrow ((⟨“ A B C ”⟩ \in (P^{(0 ..^3)}) \land ⟨“ D E F ”⟩ \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)))$
46	26 45	bitrid	$⊢ φ \to (⟨“ A B C ”⟩ \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\} ⟨“ D E F ”⟩ \leftrightarrow ((⟨“ A B C ”⟩ \in (P^{(0 ..^3)}) \land ⟨“ D E F ”⟩ \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)))$
47		elex	$⊢ G \in 𝒢_{Tarski} \to G \in V$
48		simpl	$⊢ (p = P \land k = K) \to p = P$
49	48	oveq1d	$⊢ (p = P \land k = K) \to p^{(0 ..^3)} = P^{(0 ..^3)}$
50	49	eleq2d	$⊢ (p = P \land k = K) \to (a \in (p^{(0 ..^3)}) \leftrightarrow a \in (P^{(0 ..^3)}))$
51	49	eleq2d	$⊢ (p = P \land k = K) \to (b \in (p^{(0 ..^3)}) \leftrightarrow b \in (P^{(0 ..^3)}))$
52	50 51	anbi12d	$⊢ (p = P \land k = K) \to ((a \in (p^{(0 ..^3)}) \land b \in (p^{(0 ..^3)})) \leftrightarrow (a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})))$
53		simpr	$⊢ (p = P \land k = K) \to k = K$
54	53	fveq1d	$⊢ (p = P \land k = K) \to k (b (1)) = K (b (1))$
55	54	breqd	$⊢ (p = P \land k = K) \to (x k (b (1)) b (0) \leftrightarrow x K (b (1)) b (0))$
56	54	breqd	$⊢ (p = P \land k = K) \to (y k (b (1)) b (2) \leftrightarrow y K (b (1)) b (2))$
57	55 56	3anbi23d	$⊢ (p = P \land k = K) \to ((a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2)) \leftrightarrow (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))$
58	48 57	rexeqbidv	$⊢ (p = P \land k = K) \to (\exists y \in p (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2)) \leftrightarrow \exists y \in P (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))$
59	48 58	rexeqbidv	$⊢ (p = P \land k = K) \to (\exists x \in p \exists y \in p (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2)) \leftrightarrow \exists x \in P \exists y \in P (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))$
60	52 59	anbi12d	$⊢ (p = P \land k = K) \to (((a \in (p^{(0 ..^3)}) \land b \in (p^{(0 ..^3)})) \land \exists x \in p \exists y \in p (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2))) \leftrightarrow ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2))))$
61	1 3 60	sbcie2s	$⊢ g = G \to (\underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} {hl}_{𝒢} (g) / k \underset{˙}{]} ((a \in (p^{(0 ..^3)}) \land b \in (p^{(0 ..^3)})) \land \exists x \in p \exists y \in p (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2))) \leftrightarrow ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2))))$
62	61	opabbidv	$⊢ g = G \to \{⟨a, b⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} {hl}_{𝒢} (g) / k \underset{˙}{]} ((a \in (p^{(0 ..^3)}) \land b \in (p^{(0 ..^3)})) \land \exists x \in p \exists y \in p (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2)))\} = \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\}$
63		fveq2	$⊢ g = G \to \sim_{𝒢} (g) = \sim_{𝒢} (G)$
64	63	breqd	$⊢ g = G \to (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \leftrightarrow a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩)$
65	64	3anbi1d	$⊢ g = G \to ((a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)) \leftrightarrow (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))$
66	65	2rexbidv	$⊢ g = G \to (\exists x \in P \exists y \in P (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)) \leftrightarrow \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))$
67	66	anbi2d	$⊢ g = G \to (((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2))) \leftrightarrow ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2))))$
68	67	opabbidv	$⊢ g = G \to \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\} = \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\}$
69	62 68	eqtrd	$⊢ g = G \to \{⟨a, b⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} {hl}_{𝒢} (g) / k \underset{˙}{]} ((a \in (p^{(0 ..^3)}) \land b \in (p^{(0 ..^3)})) \land \exists x \in p \exists y \in p (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2)))\} = \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\}$
70		df-cgra	$⊢ \sim_{𝒢}^{∠} = (g \in V ⟼ \{⟨a, b⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} {hl}_{𝒢} (g) / k \underset{˙}{]} ((a \in (p^{(0 ..^3)}) \land b \in (p^{(0 ..^3)})) \land \exists x \in p \exists y \in p (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2)))\})$
71		ovex	$⊢ P^{(0 ..^3)} \in V$
72	71 71	xpex	$⊢ (P^{(0 ..^3)}) \times (P^{(0 ..^3)}) \in V$
73		opabssxp	$⊢ \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\} \subseteq (P^{(0 ..^3)}) \times (P^{(0 ..^3)})$
74	72 73	ssexi	$⊢ \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\} \in V$
75	69 70 74	fvmpt	$⊢ G \in V \to \sim_{𝒢}^{∠} (G) = \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\}$
76	4 47 75	3syl	$⊢ φ \to \sim_{𝒢}^{∠} (G) = \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\}$
77	76	breqd	$⊢ φ \to (⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \leftrightarrow ⟨“ A B C ”⟩ \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\} ⟨“ D E F ”⟩)$
78	5 6 7	s3cld	$⊢ φ \to ⟨“ A B C ”⟩ \in Word P$
79		s3len	$⊢ \|⟨“ A B C ”⟩\| = 3$
80	1	fvexi	$⊢ P \in V$
81		3nn0	$⊢ 3 \in ℕ_{0}$
82		wrdmap	$⊢ (P \in V \land 3 \in ℕ_{0}) \to ((⟨“ A B C ”⟩ \in Word P \land \|⟨“ A B C ”⟩\| = 3) \leftrightarrow ⟨“ A B C ”⟩ \in (P^{(0 ..^3)}))$
83	80 81 82	mp2an	$⊢ (⟨“ A B C ”⟩ \in Word P \land \|⟨“ A B C ”⟩\| = 3) \leftrightarrow ⟨“ A B C ”⟩ \in (P^{(0 ..^3)})$
84	78 79 83	sylanblc	$⊢ φ \to ⟨“ A B C ”⟩ \in (P^{(0 ..^3)})$
85	8 9 10	s3cld	$⊢ φ \to ⟨“ D E F ”⟩ \in Word P$
86		s3len	$⊢ \|⟨“ D E F ”⟩\| = 3$
87		wrdmap	$⊢ (P \in V \land 3 \in ℕ_{0}) \to ((⟨“ D E F ”⟩ \in Word P \land \|⟨“ D E F ”⟩\| = 3) \leftrightarrow ⟨“ D E F ”⟩ \in (P^{(0 ..^3)}))$
88	80 81 87	mp2an	$⊢ (⟨“ D E F ”⟩ \in Word P \land \|⟨“ D E F ”⟩\| = 3) \leftrightarrow ⟨“ D E F ”⟩ \in (P^{(0 ..^3)})$
89	85 86 88	sylanblc	$⊢ φ \to ⟨“ D E F ”⟩ \in (P^{(0 ..^3)})$
90	84 89	jca	$⊢ φ \to (⟨“ A B C ”⟩ \in (P^{(0 ..^3)}) \land ⟨“ D E F ”⟩ \in (P^{(0 ..^3)}))$
91	90	biantrurd	$⊢ φ \to (\exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F) \leftrightarrow ((⟨“ A B C ”⟩ \in (P^{(0 ..^3)}) \land ⟨“ D E F ”⟩ \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)))$
92	46 77 91	3bitr4d	$⊢ φ \to (⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \leftrightarrow \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F))$

Metamath Proof Explorer

Theorem iscgra

Proof