trgcgrg

Description: The property for two triangles to be congruent to each other. (Contributed by Thierry Arnoux, 3-Apr-2019)

	Ref	Expression
Hypotheses	trgcgrg.p	$⊢ P = {Base}_{G}$
	trgcgrg.m	$⊢ \underset{˙}{-} = dist (G)$
	trgcgrg.r	$⊢ \underset{˙}{\sim} = \sim_{𝒢} (G)$
	trgcgrg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	trgcgrg.a	$⊢ φ \to A \in P$
	trgcgrg.b	$⊢ φ \to B \in P$
	trgcgrg.c	$⊢ φ \to C \in P$
	trgcgrg.d	$⊢ φ \to D \in P$
	trgcgrg.e	$⊢ φ \to E \in P$
	trgcgrg.f	$⊢ φ \to F \in P$
Assertion	trgcgrg	$⊢ φ \to (⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D E F ”⟩ \leftrightarrow (A \underset{˙}{-} B = D \underset{˙}{-} E \land B \underset{˙}{-} C = E \underset{˙}{-} F \land C \underset{˙}{-} A = F \underset{˙}{-} D))$

Proof

Step	Hyp	Ref	Expression
1		trgcgrg.p	$⊢ P = {Base}_{G}$
2		trgcgrg.m	$⊢ \underset{˙}{-} = dist (G)$
3		trgcgrg.r	$⊢ \underset{˙}{\sim} = \sim_{𝒢} (G)$
4		trgcgrg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		trgcgrg.a	$⊢ φ \to A \in P$
6		trgcgrg.b	$⊢ φ \to B \in P$
7		trgcgrg.c	$⊢ φ \to C \in P$
8		trgcgrg.d	$⊢ φ \to D \in P$
9		trgcgrg.e	$⊢ φ \to E \in P$
10		trgcgrg.f	$⊢ φ \to F \in P$
11	5 6 7	s3cld	$⊢ φ \to ⟨“ A B C ”⟩ \in Word P$
12		wrdf	$⊢ ⟨“ A B C ”⟩ \in Word P \to ⟨“ A B C ”⟩ : (0 ..^\|⟨“ A B C ”⟩\|) ⟶ P$
13	11 12	syl	$⊢ φ \to ⟨“ A B C ”⟩ : (0 ..^\|⟨“ A B C ”⟩\|) ⟶ P$
14		s3len	$⊢ \|⟨“ A B C ”⟩\| = 3$
15	14	oveq2i	$⊢ (0 ..^\|⟨“ A B C ”⟩\|) = (0 ..^3)$
16		fzo0to3tp	$⊢ (0 ..^3) = \{0, 1, 2\}$
17	15 16	eqtri	$⊢ (0 ..^\|⟨“ A B C ”⟩\|) = \{0, 1, 2\}$
18	17	feq2i	$⊢ ⟨“ A B C ”⟩ : (0 ..^\|⟨“ A B C ”⟩\|) ⟶ P \leftrightarrow ⟨“ A B C ”⟩ : \{0, 1, 2\} ⟶ P$
19	13 18	sylib	$⊢ φ \to ⟨“ A B C ”⟩ : \{0, 1, 2\} ⟶ P$
20	19	fdmd	$⊢ φ \to dom ⟨“ A B C ”⟩ = \{0, 1, 2\}$
21	20	raleqdv	$⊢ φ \to (\forall j \in dom ⟨“ A B C ”⟩ ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ D E F ”⟩ (i) \underset{˙}{-} ⟨“ D E F ”⟩ (j) \leftrightarrow \forall j \in \{0, 1, 2\} ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ D E F ”⟩ (i) \underset{˙}{-} ⟨“ D E F ”⟩ (j))$
22	20 21	raleqbidv	$⊢ φ \to (\forall i \in dom ⟨“ A B C ”⟩ \forall j \in dom ⟨“ A B C ”⟩ ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ D E F ”⟩ (i) \underset{˙}{-} ⟨“ D E F ”⟩ (j) \leftrightarrow \forall i \in \{0, 1, 2\} \forall j \in \{0, 1, 2\} ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ D E F ”⟩ (i) \underset{˙}{-} ⟨“ D E F ”⟩ (j))$
23		0re	$⊢ 0 \in ℝ$
24		1re	$⊢ 1 \in ℝ$
25		2re	$⊢ 2 \in ℝ$
26		tpssi	$⊢ (0 \in ℝ \land 1 \in ℝ \land 2 \in ℝ) \to \{0, 1, 2\} \subseteq ℝ$
27	23 24 25 26	mp3an	$⊢ \{0, 1, 2\} \subseteq ℝ$
28	27	a1i	$⊢ φ \to \{0, 1, 2\} \subseteq ℝ$
29	8 9 10	s3cld	$⊢ φ \to ⟨“ D E F ”⟩ \in Word P$
30		wrdf	$⊢ ⟨“ D E F ”⟩ \in Word P \to ⟨“ D E F ”⟩ : (0 ..^\|⟨“ D E F ”⟩\|) ⟶ P$
31	29 30	syl	$⊢ φ \to ⟨“ D E F ”⟩ : (0 ..^\|⟨“ D E F ”⟩\|) ⟶ P$
32		s3len	$⊢ \|⟨“ D E F ”⟩\| = 3$
33	32	oveq2i	$⊢ (0 ..^\|⟨“ D E F ”⟩\|) = (0 ..^3)$
34	33 16	eqtri	$⊢ (0 ..^\|⟨“ D E F ”⟩\|) = \{0, 1, 2\}$
35	34	feq2i	$⊢ ⟨“ D E F ”⟩ : (0 ..^\|⟨“ D E F ”⟩\|) ⟶ P \leftrightarrow ⟨“ D E F ”⟩ : \{0, 1, 2\} ⟶ P$
36	31 35	sylib	$⊢ φ \to ⟨“ D E F ”⟩ : \{0, 1, 2\} ⟶ P$
37	1 2 3 4 28 19 36	iscgrgd	$⊢ φ \to (⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D E F ”⟩ \leftrightarrow \forall i \in dom ⟨“ A B C ”⟩ \forall j \in dom ⟨“ A B C ”⟩ ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ D E F ”⟩ (i) \underset{˙}{-} ⟨“ D E F ”⟩ (j))$
38		fveq2	$⊢ j = 0 \to ⟨“ A B C ”⟩ (j) = ⟨“ A B C ”⟩ (0)$
39		s3fv0	$⊢ A \in P \to ⟨“ A B C ”⟩ (0) = A$
40	5 39	syl	$⊢ φ \to ⟨“ A B C ”⟩ (0) = A$
41	38 40	sylan9eqr	$⊢ (φ \land j = 0) \to ⟨“ A B C ”⟩ (j) = A$
42	41	oveq2d	$⊢ (φ \land j = 0) \to ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ A B C ”⟩ (i) \underset{˙}{-} A$
43		fveq2	$⊢ j = 0 \to ⟨“ D E F ”⟩ (j) = ⟨“ D E F ”⟩ (0)$
44		s3fv0	$⊢ D \in P \to ⟨“ D E F ”⟩ (0) = D$
45	8 44	syl	$⊢ φ \to ⟨“ D E F ”⟩ (0) = D$
46	43 45	sylan9eqr	$⊢ (φ \land j = 0) \to ⟨“ D E F ”⟩ (j) = D$
47	46	oveq2d	$⊢ (φ \land j = 0) \to ⟨“ D E F ”⟩ (i) \underset{˙}{-} ⟨“ D E F ”⟩ (j) = ⟨“ D E F ”⟩ (i) \underset{˙}{-} D$
48	42 47	eqeq12d	$⊢ (φ \land j = 0) \to (⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ D E F ”⟩ (i) \underset{˙}{-} ⟨“ D E F ”⟩ (j) \leftrightarrow ⟨“ A B C ”⟩ (i) \underset{˙}{-} A = ⟨“ D E F ”⟩ (i) \underset{˙}{-} D)$
49		fveq2	$⊢ j = 1 \to ⟨“ A B C ”⟩ (j) = ⟨“ A B C ”⟩ (1)$
50		s3fv1	$⊢ B \in P \to ⟨“ A B C ”⟩ (1) = B$
51	6 50	syl	$⊢ φ \to ⟨“ A B C ”⟩ (1) = B$
52	49 51	sylan9eqr	$⊢ (φ \land j = 1) \to ⟨“ A B C ”⟩ (j) = B$
53	52	oveq2d	$⊢ (φ \land j = 1) \to ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ A B C ”⟩ (i) \underset{˙}{-} B$
54		fveq2	$⊢ j = 1 \to ⟨“ D E F ”⟩ (j) = ⟨“ D E F ”⟩ (1)$
55		s3fv1	$⊢ E \in P \to ⟨“ D E F ”⟩ (1) = E$
56	9 55	syl	$⊢ φ \to ⟨“ D E F ”⟩ (1) = E$
57	54 56	sylan9eqr	$⊢ (φ \land j = 1) \to ⟨“ D E F ”⟩ (j) = E$
58	57	oveq2d	$⊢ (φ \land j = 1) \to ⟨“ D E F ”⟩ (i) \underset{˙}{-} ⟨“ D E F ”⟩ (j) = ⟨“ D E F ”⟩ (i) \underset{˙}{-} E$
59	53 58	eqeq12d	$⊢ (φ \land j = 1) \to (⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ D E F ”⟩ (i) \underset{˙}{-} ⟨“ D E F ”⟩ (j) \leftrightarrow ⟨“ A B C ”⟩ (i) \underset{˙}{-} B = ⟨“ D E F ”⟩ (i) \underset{˙}{-} E)$
60		fveq2	$⊢ j = 2 \to ⟨“ A B C ”⟩ (j) = ⟨“ A B C ”⟩ (2)$
61		s3fv2	$⊢ C \in P \to ⟨“ A B C ”⟩ (2) = C$
62	7 61	syl	$⊢ φ \to ⟨“ A B C ”⟩ (2) = C$
63	60 62	sylan9eqr	$⊢ (φ \land j = 2) \to ⟨“ A B C ”⟩ (j) = C$
64	63	oveq2d	$⊢ (φ \land j = 2) \to ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ A B C ”⟩ (i) \underset{˙}{-} C$
65		fveq2	$⊢ j = 2 \to ⟨“ D E F ”⟩ (j) = ⟨“ D E F ”⟩ (2)$
66		s3fv2	$⊢ F \in P \to ⟨“ D E F ”⟩ (2) = F$
67	10 66	syl	$⊢ φ \to ⟨“ D E F ”⟩ (2) = F$
68	65 67	sylan9eqr	$⊢ (φ \land j = 2) \to ⟨“ D E F ”⟩ (j) = F$
69	68	oveq2d	$⊢ (φ \land j = 2) \to ⟨“ D E F ”⟩ (i) \underset{˙}{-} ⟨“ D E F ”⟩ (j) = ⟨“ D E F ”⟩ (i) \underset{˙}{-} F$
70	64 69	eqeq12d	$⊢ (φ \land j = 2) \to (⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ D E F ”⟩ (i) \underset{˙}{-} ⟨“ D E F ”⟩ (j) \leftrightarrow ⟨“ A B C ”⟩ (i) \underset{˙}{-} C = ⟨“ D E F ”⟩ (i) \underset{˙}{-} F)$
71		0red	$⊢ φ \to 0 \in ℝ$
72		1red	$⊢ φ \to 1 \in ℝ$
73	25	a1i	$⊢ φ \to 2 \in ℝ$
74	48 59 70 71 72 73	raltpd	$⊢ φ \to (\forall j \in \{0, 1, 2\} ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ D E F ”⟩ (i) \underset{˙}{-} ⟨“ D E F ”⟩ (j) \leftrightarrow (⟨“ A B C ”⟩ (i) \underset{˙}{-} A = ⟨“ D E F ”⟩ (i) \underset{˙}{-} D \land ⟨“ A B C ”⟩ (i) \underset{˙}{-} B = ⟨“ D E F ”⟩ (i) \underset{˙}{-} E \land ⟨“ A B C ”⟩ (i) \underset{˙}{-} C = ⟨“ D E F ”⟩ (i) \underset{˙}{-} F))$
75	74	adantr	$⊢ (φ \land i = 0) \to (\forall j \in \{0, 1, 2\} ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ D E F ”⟩ (i) \underset{˙}{-} ⟨“ D E F ”⟩ (j) \leftrightarrow (⟨“ A B C ”⟩ (i) \underset{˙}{-} A = ⟨“ D E F ”⟩ (i) \underset{˙}{-} D \land ⟨“ A B C ”⟩ (i) \underset{˙}{-} B = ⟨“ D E F ”⟩ (i) \underset{˙}{-} E \land ⟨“ A B C ”⟩ (i) \underset{˙}{-} C = ⟨“ D E F ”⟩ (i) \underset{˙}{-} F))$
76		fveq2	$⊢ i = 0 \to ⟨“ A B C ”⟩ (i) = ⟨“ A B C ”⟩ (0)$
77	76	adantl	$⊢ (φ \land i = 0) \to ⟨“ A B C ”⟩ (i) = ⟨“ A B C ”⟩ (0)$
78	40	adantr	$⊢ (φ \land i = 0) \to ⟨“ A B C ”⟩ (0) = A$
79	77 78	eqtr2d	$⊢ (φ \land i = 0) \to A = ⟨“ A B C ”⟩ (i)$
80	79	oveq1d	$⊢ (φ \land i = 0) \to A \underset{˙}{-} A = ⟨“ A B C ”⟩ (i) \underset{˙}{-} A$
81		fveq2	$⊢ i = 0 \to ⟨“ D E F ”⟩ (i) = ⟨“ D E F ”⟩ (0)$
82	81	adantl	$⊢ (φ \land i = 0) \to ⟨“ D E F ”⟩ (i) = ⟨“ D E F ”⟩ (0)$
83	45	adantr	$⊢ (φ \land i = 0) \to ⟨“ D E F ”⟩ (0) = D$
84	82 83	eqtr2d	$⊢ (φ \land i = 0) \to D = ⟨“ D E F ”⟩ (i)$
85	84	oveq1d	$⊢ (φ \land i = 0) \to D \underset{˙}{-} D = ⟨“ D E F ”⟩ (i) \underset{˙}{-} D$
86	80 85	eqeq12d	$⊢ (φ \land i = 0) \to (A \underset{˙}{-} A = D \underset{˙}{-} D \leftrightarrow ⟨“ A B C ”⟩ (i) \underset{˙}{-} A = ⟨“ D E F ”⟩ (i) \underset{˙}{-} D)$
87	79	oveq1d	$⊢ (φ \land i = 0) \to A \underset{˙}{-} B = ⟨“ A B C ”⟩ (i) \underset{˙}{-} B$
88	84	oveq1d	$⊢ (φ \land i = 0) \to D \underset{˙}{-} E = ⟨“ D E F ”⟩ (i) \underset{˙}{-} E$
89	87 88	eqeq12d	$⊢ (φ \land i = 0) \to (A \underset{˙}{-} B = D \underset{˙}{-} E \leftrightarrow ⟨“ A B C ”⟩ (i) \underset{˙}{-} B = ⟨“ D E F ”⟩ (i) \underset{˙}{-} E)$
90	79	oveq1d	$⊢ (φ \land i = 0) \to A \underset{˙}{-} C = ⟨“ A B C ”⟩ (i) \underset{˙}{-} C$
91	84	oveq1d	$⊢ (φ \land i = 0) \to D \underset{˙}{-} F = ⟨“ D E F ”⟩ (i) \underset{˙}{-} F$
92	90 91	eqeq12d	$⊢ (φ \land i = 0) \to (A \underset{˙}{-} C = D \underset{˙}{-} F \leftrightarrow ⟨“ A B C ”⟩ (i) \underset{˙}{-} C = ⟨“ D E F ”⟩ (i) \underset{˙}{-} F)$
93	86 89 92	3anbi123d	$⊢ (φ \land i = 0) \to ((A \underset{˙}{-} A = D \underset{˙}{-} D \land A \underset{˙}{-} B = D \underset{˙}{-} E \land A \underset{˙}{-} C = D \underset{˙}{-} F) \leftrightarrow (⟨“ A B C ”⟩ (i) \underset{˙}{-} A = ⟨“ D E F ”⟩ (i) \underset{˙}{-} D \land ⟨“ A B C ”⟩ (i) \underset{˙}{-} B = ⟨“ D E F ”⟩ (i) \underset{˙}{-} E \land ⟨“ A B C ”⟩ (i) \underset{˙}{-} C = ⟨“ D E F ”⟩ (i) \underset{˙}{-} F))$
94	75 93	bitr4d	$⊢ (φ \land i = 0) \to (\forall j \in \{0, 1, 2\} ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ D E F ”⟩ (i) \underset{˙}{-} ⟨“ D E F ”⟩ (j) \leftrightarrow (A \underset{˙}{-} A = D \underset{˙}{-} D \land A \underset{˙}{-} B = D \underset{˙}{-} E \land A \underset{˙}{-} C = D \underset{˙}{-} F))$
95	74	adantr	$⊢ (φ \land i = 1) \to (\forall j \in \{0, 1, 2\} ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ D E F ”⟩ (i) \underset{˙}{-} ⟨“ D E F ”⟩ (j) \leftrightarrow (⟨“ A B C ”⟩ (i) \underset{˙}{-} A = ⟨“ D E F ”⟩ (i) \underset{˙}{-} D \land ⟨“ A B C ”⟩ (i) \underset{˙}{-} B = ⟨“ D E F ”⟩ (i) \underset{˙}{-} E \land ⟨“ A B C ”⟩ (i) \underset{˙}{-} C = ⟨“ D E F ”⟩ (i) \underset{˙}{-} F))$
96		fveq2	$⊢ i = 1 \to ⟨“ A B C ”⟩ (i) = ⟨“ A B C ”⟩ (1)$
97	96	adantl	$⊢ (φ \land i = 1) \to ⟨“ A B C ”⟩ (i) = ⟨“ A B C ”⟩ (1)$
98	51	adantr	$⊢ (φ \land i = 1) \to ⟨“ A B C ”⟩ (1) = B$
99	97 98	eqtr2d	$⊢ (φ \land i = 1) \to B = ⟨“ A B C ”⟩ (i)$
100	99	oveq1d	$⊢ (φ \land i = 1) \to B \underset{˙}{-} A = ⟨“ A B C ”⟩ (i) \underset{˙}{-} A$
101		fveq2	$⊢ i = 1 \to ⟨“ D E F ”⟩ (i) = ⟨“ D E F ”⟩ (1)$
102	101	adantl	$⊢ (φ \land i = 1) \to ⟨“ D E F ”⟩ (i) = ⟨“ D E F ”⟩ (1)$
103	56	adantr	$⊢ (φ \land i = 1) \to ⟨“ D E F ”⟩ (1) = E$
104	102 103	eqtr2d	$⊢ (φ \land i = 1) \to E = ⟨“ D E F ”⟩ (i)$
105	104	oveq1d	$⊢ (φ \land i = 1) \to E \underset{˙}{-} D = ⟨“ D E F ”⟩ (i) \underset{˙}{-} D$
106	100 105	eqeq12d	$⊢ (φ \land i = 1) \to (B \underset{˙}{-} A = E \underset{˙}{-} D \leftrightarrow ⟨“ A B C ”⟩ (i) \underset{˙}{-} A = ⟨“ D E F ”⟩ (i) \underset{˙}{-} D)$
107	99	oveq1d	$⊢ (φ \land i = 1) \to B \underset{˙}{-} B = ⟨“ A B C ”⟩ (i) \underset{˙}{-} B$
108	104	oveq1d	$⊢ (φ \land i = 1) \to E \underset{˙}{-} E = ⟨“ D E F ”⟩ (i) \underset{˙}{-} E$
109	107 108	eqeq12d	$⊢ (φ \land i = 1) \to (B \underset{˙}{-} B = E \underset{˙}{-} E \leftrightarrow ⟨“ A B C ”⟩ (i) \underset{˙}{-} B = ⟨“ D E F ”⟩ (i) \underset{˙}{-} E)$
110	99	oveq1d	$⊢ (φ \land i = 1) \to B \underset{˙}{-} C = ⟨“ A B C ”⟩ (i) \underset{˙}{-} C$
111	104	oveq1d	$⊢ (φ \land i = 1) \to E \underset{˙}{-} F = ⟨“ D E F ”⟩ (i) \underset{˙}{-} F$
112	110 111	eqeq12d	$⊢ (φ \land i = 1) \to (B \underset{˙}{-} C = E \underset{˙}{-} F \leftrightarrow ⟨“ A B C ”⟩ (i) \underset{˙}{-} C = ⟨“ D E F ”⟩ (i) \underset{˙}{-} F)$
113	106 109 112	3anbi123d	$⊢ (φ \land i = 1) \to ((B \underset{˙}{-} A = E \underset{˙}{-} D \land B \underset{˙}{-} B = E \underset{˙}{-} E \land B \underset{˙}{-} C = E \underset{˙}{-} F) \leftrightarrow (⟨“ A B C ”⟩ (i) \underset{˙}{-} A = ⟨“ D E F ”⟩ (i) \underset{˙}{-} D \land ⟨“ A B C ”⟩ (i) \underset{˙}{-} B = ⟨“ D E F ”⟩ (i) \underset{˙}{-} E \land ⟨“ A B C ”⟩ (i) \underset{˙}{-} C = ⟨“ D E F ”⟩ (i) \underset{˙}{-} F))$
114	95 113	bitr4d	$⊢ (φ \land i = 1) \to (\forall j \in \{0, 1, 2\} ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ D E F ”⟩ (i) \underset{˙}{-} ⟨“ D E F ”⟩ (j) \leftrightarrow (B \underset{˙}{-} A = E \underset{˙}{-} D \land B \underset{˙}{-} B = E \underset{˙}{-} E \land B \underset{˙}{-} C = E \underset{˙}{-} F))$
115	74	adantr	$⊢ (φ \land i = 2) \to (\forall j \in \{0, 1, 2\} ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ D E F ”⟩ (i) \underset{˙}{-} ⟨“ D E F ”⟩ (j) \leftrightarrow (⟨“ A B C ”⟩ (i) \underset{˙}{-} A = ⟨“ D E F ”⟩ (i) \underset{˙}{-} D \land ⟨“ A B C ”⟩ (i) \underset{˙}{-} B = ⟨“ D E F ”⟩ (i) \underset{˙}{-} E \land ⟨“ A B C ”⟩ (i) \underset{˙}{-} C = ⟨“ D E F ”⟩ (i) \underset{˙}{-} F))$
116		fveq2	$⊢ i = 2 \to ⟨“ A B C ”⟩ (i) = ⟨“ A B C ”⟩ (2)$
117	116	adantl	$⊢ (φ \land i = 2) \to ⟨“ A B C ”⟩ (i) = ⟨“ A B C ”⟩ (2)$
118	62	adantr	$⊢ (φ \land i = 2) \to ⟨“ A B C ”⟩ (2) = C$
119	117 118	eqtr2d	$⊢ (φ \land i = 2) \to C = ⟨“ A B C ”⟩ (i)$
120	119	oveq1d	$⊢ (φ \land i = 2) \to C \underset{˙}{-} A = ⟨“ A B C ”⟩ (i) \underset{˙}{-} A$
121		fveq2	$⊢ i = 2 \to ⟨“ D E F ”⟩ (i) = ⟨“ D E F ”⟩ (2)$
122	121	adantl	$⊢ (φ \land i = 2) \to ⟨“ D E F ”⟩ (i) = ⟨“ D E F ”⟩ (2)$
123	67	adantr	$⊢ (φ \land i = 2) \to ⟨“ D E F ”⟩ (2) = F$
124	122 123	eqtr2d	$⊢ (φ \land i = 2) \to F = ⟨“ D E F ”⟩ (i)$
125	124	oveq1d	$⊢ (φ \land i = 2) \to F \underset{˙}{-} D = ⟨“ D E F ”⟩ (i) \underset{˙}{-} D$
126	120 125	eqeq12d	$⊢ (φ \land i = 2) \to (C \underset{˙}{-} A = F \underset{˙}{-} D \leftrightarrow ⟨“ A B C ”⟩ (i) \underset{˙}{-} A = ⟨“ D E F ”⟩ (i) \underset{˙}{-} D)$
127	119	oveq1d	$⊢ (φ \land i = 2) \to C \underset{˙}{-} B = ⟨“ A B C ”⟩ (i) \underset{˙}{-} B$
128	124	oveq1d	$⊢ (φ \land i = 2) \to F \underset{˙}{-} E = ⟨“ D E F ”⟩ (i) \underset{˙}{-} E$
129	127 128	eqeq12d	$⊢ (φ \land i = 2) \to (C \underset{˙}{-} B = F \underset{˙}{-} E \leftrightarrow ⟨“ A B C ”⟩ (i) \underset{˙}{-} B = ⟨“ D E F ”⟩ (i) \underset{˙}{-} E)$
130	119	oveq1d	$⊢ (φ \land i = 2) \to C \underset{˙}{-} C = ⟨“ A B C ”⟩ (i) \underset{˙}{-} C$
131	124	oveq1d	$⊢ (φ \land i = 2) \to F \underset{˙}{-} F = ⟨“ D E F ”⟩ (i) \underset{˙}{-} F$
132	130 131	eqeq12d	$⊢ (φ \land i = 2) \to (C \underset{˙}{-} C = F \underset{˙}{-} F \leftrightarrow ⟨“ A B C ”⟩ (i) \underset{˙}{-} C = ⟨“ D E F ”⟩ (i) \underset{˙}{-} F)$
133	126 129 132	3anbi123d	$⊢ (φ \land i = 2) \to ((C \underset{˙}{-} A = F \underset{˙}{-} D \land C \underset{˙}{-} B = F \underset{˙}{-} E \land C \underset{˙}{-} C = F \underset{˙}{-} F) \leftrightarrow (⟨“ A B C ”⟩ (i) \underset{˙}{-} A = ⟨“ D E F ”⟩ (i) \underset{˙}{-} D \land ⟨“ A B C ”⟩ (i) \underset{˙}{-} B = ⟨“ D E F ”⟩ (i) \underset{˙}{-} E \land ⟨“ A B C ”⟩ (i) \underset{˙}{-} C = ⟨“ D E F ”⟩ (i) \underset{˙}{-} F))$
134	115 133	bitr4d	$⊢ (φ \land i = 2) \to (\forall j \in \{0, 1, 2\} ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ D E F ”⟩ (i) \underset{˙}{-} ⟨“ D E F ”⟩ (j) \leftrightarrow (C \underset{˙}{-} A = F \underset{˙}{-} D \land C \underset{˙}{-} B = F \underset{˙}{-} E \land C \underset{˙}{-} C = F \underset{˙}{-} F))$
135	94 114 134 71 72 73	raltpd	$⊢ φ \to (\forall i \in \{0, 1, 2\} \forall j \in \{0, 1, 2\} ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ D E F ”⟩ (i) \underset{˙}{-} ⟨“ D E F ”⟩ (j) \leftrightarrow ((A \underset{˙}{-} A = D \underset{˙}{-} D \land A \underset{˙}{-} B = D \underset{˙}{-} E \land A \underset{˙}{-} C = D \underset{˙}{-} F) \land (B \underset{˙}{-} A = E \underset{˙}{-} D \land B \underset{˙}{-} B = E \underset{˙}{-} E \land B \underset{˙}{-} C = E \underset{˙}{-} F) \land (C \underset{˙}{-} A = F \underset{˙}{-} D \land C \underset{˙}{-} B = F \underset{˙}{-} E \land C \underset{˙}{-} C = F \underset{˙}{-} F)))$
136		an33rean	$⊢ ((A \underset{˙}{-} A = D \underset{˙}{-} D \land A \underset{˙}{-} B = D \underset{˙}{-} E \land A \underset{˙}{-} C = D \underset{˙}{-} F) \land (B \underset{˙}{-} A = E \underset{˙}{-} D \land B \underset{˙}{-} B = E \underset{˙}{-} E \land B \underset{˙}{-} C = E \underset{˙}{-} F) \land (C \underset{˙}{-} A = F \underset{˙}{-} D \land C \underset{˙}{-} B = F \underset{˙}{-} E \land C \underset{˙}{-} C = F \underset{˙}{-} F)) \leftrightarrow ((A \underset{˙}{-} A = D \underset{˙}{-} D \land B \underset{˙}{-} B = E \underset{˙}{-} E \land C \underset{˙}{-} C = F \underset{˙}{-} F) \land ((A \underset{˙}{-} B = D \underset{˙}{-} E \land B \underset{˙}{-} A = E \underset{˙}{-} D) \land (B \underset{˙}{-} C = E \underset{˙}{-} F \land C \underset{˙}{-} B = F \underset{˙}{-} E) \land (A \underset{˙}{-} C = D \underset{˙}{-} F \land C \underset{˙}{-} A = F \underset{˙}{-} D)))$
137		eqid	$⊢ Itv (G) = Itv (G)$
138	1 2 137 4 5 8	tgcgrtriv	$⊢ φ \to A \underset{˙}{-} A = D \underset{˙}{-} D$
139	1 2 137 4 6 9	tgcgrtriv	$⊢ φ \to B \underset{˙}{-} B = E \underset{˙}{-} E$
140	1 2 137 4 7 10	tgcgrtriv	$⊢ φ \to C \underset{˙}{-} C = F \underset{˙}{-} F$
141	138 139 140	3jca	$⊢ φ \to (A \underset{˙}{-} A = D \underset{˙}{-} D \land B \underset{˙}{-} B = E \underset{˙}{-} E \land C \underset{˙}{-} C = F \underset{˙}{-} F)$
142	141	biantrurd	$⊢ φ \to (((A \underset{˙}{-} B = D \underset{˙}{-} E \land B \underset{˙}{-} A = E \underset{˙}{-} D) \land (B \underset{˙}{-} C = E \underset{˙}{-} F \land C \underset{˙}{-} B = F \underset{˙}{-} E) \land (A \underset{˙}{-} C = D \underset{˙}{-} F \land C \underset{˙}{-} A = F \underset{˙}{-} D)) \leftrightarrow ((A \underset{˙}{-} A = D \underset{˙}{-} D \land B \underset{˙}{-} B = E \underset{˙}{-} E \land C \underset{˙}{-} C = F \underset{˙}{-} F) \land ((A \underset{˙}{-} B = D \underset{˙}{-} E \land B \underset{˙}{-} A = E \underset{˙}{-} D) \land (B \underset{˙}{-} C = E \underset{˙}{-} F \land C \underset{˙}{-} B = F \underset{˙}{-} E) \land (A \underset{˙}{-} C = D \underset{˙}{-} F \land C \underset{˙}{-} A = F \underset{˙}{-} D))))$
143		simprl	$⊢ (φ \land (A \underset{˙}{-} B = D \underset{˙}{-} E \land B \underset{˙}{-} A = E \underset{˙}{-} D)) \to A \underset{˙}{-} B = D \underset{˙}{-} E$
144		simpr	$⊢ (φ \land A \underset{˙}{-} B = D \underset{˙}{-} E) \to A \underset{˙}{-} B = D \underset{˙}{-} E$
145	4	adantr	$⊢ (φ \land A \underset{˙}{-} B = D \underset{˙}{-} E) \to G \in 𝒢_{Tarski}$
146	5	adantr	$⊢ (φ \land A \underset{˙}{-} B = D \underset{˙}{-} E) \to A \in P$
147	6	adantr	$⊢ (φ \land A \underset{˙}{-} B = D \underset{˙}{-} E) \to B \in P$
148	8	adantr	$⊢ (φ \land A \underset{˙}{-} B = D \underset{˙}{-} E) \to D \in P$
149	9	adantr	$⊢ (φ \land A \underset{˙}{-} B = D \underset{˙}{-} E) \to E \in P$
150	1 2 137 145 146 147 148 149 144	tgcgrcomlr	$⊢ (φ \land A \underset{˙}{-} B = D \underset{˙}{-} E) \to B \underset{˙}{-} A = E \underset{˙}{-} D$
151	144 150	jca	$⊢ (φ \land A \underset{˙}{-} B = D \underset{˙}{-} E) \to (A \underset{˙}{-} B = D \underset{˙}{-} E \land B \underset{˙}{-} A = E \underset{˙}{-} D)$
152	143 151	impbida	$⊢ φ \to ((A \underset{˙}{-} B = D \underset{˙}{-} E \land B \underset{˙}{-} A = E \underset{˙}{-} D) \leftrightarrow A \underset{˙}{-} B = D \underset{˙}{-} E)$
153		simprl	$⊢ (φ \land (B \underset{˙}{-} C = E \underset{˙}{-} F \land C \underset{˙}{-} B = F \underset{˙}{-} E)) \to B \underset{˙}{-} C = E \underset{˙}{-} F$
154		simpr	$⊢ (φ \land B \underset{˙}{-} C = E \underset{˙}{-} F) \to B \underset{˙}{-} C = E \underset{˙}{-} F$
155	4	adantr	$⊢ (φ \land B \underset{˙}{-} C = E \underset{˙}{-} F) \to G \in 𝒢_{Tarski}$
156	6	adantr	$⊢ (φ \land B \underset{˙}{-} C = E \underset{˙}{-} F) \to B \in P$
157	7	adantr	$⊢ (φ \land B \underset{˙}{-} C = E \underset{˙}{-} F) \to C \in P$
158	9	adantr	$⊢ (φ \land B \underset{˙}{-} C = E \underset{˙}{-} F) \to E \in P$
159	10	adantr	$⊢ (φ \land B \underset{˙}{-} C = E \underset{˙}{-} F) \to F \in P$
160	1 2 137 155 156 157 158 159 154	tgcgrcomlr	$⊢ (φ \land B \underset{˙}{-} C = E \underset{˙}{-} F) \to C \underset{˙}{-} B = F \underset{˙}{-} E$
161	154 160	jca	$⊢ (φ \land B \underset{˙}{-} C = E \underset{˙}{-} F) \to (B \underset{˙}{-} C = E \underset{˙}{-} F \land C \underset{˙}{-} B = F \underset{˙}{-} E)$
162	153 161	impbida	$⊢ φ \to ((B \underset{˙}{-} C = E \underset{˙}{-} F \land C \underset{˙}{-} B = F \underset{˙}{-} E) \leftrightarrow B \underset{˙}{-} C = E \underset{˙}{-} F)$
163		simprr	$⊢ (φ \land (A \underset{˙}{-} C = D \underset{˙}{-} F \land C \underset{˙}{-} A = F \underset{˙}{-} D)) \to C \underset{˙}{-} A = F \underset{˙}{-} D$
164	4	adantr	$⊢ (φ \land C \underset{˙}{-} A = F \underset{˙}{-} D) \to G \in 𝒢_{Tarski}$
165	7	adantr	$⊢ (φ \land C \underset{˙}{-} A = F \underset{˙}{-} D) \to C \in P$
166	5	adantr	$⊢ (φ \land C \underset{˙}{-} A = F \underset{˙}{-} D) \to A \in P$
167	10	adantr	$⊢ (φ \land C \underset{˙}{-} A = F \underset{˙}{-} D) \to F \in P$
168	8	adantr	$⊢ (φ \land C \underset{˙}{-} A = F \underset{˙}{-} D) \to D \in P$
169		simpr	$⊢ (φ \land C \underset{˙}{-} A = F \underset{˙}{-} D) \to C \underset{˙}{-} A = F \underset{˙}{-} D$
170	1 2 137 164 165 166 167 168 169	tgcgrcomlr	$⊢ (φ \land C \underset{˙}{-} A = F \underset{˙}{-} D) \to A \underset{˙}{-} C = D \underset{˙}{-} F$
171	170 169	jca	$⊢ (φ \land C \underset{˙}{-} A = F \underset{˙}{-} D) \to (A \underset{˙}{-} C = D \underset{˙}{-} F \land C \underset{˙}{-} A = F \underset{˙}{-} D)$
172	163 171	impbida	$⊢ φ \to ((A \underset{˙}{-} C = D \underset{˙}{-} F \land C \underset{˙}{-} A = F \underset{˙}{-} D) \leftrightarrow C \underset{˙}{-} A = F \underset{˙}{-} D)$
173	152 162 172	3anbi123d	$⊢ φ \to (((A \underset{˙}{-} B = D \underset{˙}{-} E \land B \underset{˙}{-} A = E \underset{˙}{-} D) \land (B \underset{˙}{-} C = E \underset{˙}{-} F \land C \underset{˙}{-} B = F \underset{˙}{-} E) \land (A \underset{˙}{-} C = D \underset{˙}{-} F \land C \underset{˙}{-} A = F \underset{˙}{-} D)) \leftrightarrow (A \underset{˙}{-} B = D \underset{˙}{-} E \land B \underset{˙}{-} C = E \underset{˙}{-} F \land C \underset{˙}{-} A = F \underset{˙}{-} D))$
174	142 173	bitr3d	$⊢ φ \to (((A \underset{˙}{-} A = D \underset{˙}{-} D \land B \underset{˙}{-} B = E \underset{˙}{-} E \land C \underset{˙}{-} C = F \underset{˙}{-} F) \land ((A \underset{˙}{-} B = D \underset{˙}{-} E \land B \underset{˙}{-} A = E \underset{˙}{-} D) \land (B \underset{˙}{-} C = E \underset{˙}{-} F \land C \underset{˙}{-} B = F \underset{˙}{-} E) \land (A \underset{˙}{-} C = D \underset{˙}{-} F \land C \underset{˙}{-} A = F \underset{˙}{-} D))) \leftrightarrow (A \underset{˙}{-} B = D \underset{˙}{-} E \land B \underset{˙}{-} C = E \underset{˙}{-} F \land C \underset{˙}{-} A = F \underset{˙}{-} D))$
175	136 174	syl5bb	$⊢ φ \to (((A \underset{˙}{-} A = D \underset{˙}{-} D \land A \underset{˙}{-} B = D \underset{˙}{-} E \land A \underset{˙}{-} C = D \underset{˙}{-} F) \land (B \underset{˙}{-} A = E \underset{˙}{-} D \land B \underset{˙}{-} B = E \underset{˙}{-} E \land B \underset{˙}{-} C = E \underset{˙}{-} F) \land (C \underset{˙}{-} A = F \underset{˙}{-} D \land C \underset{˙}{-} B = F \underset{˙}{-} E \land C \underset{˙}{-} C = F \underset{˙}{-} F)) \leftrightarrow (A \underset{˙}{-} B = D \underset{˙}{-} E \land B \underset{˙}{-} C = E \underset{˙}{-} F \land C \underset{˙}{-} A = F \underset{˙}{-} D))$
176	135 175	bitr2d	$⊢ φ \to ((A \underset{˙}{-} B = D \underset{˙}{-} E \land B \underset{˙}{-} C = E \underset{˙}{-} F \land C \underset{˙}{-} A = F \underset{˙}{-} D) \leftrightarrow \forall i \in \{0, 1, 2\} \forall j \in \{0, 1, 2\} ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ D E F ”⟩ (i) \underset{˙}{-} ⟨“ D E F ”⟩ (j))$
177	22 37 176	3bitr4d	$⊢ φ \to (⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D E F ”⟩ \leftrightarrow (A \underset{˙}{-} B = D \underset{˙}{-} E \land B \underset{˙}{-} C = E \underset{˙}{-} F \land C \underset{˙}{-} A = F \underset{˙}{-} D))$

Metamath Proof Explorer

Theorem trgcgrg

Proof