tgcgr4 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > tgcgr4		Structured version Visualization version GIF version

Theorem tgcgr4 26316

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.)

**Hypotheses**
Ref	Expression
tgcgrxfr.p	⊢ 𝑃 = (Base‘𝐺)
tgcgrxfr.m	⊢ − = (dist‘𝐺)
tgcgrxfr.i	⊢ 𝐼 = (Itv‘𝐺)
tgcgrxfr.r	⊢ ∼ = (cgrG‘𝐺)
tgcgrxfr.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
tgcgr4.a	⊢ (𝜑 → 𝐴 ∈ 𝑃)
tgcgr4.b	⊢ (𝜑 → 𝐵 ∈ 𝑃)
tgcgr4.c	⊢ (𝜑 → 𝐶 ∈ 𝑃)
tgcgr4.d	⊢ (𝜑 → 𝐷 ∈ 𝑃)
tgcgr4.w	⊢ (𝜑 → 𝑊 ∈ 𝑃)
tgcgr4.x	⊢ (𝜑 → 𝑋 ∈ 𝑃)
tgcgr4.y	⊢ (𝜑 → 𝑌 ∈ 𝑃)
tgcgr4.z	⊢ (𝜑 → 𝑍 ∈ 𝑃)

**Assertion**
Ref	Expression
tgcgr4	⊢ (𝜑 → (⟨“𝐴𝐵𝐶𝐷”⟩ ∼ ⟨“𝑊𝑋𝑌𝑍”⟩ ↔ (⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝑊𝑋𝑌”⟩ ∧ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍)))))

