tgcgr4

Description: Two quadrilaterals to be congruent to each other if one triangle formed by their vertices is, and the additional points are equidistant too. (Contributed by Thierry Arnoux, 8-Oct-2020)

	Ref	Expression
Hypotheses	tgcgrxfr.p	$⊢ P = {Base}_{G}$
	tgcgrxfr.m	$⊢ \underset{˙}{-} = dist (G)$
	tgcgrxfr.i	$⊢ I = Itv (G)$
	tgcgrxfr.r	$⊢ \underset{˙}{\sim} = \sim_{𝒢} (G)$
	tgcgrxfr.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tgcgr4.a	$⊢ φ \to A \in P$
	tgcgr4.b	$⊢ φ \to B \in P$
	tgcgr4.c	$⊢ φ \to C \in P$
	tgcgr4.d	$⊢ φ \to D \in P$
	tgcgr4.w	$⊢ φ \to W \in P$
	tgcgr4.x	$⊢ φ \to X \in P$
	tgcgr4.y	$⊢ φ \to Y \in P$
	tgcgr4.z	$⊢ φ \to Z \in P$
Assertion	tgcgr4	$⊢ φ \to (⟨“ A B C D ”⟩ \underset{˙}{\sim} ⟨“ W X Y Z ”⟩ \leftrightarrow (⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ W X Y ”⟩ \land (A \underset{˙}{-} D = W \underset{˙}{-} Z \land B \underset{˙}{-} D = X \underset{˙}{-} Z \land C \underset{˙}{-} D = Y \underset{˙}{-} Z)))$

Proof

