iseqlg

Description: Property of a triangle being equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020)

	Ref	Expression
Hypotheses	iseqlg.p	$⊢ P = {Base}_{G}$
	iseqlg.m	$⊢ \underset{˙}{-} = dist (G)$
	iseqlg.i	$⊢ I = Itv (G)$
	iseqlg.l	$⊢ L = {Line}_{𝒢} (G)$
	iseqlg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	iseqlg.a	$⊢ φ \to A \in P$
	iseqlg.b	$⊢ φ \to B \in P$
	iseqlg.c	$⊢ φ \to C \in P$
Assertion	iseqlg	$⊢ φ \to (⟨“ A B C ”⟩ \in {Equilaterals}_{𝒢} (G) \leftrightarrow ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ B C A ”⟩)$

Proof

Step	Hyp	Ref	Expression
1		iseqlg.p	$⊢ P = {Base}_{G}$
2		iseqlg.m	$⊢ \underset{˙}{-} = dist (G)$
3		iseqlg.i	$⊢ I = Itv (G)$
4		iseqlg.l	$⊢ L = {Line}_{𝒢} (G)$
5		iseqlg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		iseqlg.a	$⊢ φ \to A \in P$
7		iseqlg.b	$⊢ φ \to B \in P$
8		iseqlg.c	$⊢ φ \to C \in P$
9		elex	$⊢ G \in 𝒢_{Tarski} \to G \in V$
10		fveq2	$⊢ g = G \to {Base}_{g} = {Base}_{G}$
11	10 1	eqtr4di	$⊢ g = G \to {Base}_{g} = P$
12	11	oveq1d	$⊢ g = G \to {Base}_{g}^{(0 ..^3)} = P^{(0 ..^3)}$
13		fveq2	$⊢ g = G \to \sim_{𝒢} (g) = \sim_{𝒢} (G)$
14	13	breqd	$⊢ g = G \to (x \sim_{𝒢} (g) ⟨“ x (1) x (2) x (0) ”⟩ \leftrightarrow x \sim_{𝒢} (G) ⟨“ x (1) x (2) x (0) ”⟩)$
15	12 14	rabeqbidv	$⊢ g = G \to \{x \in ({Base}_{g}^{(0 ..^3)}) \| x \sim_{𝒢} (g) ⟨“ x (1) x (2) x (0) ”⟩\} = \{x \in (P^{(0 ..^3)}) \| x \sim_{𝒢} (G) ⟨“ x (1) x (2) x (0) ”⟩\}$
16		df-eqlg	$⊢ {Equilaterals}_{𝒢} = (g \in V ⟼ \{x \in ({Base}_{g}^{(0 ..^3)}) \| x \sim_{𝒢} (g) ⟨“ x (1) x (2) x (0) ”⟩\})$
17		ovex	$⊢ P^{(0 ..^3)} \in V$
18	17	rabex	$⊢ \{x \in (P^{(0 ..^3)}) \| x \sim_{𝒢} (G) ⟨“ x (1) x (2) x (0) ”⟩\} \in V$
19	15 16 18	fvmpt	$⊢ G \in V \to {Equilaterals}_{𝒢} (G) = \{x \in (P^{(0 ..^3)}) \| x \sim_{𝒢} (G) ⟨“ x (1) x (2) x (0) ”⟩\}$
20	5 9 19	3syl	$⊢ φ \to {Equilaterals}_{𝒢} (G) = \{x \in (P^{(0 ..^3)}) \| x \sim_{𝒢} (G) ⟨“ x (1) x (2) x (0) ”⟩\}$
21	20	eleq2d	$⊢ φ \to (⟨“ A B C ”⟩ \in {Equilaterals}_{𝒢} (G) \leftrightarrow ⟨“ A B C ”⟩ \in \{x \in (P^{(0 ..^3)}) \| x \sim_{𝒢} (G) ⟨“ x (1) x (2) x (0) ”⟩\})$
22		id	$⊢ x = ⟨“ A B C ”⟩ \to x = ⟨“ A B C ”⟩$
23		fveq1	$⊢ x = ⟨“ A B C ”⟩ \to x (1) = ⟨“ A B C ”⟩ (1)$
24		fveq1	$⊢ x = ⟨“ A B C ”⟩ \to x (2) = ⟨“ A B C ”⟩ (2)$
25		fveq1	$⊢ x = ⟨“ A B C ”⟩ \to x (0) = ⟨“ A B C ”⟩ (0)$
26	23 24 25	s3eqd	$⊢ x = ⟨“ A B C ”⟩ \to ⟨“ x (1) x (2) x (0) ”⟩ = ⟨“ ⟨“ A B C ”⟩ (1) ⟨“ A B C ”⟩ (2) ⟨“ A B C ”⟩ (0) ”⟩$
27	22 26	breq12d	$⊢ x = ⟨“ A B C ”⟩ \to (x \sim_{𝒢} (G) ⟨“ x (1) x (2) x (0) ”⟩ \leftrightarrow ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ ⟨“ A B C ”⟩ (1) ⟨“ A B C ”⟩ (2) ⟨“ A B C ”⟩ (0) ”⟩)$
28	27	elrab	$⊢ ⟨“ A B C ”⟩ \in \{x \in (P^{(0 ..^3)}) \| x \sim_{𝒢} (G) ⟨“ x (1) x (2) x (0) ”⟩\} \leftrightarrow (⟨“ A B C ”⟩ \in (P^{(0 ..^3)}) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ ⟨“ A B C ”⟩ (1) ⟨“ A B C ”⟩ (2) ⟨“ A B C ”⟩ (0) ”⟩)$
29	28	a1i	$⊢ φ \to (⟨“ A B C ”⟩ \in \{x \in (P^{(0 ..^3)}) \| x \sim_{𝒢} (G) ⟨“ x (1) x (2) x (0) ”⟩\} \leftrightarrow (⟨“ A B C ”⟩ \in (P^{(0 ..^3)}) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ ⟨“ A B C ”⟩ (1) ⟨“ A B C ”⟩ (2) ⟨“ A B C ”⟩ (0) ”⟩))$
30	6 7 8	s3cld	$⊢ φ \to ⟨“ A B C ”⟩ \in Word P$
31		s3len	$⊢ \|⟨“ A B C ”⟩\| = 3$
32	1	fvexi	$⊢ P \in V$
33		3nn0	$⊢ 3 \in ℕ_{0}$
34		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)}))$
35	32 33 34	mp2an	$⊢ (⟨“ A B C ”⟩ \in Word P \land \|⟨“ A B C ”⟩\| = 3) \leftrightarrow ⟨“ A B C ”⟩ \in (P^{(0 ..^3)})$
36	30 31 35	sylanblc	$⊢ φ \to ⟨“ A B C ”⟩ \in (P^{(0 ..^3)})$
37	36	biantrurd	$⊢ φ \to (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ ⟨“ A B C ”⟩ (1) ⟨“ A B C ”⟩ (2) ⟨“ A B C ”⟩ (0) ”⟩ \leftrightarrow (⟨“ A B C ”⟩ \in (P^{(0 ..^3)}) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ ⟨“ A B C ”⟩ (1) ⟨“ A B C ”⟩ (2) ⟨“ A B C ”⟩ (0) ”⟩))$
38		s3fv1	$⊢ B \in P \to ⟨“ A B C ”⟩ (1) = B$
39	7 38	syl	$⊢ φ \to ⟨“ A B C ”⟩ (1) = B$
40		s3fv2	$⊢ C \in P \to ⟨“ A B C ”⟩ (2) = C$
41	8 40	syl	$⊢ φ \to ⟨“ A B C ”⟩ (2) = C$
42		s3fv0	$⊢ A \in P \to ⟨“ A B C ”⟩ (0) = A$
43	6 42	syl	$⊢ φ \to ⟨“ A B C ”⟩ (0) = A$
44	39 41 43	s3eqd	$⊢ φ \to ⟨“ ⟨“ A B C ”⟩ (1) ⟨“ A B C ”⟩ (2) ⟨“ A B C ”⟩ (0) ”⟩ = ⟨“ B C A ”⟩$
45	44	breq2d	$⊢ φ \to (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ ⟨“ A B C ”⟩ (1) ⟨“ A B C ”⟩ (2) ⟨“ A B C ”⟩ (0) ”⟩ \leftrightarrow ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ B C A ”⟩)$
46	37 45	bitr3d	$⊢ φ \to ((⟨“ A B C ”⟩ \in (P^{(0 ..^3)}) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ ⟨“ A B C ”⟩ (1) ⟨“ A B C ”⟩ (2) ⟨“ A B C ”⟩ (0) ”⟩) \leftrightarrow ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ B C A ”⟩)$
47	21 29 46	3bitrd	$⊢ φ \to (⟨“ A B C ”⟩ \in {Equilaterals}_{𝒢} (G) \leftrightarrow ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ B C A ”⟩)$

Metamath Proof Explorer

Theorem iseqlg

Proof