Proof of Theorem tgcgr4 Dummy variables 𝑖 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tgcgrxfr.p	. . 3 ⊢ 𝑃 = (Base‘𝐺)
2		tgcgrxfr.m	. . 3 ⊢ − = (dist‘𝐺)
3		tgcgrxfr.r	. . 3 ⊢ ∼ = (cgrG‘𝐺)
4		tgcgrxfr.g	. . 3 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
5		fzo0ssnn0 13117	. . . . 5 ⊢ (0..^4) ⊆ ℕ₀
6		nn0ssre 11900	. . . . 5 ⊢ ℕ₀ ⊆ ℝ
7	5, 6	sstri 3975	. . . 4 ⊢ (0..^4) ⊆ ℝ
8	7	a1i 11	. . 3 ⊢ (𝜑 → (0..^4) ⊆ ℝ)
9		tgcgr4.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
10		tgcgr4.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
11		tgcgr4.c	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
12		tgcgr4.d	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
13	9, 10, 11, 12	s4cld 14234	. . . . 5 ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷”⟩ ∈ Word 𝑃)
14		wrdf 13865	. . . . 5 ⊢ (⟨“𝐴𝐵𝐶𝐷”⟩ ∈ Word 𝑃 → ⟨“𝐴𝐵𝐶𝐷”⟩:(0..^(♯‘⟨“𝐴𝐵𝐶𝐷”⟩))⟶𝑃)
15	13, 14	syl 17	. . . 4 ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷”⟩:(0..^(♯‘⟨“𝐴𝐵𝐶𝐷”⟩))⟶𝑃)
16		s4len 14260	. . . . . 6 ⊢ (♯‘⟨“𝐴𝐵𝐶𝐷”⟩) = 4
17	16	oveq2i 7166	. . . . 5 ⊢ (0..^(♯‘⟨“𝐴𝐵𝐶𝐷”⟩)) = (0..^4)
18	17	feq2i 6505	. . . 4 ⊢ (⟨“𝐴𝐵𝐶𝐷”⟩:(0..^(♯‘⟨“𝐴𝐵𝐶𝐷”⟩))⟶𝑃 ↔ ⟨“𝐴𝐵𝐶𝐷”⟩:(0..^4)⟶𝑃)
19	15, 18	sylib 220	. . 3 ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷”⟩:(0..^4)⟶𝑃)
20		tgcgr4.w	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ 𝑃)
21		tgcgr4.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
22		tgcgr4.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
23		tgcgr4.z	. . . . . 6 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
24	20, 21, 22, 23	s4cld 14234	. . . . 5 ⊢ (𝜑 → ⟨“𝑊𝑋𝑌𝑍”⟩ ∈ Word 𝑃)
25		wrdf 13865	. . . . 5 ⊢ (⟨“𝑊𝑋𝑌𝑍”⟩ ∈ Word 𝑃 → ⟨“𝑊𝑋𝑌𝑍”⟩:(0..^(♯‘⟨“𝑊𝑋𝑌𝑍”⟩))⟶𝑃)
26	24, 25	syl 17	. . . 4 ⊢ (𝜑 → ⟨“𝑊𝑋𝑌𝑍”⟩:(0..^(♯‘⟨“𝑊𝑋𝑌𝑍”⟩))⟶𝑃)
27		s4len 14260	. . . . . 6 ⊢ (♯‘⟨“𝑊𝑋𝑌𝑍”⟩) = 4
28	27	oveq2i 7166	. . . . 5 ⊢ (0..^(♯‘⟨“𝑊𝑋𝑌𝑍”⟩)) = (0..^4)
29	28	feq2i 6505	. . . 4 ⊢ (⟨“𝑊𝑋𝑌𝑍”⟩:(0..^(♯‘⟨“𝑊𝑋𝑌𝑍”⟩))⟶𝑃 ↔ ⟨“𝑊𝑋𝑌𝑍”⟩:(0..^4)⟶𝑃)
30	26, 29	sylib 220	. . 3 ⊢ (𝜑 → ⟨“𝑊𝑋𝑌𝑍”⟩:(0..^4)⟶𝑃)
31	1, 2, 3, 4, 8, 19, 30	iscgrglt 26299	. 2 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶𝐷”⟩ ∼ ⟨“𝑊𝑋𝑌𝑍”⟩ ↔ ∀𝑖 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩∀𝑗 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗)))))
32	19	fdmd 6522	. . . . . . 7 ⊢ (𝜑 → dom ⟨“𝐴𝐵𝐶𝐷”⟩ = (0..^4))
33		3p1e4 11781	. . . . . . . . 9 ⊢ (3 + 1) = 4
34	33	oveq2i 7166	. . . . . . . 8 ⊢ (0..^(3 + 1)) = (0..^4)
35		3nn0 11914	. . . . . . . . . 10 ⊢ 3 ∈ ℕ₀
36		nn0uz 12279	. . . . . . . . . 10 ⊢ ℕ₀ = (ℤ_≥‘0)
37	35, 36	eleqtri 2911	. . . . . . . . 9 ⊢ 3 ∈ (ℤ_≥‘0)
38		fzosplitsn 13144	. . . . . . . . 9 ⊢ (3 ∈ (ℤ_≥‘0) → (0..^(3 + 1)) = ((0..^3) ∪ {3}))
39	37, 38	ax-mp 5	. . . . . . . 8 ⊢ (0..^(3 + 1)) = ((0..^3) ∪ {3})
40	34, 39	eqtr3i 2846	. . . . . . 7 ⊢ (0..^4) = ((0..^3) ∪ {3})
41	32, 40	syl6eq 2872	. . . . . 6 ⊢ (𝜑 → dom ⟨“𝐴𝐵𝐶𝐷”⟩ = ((0..^3) ∪ {3}))
42	41	raleqdv 3415	. . . . 5 ⊢ (𝜑 → (∀𝑗 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ∀𝑗 ∈ ((0..^3) ∪ {3})(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗)))))
43		breq2 5069	. . . . . . . 8 ⊢ (𝑗 = 3 → (𝑖 < 𝑗 ↔ 𝑖 < 3))
44		fveq2 6669	. . . . . . . . . 10 ⊢ (𝑗 = 3 → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗) = (⟨“𝐴𝐵𝐶𝐷”⟩‘3))
45	44	oveq2d 7171	. . . . . . . . 9 ⊢ (𝑗 = 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)))
46		fveq2 6669	. . . . . . . . . 10 ⊢ (𝑗 = 3 → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗) = (⟨“𝑊𝑋𝑌𝑍”⟩‘3))
47	46	oveq2d 7171	. . . . . . . . 9 ⊢ (𝑗 = 3 → ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))
48	45, 47	eqeq12d 2837	. . . . . . . 8 ⊢ (𝑗 = 3 → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗)) ↔ ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))
49	43, 48	imbi12d 347	. . . . . . 7 ⊢ (𝑗 = 3 → ((𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))))
50	49	ralunsn 4823	. . . . . 6 ⊢ (3 ∈ ℕ₀ → (∀𝑗 ∈ ((0..^3) ∪ {3})(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ (∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))))
51	35, 50	ax-mp 5	. . . . 5 ⊢ (∀𝑗 ∈ ((0..^3) ∪ {3})(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ (∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))))
52	42, 51	syl6bb 289	. . . 4 ⊢ (𝜑 → (∀𝑗 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ (∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))))
53	52	ralbidv 3197	. . 3 ⊢ (𝜑 → (∀𝑖 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩∀𝑗 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ∀𝑖 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))))
54	41	raleqdv 3415	. . . 4 ⊢ (𝜑 → (∀𝑖 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ↔ ∀𝑖 ∈ ((0..^3) ∪ {3})(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))))
55		fzo0ssnn0 13117	. . . . . . . . . . . . . . . 16 ⊢ (0..^3) ⊆ ℕ₀
56	55, 6	sstri 3975	. . . . . . . . . . . . . . 15 ⊢ (0..^3) ⊆ ℝ
57		simpr 487	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑗 ∈ (0..^3))
58	56, 57	sseldi 3964	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑗 ∈ ℝ)
59		simpl 485	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑖 = 3)
60		3re 11716	. . . . . . . . . . . . . . 15 ⊢ 3 ∈ ℝ
61	59, 60	eqeltrdi 2921	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑖 ∈ ℝ)
62		elfzolt2 13046	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0..^3) → 𝑗 < 3)
63	62	adantl 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑗 < 3)
64	63, 59	breqtrrd 5093	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑗 < 𝑖)
65	58, 61, 64	ltnsymd 10788	. . . . . . . . . . . . 13 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → ¬ 𝑖 < 𝑗)
66	65	pm2.21d 121	. . . . . . . . . . . 12 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → (𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))))
67		tbtru 1541	. . . . . . . . . . . 12 ⊢ ((𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ((𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ⊤))
68	66, 67	sylib 220	. . . . . . . . . . 11 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → ((𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ⊤))
69	68	ralbidva 3196	. . . . . . . . . 10 ⊢ (𝑖 = 3 → (∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ∀𝑗 ∈ (0..^3)⊤))
70		3nn 11715	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℕ
71		lbfzo0 13076	. . . . . . . . . . . . 13 ⊢ (0 ∈ (0..^3) ↔ 3 ∈ ℕ)
72	70, 71	mpbir 233	. . . . . . . . . . . 12 ⊢ 0 ∈ (0..^3)
73	72	ne0ii 4302	. . . . . . . . . . 11 ⊢ (0..^3) ≠ ∅
74		r19.3rzv 4443	. . . . . . . . . . 11 ⊢ ((0..^3) ≠ ∅ → (⊤ ↔ ∀𝑗 ∈ (0..^3)⊤))
75	73, 74	ax-mp 5	. . . . . . . . . 10 ⊢ (⊤ ↔ ∀𝑗 ∈ (0..^3)⊤)
76	69, 75	syl6bbr 291	. . . . . . . . 9 ⊢ (𝑖 = 3 → (∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ⊤))
77		breq1 5068	. . . . . . . . . . . 12 ⊢ (𝑖 = 3 → (𝑖 < 3 ↔ 3 < 3))
78	60	ltnri 10748	. . . . . . . . . . . . 13 ⊢ ¬ 3 < 3
79	78	bifal 1549	. . . . . . . . . . . 12 ⊢ (3 < 3 ↔ ⊥)
80	77, 79	syl6bb 289	. . . . . . . . . . 11 ⊢ (𝑖 = 3 → (𝑖 < 3 ↔ ⊥))
81	80	imbi1d 344	. . . . . . . . . 10 ⊢ (𝑖 = 3 → ((𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ (⊥ → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))))
82		falim 1550	. . . . . . . . . . 11 ⊢ (⊥ → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))
83	82	bitru 1542	. . . . . . . . . 10 ⊢ ((⊥ → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ ⊤)
84	81, 83	syl6bb 289	. . . . . . . . 9 ⊢ (𝑖 = 3 → ((𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ ⊤))
85	76, 84	anbi12d 632	. . . . . . . 8 ⊢ (𝑖 = 3 → ((∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ↔ (⊤ ∧ ⊤)))
86		anidm 567	. . . . . . . 8 ⊢ ((⊤ ∧ ⊤) ↔ ⊤)
87	85, 86	syl6bb 289	. . . . . . 7 ⊢ (𝑖 = 3 → ((∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ↔ ⊤))
88	87	ralunsn 4823	. . . . . 6 ⊢ (3 ∈ ℕ₀ → (∀𝑖 ∈ ((0..^3) ∪ {3})(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ↔ (∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ∧ ⊤)))
89	35, 88	ax-mp 5	. . . . 5 ⊢ (∀𝑖 ∈ ((0..^3) ∪ {3})(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ↔ (∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ∧ ⊤))
90		ancom 463	. . . . 5 ⊢ ((∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ∧ ⊤) ↔ (⊤ ∧ ∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))))
91		truan 1544	. . . . 5 ⊢ ((⊤ ∧ ∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))) ↔ ∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))))
92	89, 90, 91	3bitri 299	. . . 4 ⊢ (∀𝑖 ∈ ((0..^3) ∪ {3})(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ↔ ∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))))
93	54, 92	syl6bb 289	. . 3 ⊢ (𝜑 → (∀𝑖 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ↔ ∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))))
94	53, 93	bitrd 281	. 2 ⊢ (𝜑 → (∀𝑖 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩∀𝑗 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))))
95		r19.26 3170	. . 3 ⊢ (∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ↔ (∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ ∀𝑖 ∈ (0..^3)(𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))))
96	9, 10, 11	s3cld 14233	. . . . . . . . 9 ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∈ Word 𝑃)
97		wrdf 13865	. . . . . . . . 9 ⊢ (⟨“𝐴𝐵𝐶”⟩ ∈ Word 𝑃 → ⟨“𝐴𝐵𝐶”⟩:(0..^(♯‘⟨“𝐴𝐵𝐶”⟩))⟶𝑃)
98	96, 97	syl 17	. . . . . . . 8 ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩:(0..^(♯‘⟨“𝐴𝐵𝐶”⟩))⟶𝑃)
99		s3len 14255	. . . . . . . . . 10 ⊢ (♯‘⟨“𝐴𝐵𝐶”⟩) = 3
100	99	oveq2i 7166	. . . . . . . . 9 ⊢ (0..^(♯‘⟨“𝐴𝐵𝐶”⟩)) = (0..^3)
101	100	feq2i 6505	. . . . . . . 8 ⊢ (⟨“𝐴𝐵𝐶”⟩:(0..^(♯‘⟨“𝐴𝐵𝐶”⟩))⟶𝑃 ↔ ⟨“𝐴𝐵𝐶”⟩:(0..^3)⟶𝑃)
102	98, 101	sylib 220	. . . . . . 7 ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩:(0..^3)⟶𝑃)
103	102	fdmd 6522	. . . . . 6 ⊢ (𝜑 → dom ⟨“𝐴𝐵𝐶”⟩ = (0..^3))
104	103	raleqdv 3415	. . . . . 6 ⊢ (𝜑 → (∀𝑗 ∈ dom ⟨“𝐴𝐵𝐶”⟩(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗))) ↔ ∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗)))))
105	103, 104	raleqbidv 3401	. . . . 5 ⊢ (𝜑 → (∀𝑖 ∈ dom ⟨“𝐴𝐵𝐶”⟩∀𝑗 ∈ dom ⟨“𝐴𝐵𝐶”⟩(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗))) ↔ ∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗)))))
106	56	a1i 11	. . . . . 6 ⊢ (𝜑 → (0..^3) ⊆ ℝ)
107	20, 21, 22	s3cld 14233	. . . . . . . 8 ⊢ (𝜑 → ⟨“𝑊𝑋𝑌”⟩ ∈ Word 𝑃)
108		wrdf 13865	. . . . . . . 8 ⊢ (⟨“𝑊𝑋𝑌”⟩ ∈ Word 𝑃 → ⟨“𝑊𝑋𝑌”⟩:(0..^(♯‘⟨“𝑊𝑋𝑌”⟩))⟶𝑃)
109	107, 108	syl 17	. . . . . . 7 ⊢ (𝜑 → ⟨“𝑊𝑋𝑌”⟩:(0..^(♯‘⟨“𝑊𝑋𝑌”⟩))⟶𝑃)
110		s3len 14255	. . . . . . . . 9 ⊢ (♯‘⟨“𝑊𝑋𝑌”⟩) = 3
111	110	oveq2i 7166	. . . . . . . 8 ⊢ (0..^(♯‘⟨“𝑊𝑋𝑌”⟩)) = (0..^3)
112	111	feq2i 6505	. . . . . . 7 ⊢ (⟨“𝑊𝑋𝑌”⟩:(0..^(♯‘⟨“𝑊𝑋𝑌”⟩))⟶𝑃 ↔ ⟨“𝑊𝑋𝑌”⟩:(0..^3)⟶𝑃)
113	109, 112	sylib 220	. . . . . 6 ⊢ (𝜑 → ⟨“𝑊𝑋𝑌”⟩:(0..^3)⟶𝑃)
114	1, 2, 3, 4, 106, 102, 113	iscgrglt 26299	. . . . 5 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝑊𝑋𝑌”⟩ ↔ ∀𝑖 ∈ dom ⟨“𝐴𝐵𝐶”⟩∀𝑗 ∈ dom ⟨“𝐴𝐵𝐶”⟩(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗)))))
115		df-s4 14211	. . . . . . . . . . 11 ⊢ ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
116	115	fveq1i 6670	. . . . . . . . . 10 ⊢ (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) = ((⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)‘𝑖)
117	9	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝐴 ∈ 𝑃)
118	10	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝐵 ∈ 𝑃)
119	11	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝐶 ∈ 𝑃)
120	117, 118, 119	s3cld 14233	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ⟨“𝐴𝐵𝐶”⟩ ∈ Word 𝑃)
121	12	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝐷 ∈ 𝑃)
122	121	s1cld 13956	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ⟨“𝐷”⟩ ∈ Word 𝑃)
123		simprl 769	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑖 ∈ (0..^3))
124	123, 100	eleqtrrdi 2924	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑖 ∈ (0..^(♯‘⟨“𝐴𝐵𝐶”⟩)))
125		ccatval1 13929	. . . . . . . . . . 11 ⊢ ((⟨“𝐴𝐵𝐶”⟩ ∈ Word 𝑃 ∧ ⟨“𝐷”⟩ ∈ Word 𝑃 ∧ 𝑖 ∈ (0..^(♯‘⟨“𝐴𝐵𝐶”⟩))) → ((⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)‘𝑖) = (⟨“𝐴𝐵𝐶”⟩‘𝑖))
126	120, 122, 124, 125	syl3anc 1367	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)‘𝑖) = (⟨“𝐴𝐵𝐶”⟩‘𝑖))
127	116, 126	syl5eq 2868	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) = (⟨“𝐴𝐵𝐶”⟩‘𝑖))
128	115	fveq1i 6670	. . . . . . . . . 10 ⊢ (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗) = ((⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)‘𝑗)
129		simprr 771	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑗 ∈ (0..^3))
130	129, 100	eleqtrrdi 2924	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑗 ∈ (0..^(♯‘⟨“𝐴𝐵𝐶”⟩)))
131		ccatval1 13929	. . . . . . . . . . 11 ⊢ ((⟨“𝐴𝐵𝐶”⟩ ∈ Word 𝑃 ∧ ⟨“𝐷”⟩ ∈ Word 𝑃 ∧ 𝑗 ∈ (0..^(♯‘⟨“𝐴𝐵𝐶”⟩))) → ((⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)‘𝑗) = (⟨“𝐴𝐵𝐶”⟩‘𝑗))
132	120, 122, 130, 131	syl3anc 1367	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)‘𝑗) = (⟨“𝐴𝐵𝐶”⟩‘𝑗))
133	128, 132	syl5eq 2868	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗) = (⟨“𝐴𝐵𝐶”⟩‘𝑗))
134	127, 133	oveq12d 7173	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)))
135		df-s4 14211	. . . . . . . . . . 11 ⊢ ⟨“𝑊𝑋𝑌𝑍”⟩ = (⟨“𝑊𝑋𝑌”⟩ ++ ⟨“𝑍”⟩)
136	135	fveq1i 6670	. . . . . . . . . 10 ⊢ (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) = ((⟨“𝑊𝑋𝑌”⟩ ++ ⟨“𝑍”⟩)‘𝑖)
137	20	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑊 ∈ 𝑃)
138	21	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑋 ∈ 𝑃)
139	22	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑌 ∈ 𝑃)
140	137, 138, 139	s3cld 14233	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ⟨“𝑊𝑋𝑌”⟩ ∈ Word 𝑃)
141	23	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑍 ∈ 𝑃)
142	141	s1cld 13956	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ⟨“𝑍”⟩ ∈ Word 𝑃)
143	123, 111	eleqtrrdi 2924	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑖 ∈ (0..^(♯‘⟨“𝑊𝑋𝑌”⟩)))
144		ccatval1 13929	. . . . . . . . . . 11 ⊢ ((⟨“𝑊𝑋𝑌”⟩ ∈ Word 𝑃 ∧ ⟨“𝑍”⟩ ∈ Word 𝑃 ∧ 𝑖 ∈ (0..^(♯‘⟨“𝑊𝑋𝑌”⟩))) → ((⟨“𝑊𝑋𝑌”⟩ ++ ⟨“𝑍”⟩)‘𝑖) = (⟨“𝑊𝑋𝑌”⟩‘𝑖))
145	140, 142, 143, 144	syl3anc 1367	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((⟨“𝑊𝑋𝑌”⟩ ++ ⟨“𝑍”⟩)‘𝑖) = (⟨“𝑊𝑋𝑌”⟩‘𝑖))
146	136, 145	syl5eq 2868	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) = (⟨“𝑊𝑋𝑌”⟩‘𝑖))
147	135	fveq1i 6670	. . . . . . . . . 10 ⊢ (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗) = ((⟨“𝑊𝑋𝑌”⟩ ++ ⟨“𝑍”⟩)‘𝑗)
148	129, 111	eleqtrrdi 2924	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑗 ∈ (0..^(♯‘⟨“𝑊𝑋𝑌”⟩)))
149		ccatval1 13929	. . . . . . . . . . 11 ⊢ ((⟨“𝑊𝑋𝑌”⟩ ∈ Word 𝑃 ∧ ⟨“𝑍”⟩ ∈ Word 𝑃 ∧ 𝑗 ∈ (0..^(♯‘⟨“𝑊𝑋𝑌”⟩))) → ((⟨“𝑊𝑋𝑌”⟩ ++ ⟨“𝑍”⟩)‘𝑗) = (⟨“𝑊𝑋𝑌”⟩‘𝑗))
150	140, 142, 148, 149	syl3anc 1367	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((⟨“𝑊𝑋𝑌”⟩ ++ ⟨“𝑍”⟩)‘𝑗) = (⟨“𝑊𝑋𝑌”⟩‘𝑗))
151	147, 150	syl5eq 2868	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗) = (⟨“𝑊𝑋𝑌”⟩‘𝑗))
152	146, 151	oveq12d 7173	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗)))
153	134, 152	eqeq12d 2837	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗)) ↔ ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗))))
154	153	imbi2d 343	. . . . . 6 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ (𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗)))))
155	154	2ralbidva 3198	. . . . 5 ⊢ (𝜑 → (∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗)))))
156	105, 114, 155	3bitr4rd 314	. . . 4 ⊢ (𝜑 → (∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝑊𝑋𝑌”⟩))
157		fzo0to3tp 13122	. . . . . 6 ⊢ (0..^3) = {0, 1, 2}
158	157	raleqi 3413	. . . . 5 ⊢ (∀𝑖 ∈ (0..^3)(𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ ∀𝑖 ∈ {0, 1, 2} (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))
159		3pos 11741	. . . . . . . . . 10 ⊢ 0 < 3
160		breq1 5068	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (𝑖 < 3 ↔ 0 < 3))
161	159, 160	mpbiri 260	. . . . . . . . 9 ⊢ (𝑖 = 0 → 𝑖 < 3)
162	161	adantl 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 0) → 𝑖 < 3)
163		biimt 363	. . . . . . . 8 ⊢ (𝑖 < 3 → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) ↔ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))))
164	162, 163	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = 0) → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) ↔ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))))
165		fveq2 6669	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) = (⟨“𝐴𝐵𝐶𝐷”⟩‘0))
166		s4fv0 14256	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑃 → (⟨“𝐴𝐵𝐶𝐷”⟩‘0) = 𝐴)
167	9, 166	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶𝐷”⟩‘0) = 𝐴)
168	165, 167	sylan9eqr 2878	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 0) → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) = 𝐴)
169		s4fv3 14259	. . . . . . . . . . 11 ⊢ (𝐷 ∈ 𝑃 → (⟨“𝐴𝐵𝐶𝐷”⟩‘3) = 𝐷)
170	12, 169	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶𝐷”⟩‘3) = 𝐷)
171	170	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 0) → (⟨“𝐴𝐵𝐶𝐷”⟩‘3) = 𝐷)
172	168, 171	oveq12d 7173	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 0) → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = (𝐴 − 𝐷))
173		fveq2 6669	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) = (⟨“𝑊𝑋𝑌𝑍”⟩‘0))
174		s4fv0 14256	. . . . . . . . . . 11 ⊢ (𝑊 ∈ 𝑃 → (⟨“𝑊𝑋𝑌𝑍”⟩‘0) = 𝑊)
175	20, 174	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝑊𝑋𝑌𝑍”⟩‘0) = 𝑊)
176	173, 175	sylan9eqr 2878	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 0) → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) = 𝑊)
177		s4fv3 14259	. . . . . . . . . . 11 ⊢ (𝑍 ∈ 𝑃 → (⟨“𝑊𝑋𝑌𝑍”⟩‘3) = 𝑍)
178	23, 177	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝑊𝑋𝑌𝑍”⟩‘3) = 𝑍)
179	178	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 0) → (⟨“𝑊𝑋𝑌𝑍”⟩‘3) = 𝑍)
180	176, 179	oveq12d 7173	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 0) → ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) = (𝑊 − 𝑍))
181	172, 180	eqeq12d 2837	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = 0) → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) ↔ (𝐴 − 𝐷) = (𝑊 − 𝑍)))
182	164, 181	bitr3d 283	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ (𝐴 − 𝐷) = (𝑊 − 𝑍)))
183		1lt3 11809	. . . . . . . . . 10 ⊢ 1 < 3
184		breq1 5068	. . . . . . . . . 10 ⊢ (𝑖 = 1 → (𝑖 < 3 ↔ 1 < 3))
185	183, 184	mpbiri 260	. . . . . . . . 9 ⊢ (𝑖 = 1 → 𝑖 < 3)
186	185	adantl 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 1) → 𝑖 < 3)
187	186, 163	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = 1) → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) ↔ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))))
188		fveq2 6669	. . . . . . . . . 10 ⊢ (𝑖 = 1 → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) = (⟨“𝐴𝐵𝐶𝐷”⟩‘1))
189		s4fv1 14257	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑃 → (⟨“𝐴𝐵𝐶𝐷”⟩‘1) = 𝐵)
190	10, 189	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶𝐷”⟩‘1) = 𝐵)
191	188, 190	sylan9eqr 2878	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 1) → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) = 𝐵)
192	170	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 1) → (⟨“𝐴𝐵𝐶𝐷”⟩‘3) = 𝐷)
193	191, 192	oveq12d 7173	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 1) → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = (𝐵 − 𝐷))
194		fveq2 6669	. . . . . . . . . 10 ⊢ (𝑖 = 1 → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) = (⟨“𝑊𝑋𝑌𝑍”⟩‘1))
195		s4fv1 14257	. . . . . . . . . . 11 ⊢ (𝑋 ∈ 𝑃 → (⟨“𝑊𝑋𝑌𝑍”⟩‘1) = 𝑋)
196	21, 195	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝑊𝑋𝑌𝑍”⟩‘1) = 𝑋)
197	194, 196	sylan9eqr 2878	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 1) → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) = 𝑋)
198	178	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 1) → (⟨“𝑊𝑋𝑌𝑍”⟩‘3) = 𝑍)
199	197, 198	oveq12d 7173	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 1) → ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) = (𝑋 − 𝑍))
200	193, 199	eqeq12d 2837	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = 1) → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) ↔ (𝐵 − 𝐷) = (𝑋 − 𝑍)))
201	187, 200	bitr3d 283	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 = 1) → ((𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ (𝐵 − 𝐷) = (𝑋 − 𝑍)))
202		2lt3 11808	. . . . . . . . . 10 ⊢ 2 < 3
203		breq1 5068	. . . . . . . . . 10 ⊢ (𝑖 = 2 → (𝑖 < 3 ↔ 2 < 3))
204	202, 203	mpbiri 260	. . . . . . . . 9 ⊢ (𝑖 = 2 → 𝑖 < 3)
205	204	adantl 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 2) → 𝑖 < 3)
206	205, 163	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = 2) → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) ↔ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))))
207		fveq2 6669	. . . . . . . . . 10 ⊢ (𝑖 = 2 → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) = (⟨“𝐴𝐵𝐶𝐷”⟩‘2))
208		s4fv2 14258	. . . . . . . . . . 11 ⊢ (𝐶 ∈ 𝑃 → (⟨“𝐴𝐵𝐶𝐷”⟩‘2) = 𝐶)
209	11, 208	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶𝐷”⟩‘2) = 𝐶)
210	207, 209	sylan9eqr 2878	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 2) → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) = 𝐶)
211	170	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 2) → (⟨“𝐴𝐵𝐶𝐷”⟩‘3) = 𝐷)
212	210, 211	oveq12d 7173	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 2) → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = (𝐶 − 𝐷))
213		fveq2 6669	. . . . . . . . . 10 ⊢ (𝑖 = 2 → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) = (⟨“𝑊𝑋𝑌𝑍”⟩‘2))
214		s4fv2 14258	. . . . . . . . . . 11 ⊢ (𝑌 ∈ 𝑃 → (⟨“𝑊𝑋𝑌𝑍”⟩‘2) = 𝑌)
215	22, 214	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝑊𝑋𝑌𝑍”⟩‘2) = 𝑌)
216	213, 215	sylan9eqr 2878	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 2) → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) = 𝑌)
217	178	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 2) → (⟨“𝑊𝑋𝑌𝑍”⟩‘3) = 𝑍)
218	216, 217	oveq12d 7173	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 2) → ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) = (𝑌 − 𝑍))
219	212, 218	eqeq12d 2837	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = 2) → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) ↔ (𝐶 − 𝐷) = (𝑌 − 𝑍)))
220	206, 219	bitr3d 283	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 = 2) → ((𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ (𝐶 − 𝐷) = (𝑌 − 𝑍)))
221		0red 10643	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℝ)
222		1red 10641	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℝ)
223		2re 11710	. . . . . . 7 ⊢ 2 ∈ ℝ
224	223	a1i 11	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℝ)
225	182, 201, 220, 221, 222, 224	raltpd 4715	. . . . 5 ⊢ (𝜑 → (∀𝑖 ∈ {0, 1, 2} (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍))))
226	158, 225	syl5bb 285	. . . 4 ⊢ (𝜑 → (∀𝑖 ∈ (0..^3)(𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍))))
227	156, 226	anbi12d 632	. . 3 ⊢ (𝜑 → ((∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ ∀𝑖 ∈ (0..^3)(𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ↔ (⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝑊𝑋𝑌”⟩ ∧ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍)))))
228	95, 227	syl5bb 285	. 2 ⊢ (𝜑 → (∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ↔ (⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝑊𝑋𝑌”⟩ ∧ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍)))))
229	31, 94, 228	3bitrd 307	1 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶𝐷”⟩ ∼ ⟨“𝑊𝑋𝑌𝑍”⟩ ↔ (⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝑊𝑋𝑌”⟩ ∧ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ⊤wtru 1534 ⊥wfal 1545 ∈ wcel 2110 ≠ wne 3016 ∀wral 3138 ∪ cun 3933 ⊆ wss 3935 ∅c0 4290 {csn 4566 {ctp 4570 class class class wbr 5065 dom cdm 5554 ⟶wf 6350 ‘cfv 6354 (class class class)co 7155 ℝcr 10535 0cc0 10536 1c1 10537 + caddc 10539 < clt 10674 ℕcn 11637 2c2 11691 3c3 11692 4c4 11693 ℕ₀cn0 11896 ℤ_≥cuz 12242 ..^cfzo 13032 ♯chash 13689 Word cword 13860 ++ cconcat 13921 ⟨“cs1 13948 ⟨“cs3 14203 ⟨“cs4 14204 Basecbs 16482 distcds 16573 TarskiGcstrkg 26215 Itvcitv 26221 cgrGccgrg 26295

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-rep 5189 ax-sep 5202 ax-nul 5209 ax-pow 5265 ax-pr 5329 ax-un 7460 ax-cnex 10592 ax-resscn 10593 ax-1cn 10594 ax-icn 10595 ax-addcl 10596 ax-addrcl 10597 ax-mulcl 10598 ax-mulrcl 10599 ax-mulcom 10600 ax-addass 10601 ax-mulass 10602 ax-distr 10603 ax-i2m1 10604 ax-1ne0 10605 ax-1rid 10606 ax-rnegex 10607 ax-rrecex 10608 ax-cnre 10609 ax-pre-lttri 10610 ax-pre-lttrn 10611 ax-pre-ltadd 10612 ax-pre-mulgt0 10613

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-fal 1546 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4567 df-pr 4569 df-tp 4571 df-op 4573 df-uni 4838 df-int 4876 df-iun 4920 df-br 5066 df-opab 5128 df-mpt 5146 df-tr 5172 df-id 5459 df-eprel 5464 df-po 5473 df-so 5474 df-fr 5513 df-we 5515 df-xp 5560 df-rel 5561 df-cnv 5562 df-co 5563 df-dm 5564 df-rn 5565 df-res 5566 df-ima 5567 df-pred 6147 df-ord 6193 df-on 6194 df-lim 6195 df-suc 6196 df-iota 6313 df-fun 6356 df-fn 6357 df-f 6358 df-f1 6359 df-fo 6360 df-f1o 6361 df-fv 6362 df-riota 7113 df-ov 7158 df-oprab 7159 df-mpo 7160 df-om 7580 df-1st 7688 df-2nd 7689 df-wrecs 7946 df-recs 8007 df-rdg 8045 df-1o 8101 df-oadd 8105 df-er 8288 df-pm 8408 df-en 8509 df-dom 8510 df-sdom 8511 df-fin 8512 df-card 9367 df-pnf 10676 df-mnf 10677 df-xr 10678 df-ltxr 10679 df-le 10680 df-sub 10871 df-neg 10872 df-nn 11638 df-2 11699 df-3 11700 df-4 11701 df-n0 11897 df-z 11981 df-uz 12243 df-fz 12892 df-fzo 13033 df-hash 13690 df-word 13861 df-concat 13922 df-s1 13949 df-s2 14209 df-s3 14210 df-s4 14211 df-trkgc 26233 df-trkgcb 26235 df-trkg 26238 df-cgrg 26296

This theorem is referenced by: cgrg3col4 26638

W3C validator