Step	Hyp	Ref	Expression
1		tgcgrxfr.p	$⊢ P = {Base}_{G}$
2		tgcgrxfr.m	$⊢ \underset{˙}{-} = dist (G)$
3		tgcgrxfr.i	$⊢ I = Itv (G)$
4		tgcgrxfr.r	$⊢ \underset{˙}{\sim} = \sim_{𝒢} (G)$
5		tgcgrxfr.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		tgcgr4.a	$⊢ φ \to A \in P$
7		tgcgr4.b	$⊢ φ \to B \in P$
8		tgcgr4.c	$⊢ φ \to C \in P$
9		tgcgr4.d	$⊢ φ \to D \in P$
10		tgcgr4.w	$⊢ φ \to W \in P$
11		tgcgr4.x	$⊢ φ \to X \in P$
12		tgcgr4.y	$⊢ φ \to Y \in P$
13		tgcgr4.z	$⊢ φ \to Z \in P$
14		fzo0ssnn0	$⊢ (0 ..^4) \subseteq ℕ_{0}$
15		nn0ssre	$⊢ ℕ_{0} \subseteq ℝ$
16	14 15	sstri	$⊢ (0 ..^4) \subseteq ℝ$
17	16	a1i	$⊢ φ \to (0 ..^4) \subseteq ℝ$
18	6 7 8 9	s4cld	$⊢ φ \to ⟨“ A B C D ”⟩ \in Word P$
19		wrdf	$⊢ ⟨“ A B C D ”⟩ \in Word P \to ⟨“ A B C D ”⟩ : (0 ..^\|⟨“ A B C D ”⟩\|) ⟶ P$
20	18 19	syl	$⊢ φ \to ⟨“ A B C D ”⟩ : (0 ..^\|⟨“ A B C D ”⟩\|) ⟶ P$
21		s4len	$⊢ \|⟨“ A B C D ”⟩\| = 4$
22	21	oveq2i	$⊢ (0 ..^\|⟨“ A B C D ”⟩\|) = (0 ..^4)$
23	22	feq2i	$⊢ ⟨“ A B C D ”⟩ : (0 ..^\|⟨“ A B C D ”⟩\|) ⟶ P \leftrightarrow ⟨“ A B C D ”⟩ : (0 ..^4) ⟶ P$
24	20 23	sylib	$⊢ φ \to ⟨“ A B C D ”⟩ : (0 ..^4) ⟶ P$
25	10 11 12 13	s4cld	$⊢ φ \to ⟨“ W X Y Z ”⟩ \in Word P$
26		wrdf	$⊢ ⟨“ W X Y Z ”⟩ \in Word P \to ⟨“ W X Y Z ”⟩ : (0 ..^\|⟨“ W X Y Z ”⟩\|) ⟶ P$
27	25 26	syl	$⊢ φ \to ⟨“ W X Y Z ”⟩ : (0 ..^\|⟨“ W X Y Z ”⟩\|) ⟶ P$
28		s4len	$⊢ \|⟨“ W X Y Z ”⟩\| = 4$
29	28	oveq2i	$⊢ (0 ..^\|⟨“ W X Y Z ”⟩\|) = (0 ..^4)$
30	29	feq2i	$⊢ ⟨“ W X Y Z ”⟩ : (0 ..^\|⟨“ W X Y Z ”⟩\|) ⟶ P \leftrightarrow ⟨“ W X Y Z ”⟩ : (0 ..^4) ⟶ P$
31	27 30	sylib	$⊢ φ \to ⟨“ W X Y Z ”⟩ : (0 ..^4) ⟶ P$
32	1 2 4 5 17 24 31	iscgrglt	$⊢ φ \to (⟨“ A B C D ”⟩ \underset{˙}{\sim} ⟨“ W X Y Z ”⟩ \leftrightarrow \forall i \in dom ⟨“ A B C D ”⟩ \forall j \in dom ⟨“ A B C D ”⟩ (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)))$
33	24	fdmd	$⊢ φ \to dom ⟨“ A B C D ”⟩ = (0 ..^4)$
34		3p1e4	$⊢ 3 + 1 = 4$
35	34	oveq2i	$⊢ (0 ..^3 + 1) = (0 ..^4)$
36		3nn0	$⊢ 3 \in ℕ_{0}$
37		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
38	36 37	eleqtri	$⊢ 3 \in ℤ_{\geq 0}$
39		fzosplitsn	$⊢ 3 \in ℤ_{\geq 0} \to (0 ..^3 + 1) = (0 ..^3) \cup \{3\}$
40	38 39	ax-mp	$⊢ (0 ..^3 + 1) = (0 ..^3) \cup \{3\}$
41	35 40	eqtr3i	$⊢ (0 ..^4) = (0 ..^3) \cup \{3\}$
42	33 41	eqtrdi	$⊢ φ \to dom ⟨“ A B C D ”⟩ = (0 ..^3) \cup \{3\}$
43	42	raleqdv	$⊢ φ \to (\forall j \in dom ⟨“ A B C D ”⟩ (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \leftrightarrow \forall j \in ((0 ..^3) \cup \{3\}) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)))$
44		breq2	$⊢ j = 3 \to (i < j \leftrightarrow i < 3)$
45		fveq2	$⊢ j = 3 \to ⟨“ A B C D ”⟩ (j) = ⟨“ A B C D ”⟩ (3)$
46	45	oveq2d	$⊢ j = 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3)$
47		fveq2	$⊢ j = 3 \to ⟨“ W X Y Z ”⟩ (j) = ⟨“ W X Y Z ”⟩ (3)$
48	47	oveq2d	$⊢ j = 3 \to ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3)$
49	46 48	eqeq12d	$⊢ j = 3 \to (⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j) \leftrightarrow ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3))$
50	44 49	imbi12d	$⊢ j = 3 \to ((i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \leftrightarrow (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3)))$
51	50	ralunsn	$⊢ 3 \in ℕ_{0} \to (\forall j \in ((0 ..^3) \cup \{3\}) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \leftrightarrow (\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3))))$
52	36 51	ax-mp	$⊢ \forall j \in ((0 ..^3) \cup \{3\}) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \leftrightarrow (\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3)))$
53	43 52	bitrdi	$⊢ φ \to (\forall j \in dom ⟨“ A B C D ”⟩ (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \leftrightarrow (\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3))))$
54	53	ralbidv	$⊢ φ \to (\forall i \in dom ⟨“ A B C D ”⟩ \forall j \in dom ⟨“ A B C D ”⟩ (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \leftrightarrow \forall i \in dom ⟨“ A B C D ”⟩ (\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3))))$
55	42	raleqdv	$⊢ φ \to (\forall i \in dom ⟨“ A B C D ”⟩ (\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3))) \leftrightarrow \forall i \in ((0 ..^3) \cup \{3\}) (\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3))))$
56		fzo0ssnn0	$⊢ (0 ..^3) \subseteq ℕ_{0}$
57	56 15	sstri	$⊢ (0 ..^3) \subseteq ℝ$
58		simpr	$⊢ (i = 3 \land j \in (0 ..^3)) \to j \in (0 ..^3)$
59	57 58	sselid	$⊢ (i = 3 \land j \in (0 ..^3)) \to j \in ℝ$
60		simpl	$⊢ (i = 3 \land j \in (0 ..^3)) \to i = 3$
61		3re	$⊢ 3 \in ℝ$
62	60 61	eqeltrdi	$⊢ (i = 3 \land j \in (0 ..^3)) \to i \in ℝ$
63		elfzolt2	$⊢ j \in (0 ..^3) \to j < 3$
64	63	adantl	$⊢ (i = 3 \land j \in (0 ..^3)) \to j < 3$
65	64 60	breqtrrd	$⊢ (i = 3 \land j \in (0 ..^3)) \to j < i$
66	59 62 65	ltnsymd	$⊢ (i = 3 \land j \in (0 ..^3)) \to \neg i < j$
67	66	pm2.21d	$⊢ (i = 3 \land j \in (0 ..^3)) \to (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j))$
68		tbtru	$⊢ (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \leftrightarrow ((i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \leftrightarrow ⊤)$
69	67 68	sylib	$⊢ (i = 3 \land j \in (0 ..^3)) \to ((i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \leftrightarrow ⊤)$
70	69	ralbidva	$⊢ i = 3 \to (\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \leftrightarrow \forall j \in (0 ..^3) ⊤)$
71		3nn	$⊢ 3 \in ℕ$
72		lbfzo0	$⊢ 0 \in (0 ..^3) \leftrightarrow 3 \in ℕ$
73	71 72	mpbir	$⊢ 0 \in (0 ..^3)$
74	73	ne0ii	$⊢ (0 ..^3) \neq \emptyset$
75		r19.3rzv	$⊢ (0 ..^3) \neq \emptyset \to (⊤ \leftrightarrow \forall j \in (0 ..^3) ⊤)$
76	74 75	ax-mp	$⊢ ⊤ \leftrightarrow \forall j \in (0 ..^3) ⊤$
77	70 76	bitr4di	$⊢ i = 3 \to (\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \leftrightarrow ⊤)$
78		breq1	$⊢ i = 3 \to (i < 3 \leftrightarrow 3 < 3)$
79	61	ltnri	$⊢ \neg 3 < 3$
80	79	bifal	$⊢ 3 < 3 \leftrightarrow ⊥$
81	78 80	bitrdi	$⊢ i = 3 \to (i < 3 \leftrightarrow ⊥)$
82	81	imbi1d	$⊢ i = 3 \to ((i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3)) \leftrightarrow (⊥ \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3)))$
83		falim	$⊢ ⊥ \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3)$
84	83	bitru	$⊢ (⊥ \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3)) \leftrightarrow ⊤$
85	82 84	bitrdi	$⊢ i = 3 \to ((i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3)) \leftrightarrow ⊤)$
86	77 85	anbi12d	$⊢ i = 3 \to ((\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3))) \leftrightarrow (⊤ \land ⊤))$
87		anidm	$⊢ (⊤ \land ⊤) \leftrightarrow ⊤$
88	86 87	bitrdi	$⊢ i = 3 \to ((\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3))) \leftrightarrow ⊤)$
89	88	ralunsn	$⊢ 3 \in ℕ_{0} \to (\forall i \in ((0 ..^3) \cup \{3\}) (\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3))) \leftrightarrow (\forall i \in (0 ..^3) (\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3))) \land ⊤))$
90	36 89	ax-mp	$⊢ \forall i \in ((0 ..^3) \cup \{3\}) (\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3))) \leftrightarrow (\forall i \in (0 ..^3) (\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3))) \land ⊤)$
91		ancom	$⊢ (\forall i \in (0 ..^3) (\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3))) \land ⊤) \leftrightarrow (⊤ \land \forall i \in (0 ..^3) (\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3))))$
92		truan	$⊢ (⊤ \land \forall i \in (0 ..^3) (\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3)))) \leftrightarrow \forall i \in (0 ..^3) (\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3)))$
93	90 91 92	3bitri	$⊢ \forall i \in ((0 ..^3) \cup \{3\}) (\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3))) \leftrightarrow \forall i \in (0 ..^3) (\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3)))$
94	55 93	bitrdi	$⊢ φ \to (\forall i \in dom ⟨“ A B C D ”⟩ (\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3))) \leftrightarrow \forall i \in (0 ..^3) (\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3))))$
95	54 94	bitrd	$⊢ φ \to (\forall i \in dom ⟨“ A B C D ”⟩ \forall j \in dom ⟨“ A B C D ”⟩ (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \leftrightarrow \forall i \in (0 ..^3) (\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3))))$
96		r19.26	$⊢ \forall i \in (0 ..^3) (\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3))) \leftrightarrow (\forall i \in (0 ..^3) \forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land \forall i \in (0 ..^3) (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3)))$
97	6 7 8	s3cld	$⊢ φ \to ⟨“ A B C ”⟩ \in Word P$
98		wrdf	$⊢ ⟨“ A B C ”⟩ \in Word P \to ⟨“ A B C ”⟩ : (0 ..^\|⟨“ A B C ”⟩\|) ⟶ P$
99	97 98	syl	$⊢ φ \to ⟨“ A B C ”⟩ : (0 ..^\|⟨“ A B C ”⟩\|) ⟶ P$
100		s3len	$⊢ \|⟨“ A B C ”⟩\| = 3$
101	100	oveq2i	$⊢ (0 ..^\|⟨“ A B C ”⟩\|) = (0 ..^3)$
102	101	feq2i	$⊢ ⟨“ A B C ”⟩ : (0 ..^\|⟨“ A B C ”⟩\|) ⟶ P \leftrightarrow ⟨“ A B C ”⟩ : (0 ..^3) ⟶ P$
103	99 102	sylib	$⊢ φ \to ⟨“ A B C ”⟩ : (0 ..^3) ⟶ P$
104	103	fdmd	$⊢ φ \to dom ⟨“ A B C ”⟩ = (0 ..^3)$
105	104	raleqdv	$⊢ φ \to (\forall j \in dom ⟨“ A B C ”⟩ (i < j \to ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ W X Y ”⟩ (i) \underset{˙}{-} ⟨“ W X Y ”⟩ (j)) \leftrightarrow \forall j \in (0 ..^3) (i < j \to ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ W X Y ”⟩ (i) \underset{˙}{-} ⟨“ W X Y ”⟩ (j)))$
106	104 105	raleqbidv	$⊢ φ \to (\forall i \in dom ⟨“ A B C ”⟩ \forall j \in dom ⟨“ A B C ”⟩ (i < j \to ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ W X Y ”⟩ (i) \underset{˙}{-} ⟨“ W X Y ”⟩ (j)) \leftrightarrow \forall i \in (0 ..^3) \forall j \in (0 ..^3) (i < j \to ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ W X Y ”⟩ (i) \underset{˙}{-} ⟨“ W X Y ”⟩ (j)))$
107	57	a1i	$⊢ φ \to (0 ..^3) \subseteq ℝ$
108	10 11 12	s3cld	$⊢ φ \to ⟨“ W X Y ”⟩ \in Word P$
109		wrdf	$⊢ ⟨“ W X Y ”⟩ \in Word P \to ⟨“ W X Y ”⟩ : (0 ..^\|⟨“ W X Y ”⟩\|) ⟶ P$
110	108 109	syl	$⊢ φ \to ⟨“ W X Y ”⟩ : (0 ..^\|⟨“ W X Y ”⟩\|) ⟶ P$
111		s3len	$⊢ \|⟨“ W X Y ”⟩\| = 3$
112	111	oveq2i	$⊢ (0 ..^\|⟨“ W X Y ”⟩\|) = (0 ..^3)$
113	112	feq2i	$⊢ ⟨“ W X Y ”⟩ : (0 ..^\|⟨“ W X Y ”⟩\|) ⟶ P \leftrightarrow ⟨“ W X Y ”⟩ : (0 ..^3) ⟶ P$
114	110 113	sylib	$⊢ φ \to ⟨“ W X Y ”⟩ : (0 ..^3) ⟶ P$
115	1 2 4 5 107 103 114	iscgrglt	$⊢ φ \to (⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ W X Y ”⟩ \leftrightarrow \forall i \in dom ⟨“ A B C ”⟩ \forall j \in dom ⟨“ A B C ”⟩ (i < j \to ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ W X Y ”⟩ (i) \underset{˙}{-} ⟨“ W X Y ”⟩ (j)))$
116		df-s4	$⊢ ⟨“ A B C D ”⟩ = ⟨“ A B C ”⟩ ++ ⟨“ D ”⟩$
117	116	fveq1i	$⊢ ⟨“ A B C D ”⟩ (i) = (⟨“ A B C ”⟩ ++ ⟨“ D ”⟩) (i)$
118	6	adantr	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to A \in P$
119	7	adantr	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to B \in P$
120	8	adantr	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to C \in P$
121	118 119 120	s3cld	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to ⟨“ A B C ”⟩ \in Word P$
122	9	adantr	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to D \in P$
123	122	s1cld	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to ⟨“ D ”⟩ \in Word P$
124		simprl	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to i \in (0 ..^3)$
125	124 101	eleqtrrdi	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to i \in (0 ..^\|⟨“ A B C ”⟩\|)$
126		ccatval1	$⊢ (⟨“ A B C ”⟩ \in Word P \land ⟨“ D ”⟩ \in Word P \land i \in (0 ..^\|⟨“ A B C ”⟩\|)) \to (⟨“ A B C ”⟩ ++ ⟨“ D ”⟩) (i) = ⟨“ A B C ”⟩ (i)$
127	121 123 125 126	syl3anc	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to (⟨“ A B C ”⟩ ++ ⟨“ D ”⟩) (i) = ⟨“ A B C ”⟩ (i)$
128	117 127	syl5eq	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to ⟨“ A B C D ”⟩ (i) = ⟨“ A B C ”⟩ (i)$
129	116	fveq1i	$⊢ ⟨“ A B C D ”⟩ (j) = (⟨“ A B C ”⟩ ++ ⟨“ D ”⟩) (j)$
130		simprr	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to j \in (0 ..^3)$
131	130 101	eleqtrrdi	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to j \in (0 ..^\|⟨“ A B C ”⟩\|)$
132		ccatval1	$⊢ (⟨“ A B C ”⟩ \in Word P \land ⟨“ D ”⟩ \in Word P \land j \in (0 ..^\|⟨“ A B C ”⟩\|)) \to (⟨“ A B C ”⟩ ++ ⟨“ D ”⟩) (j) = ⟨“ A B C ”⟩ (j)$
133	121 123 131 132	syl3anc	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to (⟨“ A B C ”⟩ ++ ⟨“ D ”⟩) (j) = ⟨“ A B C ”⟩ (j)$
134	129 133	syl5eq	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to ⟨“ A B C D ”⟩ (j) = ⟨“ A B C ”⟩ (j)$
135	128 134	oveq12d	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j)$
136		df-s4	$⊢ ⟨“ W X Y Z ”⟩ = ⟨“ W X Y ”⟩ ++ ⟨“ Z ”⟩$
137	136	fveq1i	$⊢ ⟨“ W X Y Z ”⟩ (i) = (⟨“ W X Y ”⟩ ++ ⟨“ Z ”⟩) (i)$
138	10	adantr	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to W \in P$
139	11	adantr	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to X \in P$
140	12	adantr	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to Y \in P$
141	138 139 140	s3cld	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to ⟨“ W X Y ”⟩ \in Word P$
142	13	adantr	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to Z \in P$
143	142	s1cld	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to ⟨“ Z ”⟩ \in Word P$
144	124 112	eleqtrrdi	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to i \in (0 ..^\|⟨“ W X Y ”⟩\|)$
145		ccatval1	$⊢ (⟨“ W X Y ”⟩ \in Word P \land ⟨“ Z ”⟩ \in Word P \land i \in (0 ..^\|⟨“ W X Y ”⟩\|)) \to (⟨“ W X Y ”⟩ ++ ⟨“ Z ”⟩) (i) = ⟨“ W X Y ”⟩ (i)$
146	141 143 144 145	syl3anc	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to (⟨“ W X Y ”⟩ ++ ⟨“ Z ”⟩) (i) = ⟨“ W X Y ”⟩ (i)$
147	137 146	syl5eq	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to ⟨“ W X Y Z ”⟩ (i) = ⟨“ W X Y ”⟩ (i)$
148	136	fveq1i	$⊢ ⟨“ W X Y Z ”⟩ (j) = (⟨“ W X Y ”⟩ ++ ⟨“ Z ”⟩) (j)$
149	130 112	eleqtrrdi	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to j \in (0 ..^\|⟨“ W X Y ”⟩\|)$
150		ccatval1	$⊢ (⟨“ W X Y ”⟩ \in Word P \land ⟨“ Z ”⟩ \in Word P \land j \in (0 ..^\|⟨“ W X Y ”⟩\|)) \to (⟨“ W X Y ”⟩ ++ ⟨“ Z ”⟩) (j) = ⟨“ W X Y ”⟩ (j)$
151	141 143 149 150	syl3anc	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to (⟨“ W X Y ”⟩ ++ ⟨“ Z ”⟩) (j) = ⟨“ W X Y ”⟩ (j)$
152	148 151	syl5eq	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to ⟨“ W X Y Z ”⟩ (j) = ⟨“ W X Y ”⟩ (j)$
153	147 152	oveq12d	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j) = ⟨“ W X Y ”⟩ (i) \underset{˙}{-} ⟨“ W X Y ”⟩ (j)$
154	135 153	eqeq12d	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to (⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j) \leftrightarrow ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ W X Y ”⟩ (i) \underset{˙}{-} ⟨“ W X Y ”⟩ (j))$
155	154	imbi2d	$⊢ (φ \land (i \in (0 ..^3) \land j \in (0 ..^3))) \to ((i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \leftrightarrow (i < j \to ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ W X Y ”⟩ (i) \underset{˙}{-} ⟨“ W X Y ”⟩ (j)))$
156	155	2ralbidva	$⊢ φ \to (\forall i \in (0 ..^3) \forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \leftrightarrow \forall i \in (0 ..^3) \forall j \in (0 ..^3) (i < j \to ⟨“ A B C ”⟩ (i) \underset{˙}{-} ⟨“ A B C ”⟩ (j) = ⟨“ W X Y ”⟩ (i) \underset{˙}{-} ⟨“ W X Y ”⟩ (j)))$
157	106 115 156	3bitr4rd	$⊢ φ \to (\forall i \in (0 ..^3) \forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \leftrightarrow ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ W X Y ”⟩)$
158		fzo0to3tp	$⊢ (0 ..^3) = \{0, 1, 2\}$
159	158	raleqi	$⊢ \forall i \in (0 ..^3) (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3)) \leftrightarrow \forall i \in \{0, 1, 2\} (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3))$
160		3pos	$⊢ 0 < 3$
161		breq1	$⊢ i = 0 \to (i < 3 \leftrightarrow 0 < 3)$
162	160 161	mpbiri	$⊢ i = 0 \to i < 3$
163	162	adantl	$⊢ (φ \land i = 0) \to i < 3$
164		biimt	$⊢ i < 3 \to (⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3) \leftrightarrow (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3)))$
165	163 164	syl	$⊢ (φ \land i = 0) \to (⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3) \leftrightarrow (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3)))$
166		fveq2	$⊢ i = 0 \to ⟨“ A B C D ”⟩ (i) = ⟨“ A B C D ”⟩ (0)$
167		s4fv0	$⊢ A \in P \to ⟨“ A B C D ”⟩ (0) = A$
168	6 167	syl	$⊢ φ \to ⟨“ A B C D ”⟩ (0) = A$
169	166 168	sylan9eqr	$⊢ (φ \land i = 0) \to ⟨“ A B C D ”⟩ (i) = A$
170		s4fv3	$⊢ D \in P \to ⟨“ A B C D ”⟩ (3) = D$
171	9 170	syl	$⊢ φ \to ⟨“ A B C D ”⟩ (3) = D$
172	171	adantr	$⊢ (φ \land i = 0) \to ⟨“ A B C D ”⟩ (3) = D$
173	169 172	oveq12d	$⊢ (φ \land i = 0) \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = A \underset{˙}{-} D$
174		fveq2	$⊢ i = 0 \to ⟨“ W X Y Z ”⟩ (i) = ⟨“ W X Y Z ”⟩ (0)$
175		s4fv0	$⊢ W \in P \to ⟨“ W X Y Z ”⟩ (0) = W$
176	10 175	syl	$⊢ φ \to ⟨“ W X Y Z ”⟩ (0) = W$
177	174 176	sylan9eqr	$⊢ (φ \land i = 0) \to ⟨“ W X Y Z ”⟩ (i) = W$
178		s4fv3	$⊢ Z \in P \to ⟨“ W X Y Z ”⟩ (3) = Z$
179	13 178	syl	$⊢ φ \to ⟨“ W X Y Z ”⟩ (3) = Z$
180	179	adantr	$⊢ (φ \land i = 0) \to ⟨“ W X Y Z ”⟩ (3) = Z$
181	177 180	oveq12d	$⊢ (φ \land i = 0) \to ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3) = W \underset{˙}{-} Z$
182	173 181	eqeq12d	$⊢ (φ \land i = 0) \to (⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3) \leftrightarrow A \underset{˙}{-} D = W \underset{˙}{-} Z)$
183	165 182	bitr3d	$⊢ (φ \land i = 0) \to ((i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3)) \leftrightarrow A \underset{˙}{-} D = W \underset{˙}{-} Z)$
184		1lt3	$⊢ 1 < 3$
185		breq1	$⊢ i = 1 \to (i < 3 \leftrightarrow 1 < 3)$
186	184 185	mpbiri	$⊢ i = 1 \to i < 3$
187	186	adantl	$⊢ (φ \land i = 1) \to i < 3$
188	187 164	syl	$⊢ (φ \land i = 1) \to (⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3) \leftrightarrow (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3)))$
189		fveq2	$⊢ i = 1 \to ⟨“ A B C D ”⟩ (i) = ⟨“ A B C D ”⟩ (1)$
190		s4fv1	$⊢ B \in P \to ⟨“ A B C D ”⟩ (1) = B$
191	7 190	syl	$⊢ φ \to ⟨“ A B C D ”⟩ (1) = B$
192	189 191	sylan9eqr	$⊢ (φ \land i = 1) \to ⟨“ A B C D ”⟩ (i) = B$
193	171	adantr	$⊢ (φ \land i = 1) \to ⟨“ A B C D ”⟩ (3) = D$
194	192 193	oveq12d	$⊢ (φ \land i = 1) \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = B \underset{˙}{-} D$
195		fveq2	$⊢ i = 1 \to ⟨“ W X Y Z ”⟩ (i) = ⟨“ W X Y Z ”⟩ (1)$
196		s4fv1	$⊢ X \in P \to ⟨“ W X Y Z ”⟩ (1) = X$
197	11 196	syl	$⊢ φ \to ⟨“ W X Y Z ”⟩ (1) = X$
198	195 197	sylan9eqr	$⊢ (φ \land i = 1) \to ⟨“ W X Y Z ”⟩ (i) = X$
199	179	adantr	$⊢ (φ \land i = 1) \to ⟨“ W X Y Z ”⟩ (3) = Z$
200	198 199	oveq12d	$⊢ (φ \land i = 1) \to ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3) = X \underset{˙}{-} Z$
201	194 200	eqeq12d	$⊢ (φ \land i = 1) \to (⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3) \leftrightarrow B \underset{˙}{-} D = X \underset{˙}{-} Z)$
202	188 201	bitr3d	$⊢ (φ \land i = 1) \to ((i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3)) \leftrightarrow B \underset{˙}{-} D = X \underset{˙}{-} Z)$
203		2lt3	$⊢ 2 < 3$
204		breq1	$⊢ i = 2 \to (i < 3 \leftrightarrow 2 < 3)$
205	203 204	mpbiri	$⊢ i = 2 \to i < 3$
206	205	adantl	$⊢ (φ \land i = 2) \to i < 3$
207	206 164	syl	$⊢ (φ \land i = 2) \to (⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3) \leftrightarrow (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3)))$
208		fveq2	$⊢ i = 2 \to ⟨“ A B C D ”⟩ (i) = ⟨“ A B C D ”⟩ (2)$
209		s4fv2	$⊢ C \in P \to ⟨“ A B C D ”⟩ (2) = C$
210	8 209	syl	$⊢ φ \to ⟨“ A B C D ”⟩ (2) = C$
211	208 210	sylan9eqr	$⊢ (φ \land i = 2) \to ⟨“ A B C D ”⟩ (i) = C$
212	171	adantr	$⊢ (φ \land i = 2) \to ⟨“ A B C D ”⟩ (3) = D$
213	211 212	oveq12d	$⊢ (φ \land i = 2) \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = C \underset{˙}{-} D$
214		fveq2	$⊢ i = 2 \to ⟨“ W X Y Z ”⟩ (i) = ⟨“ W X Y Z ”⟩ (2)$
215		s4fv2	$⊢ Y \in P \to ⟨“ W X Y Z ”⟩ (2) = Y$
216	12 215	syl	$⊢ φ \to ⟨“ W X Y Z ”⟩ (2) = Y$
217	214 216	sylan9eqr	$⊢ (φ \land i = 2) \to ⟨“ W X Y Z ”⟩ (i) = Y$
218	179	adantr	$⊢ (φ \land i = 2) \to ⟨“ W X Y Z ”⟩ (3) = Z$
219	217 218	oveq12d	$⊢ (φ \land i = 2) \to ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3) = Y \underset{˙}{-} Z$
220	213 219	eqeq12d	$⊢ (φ \land i = 2) \to (⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3) \leftrightarrow C \underset{˙}{-} D = Y \underset{˙}{-} Z)$
221	207 220	bitr3d	$⊢ (φ \land i = 2) \to ((i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3)) \leftrightarrow C \underset{˙}{-} D = Y \underset{˙}{-} Z)$
222		0red	$⊢ φ \to 0 \in ℝ$
223		1red	$⊢ φ \to 1 \in ℝ$
224		2re	$⊢ 2 \in ℝ$
225	224	a1i	$⊢ φ \to 2 \in ℝ$
226	183 202 221 222 223 225	raltpd	$⊢ φ \to (\forall i \in \{0, 1, 2\} (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3)) \leftrightarrow (A \underset{˙}{-} D = W \underset{˙}{-} Z \land B \underset{˙}{-} D = X \underset{˙}{-} Z \land C \underset{˙}{-} D = Y \underset{˙}{-} Z))$
227	159 226	syl5bb	$⊢ φ \to (\forall i \in (0 ..^3) (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3)) \leftrightarrow (A \underset{˙}{-} D = W \underset{˙}{-} Z \land B \underset{˙}{-} D = X \underset{˙}{-} Z \land C \underset{˙}{-} D = Y \underset{˙}{-} Z))$
228	157 227	anbi12d	$⊢ φ \to ((\forall i \in (0 ..^3) \forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land \forall i \in (0 ..^3) (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3))) \leftrightarrow (⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ W X Y ”⟩ \land (A \underset{˙}{-} D = W \underset{˙}{-} Z \land B \underset{˙}{-} D = X \underset{˙}{-} Z \land C \underset{˙}{-} D = Y \underset{˙}{-} Z)))$
229	96 228	syl5bb	$⊢ φ \to (\forall i \in (0 ..^3) (\forall j \in (0 ..^3) (i < j \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (j) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (j)) \land (i < 3 \to ⟨“ A B C D ”⟩ (i) \underset{˙}{-} ⟨“ A B C D ”⟩ (3) = ⟨“ W X Y Z ”⟩ (i) \underset{˙}{-} ⟨“ W X Y Z ”⟩ (3))) \leftrightarrow (⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ W X Y ”⟩ \land (A \underset{˙}{-} D = W \underset{˙}{-} Z \land B \underset{˙}{-} D = X \underset{˙}{-} Z \land C \underset{˙}{-} D = Y \underset{˙}{-} Z)))$
230	32 95 229	3bitrd	$⊢ φ \to (⟨“ A B C D ”⟩ \underset{˙}{\sim} ⟨“ W X Y Z ”⟩ \leftrightarrow (⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ W X Y ”⟩ \land (A \underset{˙}{-} D = W \underset{˙}{-} Z \land B \underset{˙}{-} D = X \underset{˙}{-} Z \land C \underset{˙}{-} D = Y \underset{˙}{-} Z)))$

Metamath Proof Explorer

Theorem tgcgr4

Proof