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 27772

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 13710	. . . . 5 ⊢ (0..^4) ⊆ ℕ₀
6		nn0ssre 12473	. . . . 5 ⊢ ℕ₀ ⊆ ℝ
7	5, 6	sstri 3991	. . . 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 14821	. . . . 5 ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷”⟩ ∈ Word 𝑃)
14		wrdf 14466	. . . . 5 ⊢ (⟨“𝐴𝐵𝐶𝐷”⟩ ∈ Word 𝑃 → ⟨“𝐴𝐵𝐶𝐷”⟩:(0..^(♯‘⟨“𝐴𝐵𝐶𝐷”⟩))⟶𝑃)
15	13, 14	syl 17	. . . 4 ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷”⟩:(0..^(♯‘⟨“𝐴𝐵𝐶𝐷”⟩))⟶𝑃)
16		s4len 14847	. . . . . 6 ⊢ (♯‘⟨“𝐴𝐵𝐶𝐷”⟩) = 4
17	16	oveq2i 7417	. . . . 5 ⊢ (0..^(♯‘⟨“𝐴𝐵𝐶𝐷”⟩)) = (0..^4)
18	17	feq2i 6707	. . . 4 ⊢ (⟨“𝐴𝐵𝐶𝐷”⟩:(0..^(♯‘⟨“𝐴𝐵𝐶𝐷”⟩))⟶𝑃 ↔ ⟨“𝐴𝐵𝐶𝐷”⟩:(0..^4)⟶𝑃)
19	15, 18	sylib 217	. . 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 14821	. . . . 5 ⊢ (𝜑 → ⟨“𝑊𝑋𝑌𝑍”⟩ ∈ Word 𝑃)
25		wrdf 14466	. . . . 5 ⊢ (⟨“𝑊𝑋𝑌𝑍”⟩ ∈ Word 𝑃 → ⟨“𝑊𝑋𝑌𝑍”⟩:(0..^(♯‘⟨“𝑊𝑋𝑌𝑍”⟩))⟶𝑃)
26	24, 25	syl 17	. . . 4 ⊢ (𝜑 → ⟨“𝑊𝑋𝑌𝑍”⟩:(0..^(♯‘⟨“𝑊𝑋𝑌𝑍”⟩))⟶𝑃)
27		s4len 14847	. . . . . 6 ⊢ (♯‘⟨“𝑊𝑋𝑌𝑍”⟩) = 4
28	27	oveq2i 7417	. . . . 5 ⊢ (0..^(♯‘⟨“𝑊𝑋𝑌𝑍”⟩)) = (0..^4)
29	28	feq2i 6707	. . . 4 ⊢ (⟨“𝑊𝑋𝑌𝑍”⟩:(0..^(♯‘⟨“𝑊𝑋𝑌𝑍”⟩))⟶𝑃 ↔ ⟨“𝑊𝑋𝑌𝑍”⟩:(0..^4)⟶𝑃)
30	26, 29	sylib 217	. . 3 ⊢ (𝜑 → ⟨“𝑊𝑋𝑌𝑍”⟩:(0..^4)⟶𝑃)
31	1, 2, 3, 4, 8, 19, 30	iscgrglt 27755	. 2 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶𝐷”⟩ ∼ ⟨“𝑊𝑋𝑌𝑍”⟩ ↔ ∀𝑖 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩∀𝑗 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗)))))
32	19	fdmd 6726	. . . . . . 7 ⊢ (𝜑 → dom ⟨“𝐴𝐵𝐶𝐷”⟩ = (0..^4))
33		3p1e4 12354	. . . . . . . . 9 ⊢ (3 + 1) = 4
34	33	oveq2i 7417	. . . . . . . 8 ⊢ (0..^(3 + 1)) = (0..^4)
35		3nn0 12487	. . . . . . . . . 10 ⊢ 3 ∈ ℕ₀
36		nn0uz 12861	. . . . . . . . . 10 ⊢ ℕ₀ = (ℤ_≥‘0)
37	35, 36	eleqtri 2832	. . . . . . . . 9 ⊢ 3 ∈ (ℤ_≥‘0)
38		fzosplitsn 13737	. . . . . . . . 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 2763	. . . . . . 7 ⊢ (0..^4) = ((0..^3) ∪ {3})
41	32, 40	eqtrdi 2789	. . . . . 6 ⊢ (𝜑 → dom ⟨“𝐴𝐵𝐶𝐷”⟩ = ((0..^3) ∪ {3}))
42	41	raleqdv 3326	. . . . 5 ⊢ (𝜑 → (∀𝑗 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ∀𝑗 ∈ ((0..^3) ∪ {3})(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗)))))
43		breq2 5152	. . . . . . . 8 ⊢ (𝑗 = 3 → (𝑖 < 𝑗 ↔ 𝑖 < 3))
44		fveq2 6889	. . . . . . . . . 10 ⊢ (𝑗 = 3 → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗) = (⟨“𝐴𝐵𝐶𝐷”⟩‘3))
45	44	oveq2d 7422	. . . . . . . . 9 ⊢ (𝑗 = 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)))
46		fveq2 6889	. . . . . . . . . 10 ⊢ (𝑗 = 3 → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗) = (⟨“𝑊𝑋𝑌𝑍”⟩‘3))
47	46	oveq2d 7422	. . . . . . . . 9 ⊢ (𝑗 = 3 → ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))
48	45, 47	eqeq12d 2749	. . . . . . . 8 ⊢ (𝑗 = 3 → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗)) ↔ ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))
49	43, 48	imbi12d 345	. . . . . . 7 ⊢ (𝑗 = 3 → ((𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))))
50	49	ralunsn 4894	. . . . . 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	bitrdi 287	. . . 4 ⊢ (𝜑 → (∀𝑗 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ (∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))))
53	52	ralbidv 3178	. . 3 ⊢ (𝜑 → (∀𝑖 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩∀𝑗 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ∀𝑖 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))))
54	41	raleqdv 3326	. . . 4 ⊢ (𝜑 → (∀𝑖 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ↔ ∀𝑖 ∈ ((0..^3) ∪ {3})(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))))
55		fzo0ssnn0 13710	. . . . . . . . . . . . . . . 16 ⊢ (0..^3) ⊆ ℕ₀
56	55, 6	sstri 3991	. . . . . . . . . . . . . . 15 ⊢ (0..^3) ⊆ ℝ
57		simpr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑗 ∈ (0..^3))
58	56, 57	sselid 3980	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑗 ∈ ℝ)
59		simpl 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑖 = 3)
60		3re 12289	. . . . . . . . . . . . . . 15 ⊢ 3 ∈ ℝ
61	59, 60	eqeltrdi 2842	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑖 ∈ ℝ)
62		elfzolt2 13638	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0..^3) → 𝑗 < 3)
63	62	adantl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑗 < 3)
64	63, 59	breqtrrd 5176	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑗 < 𝑖)
65	58, 61, 64	ltnsymd 11360	. . . . . . . . . . . . 13 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → ¬ 𝑖 < 𝑗)
66	65	pm2.21d 121	. . . . . . . . . . . 12 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → (𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))))
67		tbtru 1550	. . . . . . . . . . . 12 ⊢ ((𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ((𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ⊤))
68	66, 67	sylib 217	. . . . . . . . . . 11 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → ((𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ⊤))
69	68	ralbidva 3176	. . . . . . . . . 10 ⊢ (𝑖 = 3 → (∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ∀𝑗 ∈ (0..^3)⊤))
70		3nn 12288	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℕ
71		lbfzo0 13669	. . . . . . . . . . . . 13 ⊢ (0 ∈ (0..^3) ↔ 3 ∈ ℕ)
72	70, 71	mpbir 230	. . . . . . . . . . . 12 ⊢ 0 ∈ (0..^3)
73	72	ne0ii 4337	. . . . . . . . . . 11 ⊢ (0..^3) ≠ ∅
74		r19.3rzv 4498	. . . . . . . . . . 11 ⊢ ((0..^3) ≠ ∅ → (⊤ ↔ ∀𝑗 ∈ (0..^3)⊤))
75	73, 74	ax-mp 5	. . . . . . . . . 10 ⊢ (⊤ ↔ ∀𝑗 ∈ (0..^3)⊤)
76	69, 75	bitr4di 289	. . . . . . . . 9 ⊢ (𝑖 = 3 → (∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ⊤))
77		breq1 5151	. . . . . . . . . . . 12 ⊢ (𝑖 = 3 → (𝑖 < 3 ↔ 3 < 3))
78	60	ltnri 11320	. . . . . . . . . . . . 13 ⊢ ¬ 3 < 3
79	78	bifal 1558	. . . . . . . . . . . 12 ⊢ (3 < 3 ↔ ⊥)
80	77, 79	bitrdi 287	. . . . . . . . . . 11 ⊢ (𝑖 = 3 → (𝑖 < 3 ↔ ⊥))
81	80	imbi1d 342	. . . . . . . . . 10 ⊢ (𝑖 = 3 → ((𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ (⊥ → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))))
82		falim 1559	. . . . . . . . . . 11 ⊢ (⊥ → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))
83	82	bitru 1551	. . . . . . . . . 10 ⊢ ((⊥ → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ ⊤)
84	81, 83	bitrdi 287	. . . . . . . . 9 ⊢ (𝑖 = 3 → ((𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ ⊤))
85	76, 84	anbi12d 632	. . . . . . . 8 ⊢ (𝑖 = 3 → ((∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ↔ (⊤ ∧ ⊤)))
86		anidm 566	. . . . . . . 8 ⊢ ((⊤ ∧ ⊤) ↔ ⊤)
87	85, 86	bitrdi 287	. . . . . . 7 ⊢ (𝑖 = 3 → ((∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ↔ ⊤))
88	87	ralunsn 4894	. . . . . 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 462	. . . . 5 ⊢ ((∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ∧ ⊤) ↔ (⊤ ∧ ∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))))
91		truan 1553	. . . . 5 ⊢ ((⊤ ∧ ∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))) ↔ ∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))))
92	89, 90, 91	3bitri 297	. . . 4 ⊢ (∀𝑖 ∈ ((0..^3) ∪ {3})(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ↔ ∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))))
93	54, 92	bitrdi 287	. . 3 ⊢ (𝜑 → (∀𝑖 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ↔ ∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))))
94	53, 93	bitrd 279	. 2 ⊢ (𝜑 → (∀𝑖 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩∀𝑗 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))))
95		r19.26 3112	. . 3 ⊢ (∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ↔ (∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ ∀𝑖 ∈ (0..^3)(𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))))
96	9, 10, 11	s3cld 14820	. . . . . . . . 9 ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∈ Word 𝑃)
97		wrdf 14466	. . . . . . . . 9 ⊢ (⟨“𝐴𝐵𝐶”⟩ ∈ Word 𝑃 → ⟨“𝐴𝐵𝐶”⟩:(0..^(♯‘⟨“𝐴𝐵𝐶”⟩))⟶𝑃)
98	96, 97	syl 17	. . . . . . . 8 ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩:(0..^(♯‘⟨“𝐴𝐵𝐶”⟩))⟶𝑃)
99		s3len 14842	. . . . . . . . . 10 ⊢ (♯‘⟨“𝐴𝐵𝐶”⟩) = 3
100	99	oveq2i 7417	. . . . . . . . 9 ⊢ (0..^(♯‘⟨“𝐴𝐵𝐶”⟩)) = (0..^3)
101	100	feq2i 6707	. . . . . . . 8 ⊢ (⟨“𝐴𝐵𝐶”⟩:(0..^(♯‘⟨“𝐴𝐵𝐶”⟩))⟶𝑃 ↔ ⟨“𝐴𝐵𝐶”⟩:(0..^3)⟶𝑃)
102	98, 101	sylib 217	. . . . . . 7 ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩:(0..^3)⟶𝑃)
103	102	fdmd 6726	. . . . . 6 ⊢ (𝜑 → dom ⟨“𝐴𝐵𝐶”⟩ = (0..^3))
104	103	raleqdv 3326	. . . . . 6 ⊢ (𝜑 → (∀𝑗 ∈ dom ⟨“𝐴𝐵𝐶”⟩(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗))) ↔ ∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗)))))
105	103, 104	raleqbidv 3343	. . . . 5 ⊢ (𝜑 → (∀𝑖 ∈ dom ⟨“𝐴𝐵𝐶”⟩∀𝑗 ∈ dom ⟨“𝐴𝐵𝐶”⟩(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗))) ↔ ∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗)))))
106	56	a1i 11	. . . . . 6 ⊢ (𝜑 → (0..^3) ⊆ ℝ)
107	20, 21, 22	s3cld 14820	. . . . . . . 8 ⊢ (𝜑 → ⟨“𝑊𝑋𝑌”⟩ ∈ Word 𝑃)
108		wrdf 14466	. . . . . . . 8 ⊢ (⟨“𝑊𝑋𝑌”⟩ ∈ Word 𝑃 → ⟨“𝑊𝑋𝑌”⟩:(0..^(♯‘⟨“𝑊𝑋𝑌”⟩))⟶𝑃)
109	107, 108	syl 17	. . . . . . 7 ⊢ (𝜑 → ⟨“𝑊𝑋𝑌”⟩:(0..^(♯‘⟨“𝑊𝑋𝑌”⟩))⟶𝑃)
110		s3len 14842	. . . . . . . . 9 ⊢ (♯‘⟨“𝑊𝑋𝑌”⟩) = 3
111	110	oveq2i 7417	. . . . . . . 8 ⊢ (0..^(♯‘⟨“𝑊𝑋𝑌”⟩)) = (0..^3)
112	111	feq2i 6707	. . . . . . 7 ⊢ (⟨“𝑊𝑋𝑌”⟩:(0..^(♯‘⟨“𝑊𝑋𝑌”⟩))⟶𝑃 ↔ ⟨“𝑊𝑋𝑌”⟩:(0..^3)⟶𝑃)
113	109, 112	sylib 217	. . . . . 6 ⊢ (𝜑 → ⟨“𝑊𝑋𝑌”⟩:(0..^3)⟶𝑃)
114	1, 2, 3, 4, 106, 102, 113	iscgrglt 27755	. . . . 5 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝑊𝑋𝑌”⟩ ↔ ∀𝑖 ∈ dom ⟨“𝐴𝐵𝐶”⟩∀𝑗 ∈ dom ⟨“𝐴𝐵𝐶”⟩(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗)))))
115		df-s4 14798	. . . . . . . . . . 11 ⊢ ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
116	115	fveq1i 6890	. . . . . . . . . 10 ⊢ (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) = ((⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)‘𝑖)
117	9	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝐴 ∈ 𝑃)
118	10	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝐵 ∈ 𝑃)
119	11	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝐶 ∈ 𝑃)
120	117, 118, 119	s3cld 14820	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ⟨“𝐴𝐵𝐶”⟩ ∈ Word 𝑃)
121	12	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝐷 ∈ 𝑃)
122	121	s1cld 14550	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ⟨“𝐷”⟩ ∈ Word 𝑃)
123		simprl 770	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑖 ∈ (0..^3))
124	123, 100	eleqtrrdi 2845	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑖 ∈ (0..^(♯‘⟨“𝐴𝐵𝐶”⟩)))
125		ccatval1 14524	. . . . . . . . . . 11 ⊢ ((⟨“𝐴𝐵𝐶”⟩ ∈ Word 𝑃 ∧ ⟨“𝐷”⟩ ∈ Word 𝑃 ∧ 𝑖 ∈ (0..^(♯‘⟨“𝐴𝐵𝐶”⟩))) → ((⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)‘𝑖) = (⟨“𝐴𝐵𝐶”⟩‘𝑖))
126	120, 122, 124, 125	syl3anc 1372	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)‘𝑖) = (⟨“𝐴𝐵𝐶”⟩‘𝑖))
127	116, 126	eqtrid 2785	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) = (⟨“𝐴𝐵𝐶”⟩‘𝑖))
128	115	fveq1i 6890	. . . . . . . . . 10 ⊢ (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗) = ((⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)‘𝑗)
129		simprr 772	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑗 ∈ (0..^3))
130	129, 100	eleqtrrdi 2845	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑗 ∈ (0..^(♯‘⟨“𝐴𝐵𝐶”⟩)))
131		ccatval1 14524	. . . . . . . . . . 11 ⊢ ((⟨“𝐴𝐵𝐶”⟩ ∈ Word 𝑃 ∧ ⟨“𝐷”⟩ ∈ Word 𝑃 ∧ 𝑗 ∈ (0..^(♯‘⟨“𝐴𝐵𝐶”⟩))) → ((⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)‘𝑗) = (⟨“𝐴𝐵𝐶”⟩‘𝑗))
132	120, 122, 130, 131	syl3anc 1372	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)‘𝑗) = (⟨“𝐴𝐵𝐶”⟩‘𝑗))
133	128, 132	eqtrid 2785	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗) = (⟨“𝐴𝐵𝐶”⟩‘𝑗))
134	127, 133	oveq12d 7424	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)))
135		df-s4 14798	. . . . . . . . . . 11 ⊢ ⟨“𝑊𝑋𝑌𝑍”⟩ = (⟨“𝑊𝑋𝑌”⟩ ++ ⟨“𝑍”⟩)
136	135	fveq1i 6890	. . . . . . . . . 10 ⊢ (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) = ((⟨“𝑊𝑋𝑌”⟩ ++ ⟨“𝑍”⟩)‘𝑖)
137	20	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑊 ∈ 𝑃)
138	21	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑋 ∈ 𝑃)
139	22	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑌 ∈ 𝑃)
140	137, 138, 139	s3cld 14820	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ⟨“𝑊𝑋𝑌”⟩ ∈ Word 𝑃)
141	23	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑍 ∈ 𝑃)
142	141	s1cld 14550	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ⟨“𝑍”⟩ ∈ Word 𝑃)
143	123, 111	eleqtrrdi 2845	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑖 ∈ (0..^(♯‘⟨“𝑊𝑋𝑌”⟩)))
144		ccatval1 14524	. . . . . . . . . . 11 ⊢ ((⟨“𝑊𝑋𝑌”⟩ ∈ Word 𝑃 ∧ ⟨“𝑍”⟩ ∈ Word 𝑃 ∧ 𝑖 ∈ (0..^(♯‘⟨“𝑊𝑋𝑌”⟩))) → ((⟨“𝑊𝑋𝑌”⟩ ++ ⟨“𝑍”⟩)‘𝑖) = (⟨“𝑊𝑋𝑌”⟩‘𝑖))
145	140, 142, 143, 144	syl3anc 1372	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((⟨“𝑊𝑋𝑌”⟩ ++ ⟨“𝑍”⟩)‘𝑖) = (⟨“𝑊𝑋𝑌”⟩‘𝑖))
146	136, 145	eqtrid 2785	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) = (⟨“𝑊𝑋𝑌”⟩‘𝑖))
147	135	fveq1i 6890	. . . . . . . . . 10 ⊢ (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗) = ((⟨“𝑊𝑋𝑌”⟩ ++ ⟨“𝑍”⟩)‘𝑗)
148	129, 111	eleqtrrdi 2845	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑗 ∈ (0..^(♯‘⟨“𝑊𝑋𝑌”⟩)))
149		ccatval1 14524	. . . . . . . . . . 11 ⊢ ((⟨“𝑊𝑋𝑌”⟩ ∈ Word 𝑃 ∧ ⟨“𝑍”⟩ ∈ Word 𝑃 ∧ 𝑗 ∈ (0..^(♯‘⟨“𝑊𝑋𝑌”⟩))) → ((⟨“𝑊𝑋𝑌”⟩ ++ ⟨“𝑍”⟩)‘𝑗) = (⟨“𝑊𝑋𝑌”⟩‘𝑗))
150	140, 142, 148, 149	syl3anc 1372	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((⟨“𝑊𝑋𝑌”⟩ ++ ⟨“𝑍”⟩)‘𝑗) = (⟨“𝑊𝑋𝑌”⟩‘𝑗))
151	147, 150	eqtrid 2785	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗) = (⟨“𝑊𝑋𝑌”⟩‘𝑗))
152	146, 151	oveq12d 7424	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗)))
153	134, 152	eqeq12d 2749	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗)) ↔ ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗))))
154	153	imbi2d 341	. . . . . 6 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ (𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗)))))
155	154	2ralbidva 3217	. . . . 5 ⊢ (𝜑 → (∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗)))))
156	105, 114, 155	3bitr4rd 312	. . . 4 ⊢ (𝜑 → (∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝑊𝑋𝑌”⟩))
157		fzo0to3tp 13715	. . . . . 6 ⊢ (0..^3) = {0, 1, 2}
158	157	raleqi 3324	. . . . 5 ⊢ (∀𝑖 ∈ (0..^3)(𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ ∀𝑖 ∈ {0, 1, 2} (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))
159		3pos 12314	. . . . . . . . . 10 ⊢ 0 < 3
160		breq1 5151	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (𝑖 < 3 ↔ 0 < 3))
161	159, 160	mpbiri 258	. . . . . . . . 9 ⊢ (𝑖 = 0 → 𝑖 < 3)
162	161	adantl 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 0) → 𝑖 < 3)
163		biimt 361	. . . . . . . 8 ⊢ (𝑖 < 3 → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) ↔ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))))
164	162, 163	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = 0) → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) ↔ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))))
165		fveq2 6889	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) = (⟨“𝐴𝐵𝐶𝐷”⟩‘0))
166		s4fv0 14843	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑃 → (⟨“𝐴𝐵𝐶𝐷”⟩‘0) = 𝐴)
167	9, 166	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶𝐷”⟩‘0) = 𝐴)
168	165, 167	sylan9eqr 2795	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 0) → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) = 𝐴)
169		s4fv3 14846	. . . . . . . . . . 11 ⊢ (𝐷 ∈ 𝑃 → (⟨“𝐴𝐵𝐶𝐷”⟩‘3) = 𝐷)
170	12, 169	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶𝐷”⟩‘3) = 𝐷)
171	170	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 0) → (⟨“𝐴𝐵𝐶𝐷”⟩‘3) = 𝐷)
172	168, 171	oveq12d 7424	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 0) → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = (𝐴 − 𝐷))
173		fveq2 6889	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) = (⟨“𝑊𝑋𝑌𝑍”⟩‘0))
174		s4fv0 14843	. . . . . . . . . . 11 ⊢ (𝑊 ∈ 𝑃 → (⟨“𝑊𝑋𝑌𝑍”⟩‘0) = 𝑊)
175	20, 174	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝑊𝑋𝑌𝑍”⟩‘0) = 𝑊)
176	173, 175	sylan9eqr 2795	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 0) → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) = 𝑊)
177		s4fv3 14846	. . . . . . . . . . 11 ⊢ (𝑍 ∈ 𝑃 → (⟨“𝑊𝑋𝑌𝑍”⟩‘3) = 𝑍)
178	23, 177	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝑊𝑋𝑌𝑍”⟩‘3) = 𝑍)
179	178	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 0) → (⟨“𝑊𝑋𝑌𝑍”⟩‘3) = 𝑍)
180	176, 179	oveq12d 7424	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 0) → ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) = (𝑊 − 𝑍))
181	172, 180	eqeq12d 2749	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = 0) → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) ↔ (𝐴 − 𝐷) = (𝑊 − 𝑍)))
182	164, 181	bitr3d 281	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ (𝐴 − 𝐷) = (𝑊 − 𝑍)))
183		1lt3 12382	. . . . . . . . . 10 ⊢ 1 < 3
184		breq1 5151	. . . . . . . . . 10 ⊢ (𝑖 = 1 → (𝑖 < 3 ↔ 1 < 3))
185	183, 184	mpbiri 258	. . . . . . . . 9 ⊢ (𝑖 = 1 → 𝑖 < 3)
186	185	adantl 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 1) → 𝑖 < 3)
187	186, 163	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = 1) → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) ↔ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))))
188		fveq2 6889	. . . . . . . . . 10 ⊢ (𝑖 = 1 → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) = (⟨“𝐴𝐵𝐶𝐷”⟩‘1))
189		s4fv1 14844	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑃 → (⟨“𝐴𝐵𝐶𝐷”⟩‘1) = 𝐵)
190	10, 189	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶𝐷”⟩‘1) = 𝐵)
191	188, 190	sylan9eqr 2795	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 1) → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) = 𝐵)
192	170	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 1) → (⟨“𝐴𝐵𝐶𝐷”⟩‘3) = 𝐷)
193	191, 192	oveq12d 7424	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 1) → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = (𝐵 − 𝐷))
194		fveq2 6889	. . . . . . . . . 10 ⊢ (𝑖 = 1 → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) = (⟨“𝑊𝑋𝑌𝑍”⟩‘1))
195		s4fv1 14844	. . . . . . . . . . 11 ⊢ (𝑋 ∈ 𝑃 → (⟨“𝑊𝑋𝑌𝑍”⟩‘1) = 𝑋)
196	21, 195	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝑊𝑋𝑌𝑍”⟩‘1) = 𝑋)
197	194, 196	sylan9eqr 2795	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 1) → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) = 𝑋)
198	178	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 1) → (⟨“𝑊𝑋𝑌𝑍”⟩‘3) = 𝑍)
199	197, 198	oveq12d 7424	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 1) → ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) = (𝑋 − 𝑍))
200	193, 199	eqeq12d 2749	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = 1) → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) ↔ (𝐵 − 𝐷) = (𝑋 − 𝑍)))
201	187, 200	bitr3d 281	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 = 1) → ((𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ (𝐵 − 𝐷) = (𝑋 − 𝑍)))
202		2lt3 12381	. . . . . . . . . 10 ⊢ 2 < 3
203		breq1 5151	. . . . . . . . . 10 ⊢ (𝑖 = 2 → (𝑖 < 3 ↔ 2 < 3))
204	202, 203	mpbiri 258	. . . . . . . . 9 ⊢ (𝑖 = 2 → 𝑖 < 3)
205	204	adantl 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 2) → 𝑖 < 3)
206	205, 163	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = 2) → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) ↔ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))))
207		fveq2 6889	. . . . . . . . . 10 ⊢ (𝑖 = 2 → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) = (⟨“𝐴𝐵𝐶𝐷”⟩‘2))
208		s4fv2 14845	. . . . . . . . . . 11 ⊢ (𝐶 ∈ 𝑃 → (⟨“𝐴𝐵𝐶𝐷”⟩‘2) = 𝐶)
209	11, 208	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶𝐷”⟩‘2) = 𝐶)
210	207, 209	sylan9eqr 2795	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 2) → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) = 𝐶)
211	170	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 2) → (⟨“𝐴𝐵𝐶𝐷”⟩‘3) = 𝐷)
212	210, 211	oveq12d 7424	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 2) → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = (𝐶 − 𝐷))
213		fveq2 6889	. . . . . . . . . 10 ⊢ (𝑖 = 2 → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) = (⟨“𝑊𝑋𝑌𝑍”⟩‘2))
214		s4fv2 14845	. . . . . . . . . . 11 ⊢ (𝑌 ∈ 𝑃 → (⟨“𝑊𝑋𝑌𝑍”⟩‘2) = 𝑌)
215	22, 214	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝑊𝑋𝑌𝑍”⟩‘2) = 𝑌)
216	213, 215	sylan9eqr 2795	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 2) → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) = 𝑌)
217	178	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 2) → (⟨“𝑊𝑋𝑌𝑍”⟩‘3) = 𝑍)
218	216, 217	oveq12d 7424	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 2) → ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) = (𝑌 − 𝑍))
219	212, 218	eqeq12d 2749	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = 2) → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) ↔ (𝐶 − 𝐷) = (𝑌 − 𝑍)))
220	206, 219	bitr3d 281	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 = 2) → ((𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ (𝐶 − 𝐷) = (𝑌 − 𝑍)))
221		0red 11214	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℝ)
222		1red 11212	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℝ)
223		2re 12283	. . . . . . 7 ⊢ 2 ∈ ℝ
224	223	a1i 11	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℝ)
225	182, 201, 220, 221, 222, 224	raltpd 4785	. . . . 5 ⊢ (𝜑 → (∀𝑖 ∈ {0, 1, 2} (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍))))
226	158, 225	bitrid 283	. . . 4 ⊢ (𝜑 → (∀𝑖 ∈ (0..^3)(𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍))))
227	156, 226	anbi12d 632	. . 3 ⊢ (𝜑 → ((∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ ∀𝑖 ∈ (0..^3)(𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ↔ (⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝑊𝑋𝑌”⟩ ∧ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍)))))
228	95, 227	bitrid 283	. 2 ⊢ (𝜑 → (∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ↔ (⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝑊𝑋𝑌”⟩ ∧ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍)))))
229	31, 94, 228	3bitrd 305	1 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶𝐷”⟩ ∼ ⟨“𝑊𝑋𝑌𝑍”⟩ ↔ (⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝑊𝑋𝑌”⟩ ∧ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ⊤wtru 1543 ⊥wfal 1554 ∈ wcel 2107 ≠ wne 2941 ∀wral 3062 ∪ cun 3946 ⊆ wss 3948 ∅c0 4322 {csn 4628 {ctp 4632 class class class wbr 5148 dom cdm 5676 ⟶wf 6537 ‘cfv 6541 (class class class)co 7406 ℝcr 11106 0cc0 11107 1c1 11108 + caddc 11110 < clt 11245 ℕcn 12209 2c2 12264 3c3 12265 4c4 12266 ℕ₀cn0 12469 ℤ_≥cuz 12819 ..^cfzo 13624 ♯chash 14287 Word cword 14461 ++ cconcat 14517 ⟨“cs1 14542 ⟨“cs3 14790 ⟨“cs4 14791 Basecbs 17141 distcds 17203 TarskiGcstrkg 27668 Itvcitv 27674 cgrGccgrg 27751

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 ax-cnex 11163 ax-resscn 11164 ax-1cn 11165 ax-icn 11166 ax-addcl 11167 ax-addrcl 11168 ax-mulcl 11169 ax-mulrcl 11170 ax-mulcom 11171 ax-addass 11172 ax-mulass 11173 ax-distr 11174 ax-i2m1 11175 ax-1ne0 11176 ax-1rid 11177 ax-rnegex 11178 ax-rrecex 11179 ax-cnre 11180 ax-pre-lttri 11181 ax-pre-lttrn 11182 ax-pre-ltadd 11183 ax-pre-mulgt0 11184

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6298 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7362 df-ov 7409 df-oprab 7410 df-mpo 7411 df-om 7853 df-1st 7972 df-2nd 7973 df-frecs 8263 df-wrecs 8294 df-recs 8368 df-rdg 8407 df-1o 8463 df-er 8700 df-pm 8820 df-en 8937 df-dom 8938 df-sdom 8939 df-fin 8940 df-card 9931 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-nn 12210 df-2 12272 df-3 12273 df-4 12274 df-n0 12470 df-z 12556 df-uz 12820 df-fz 13482 df-fzo 13625 df-hash 14288 df-word 14462 df-concat 14518 df-s1 14543 df-s2 14796 df-s3 14797 df-s4 14798 df-trkgc 27689 df-trkgcb 27691 df-trkg 27694 df-cgrg 27752

This theorem is referenced by: cgrg3col4 28094

W3C validator