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 26892

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 13468	. . . . 5 ⊢ (0..^4) ⊆ ℕ₀
6		nn0ssre 12237	. . . . 5 ⊢ ℕ₀ ⊆ ℝ
7	5, 6	sstri 3930	. . . 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 14586	. . . . 5 ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷”⟩ ∈ Word 𝑃)
14		wrdf 14222	. . . . 5 ⊢ (⟨“𝐴𝐵𝐶𝐷”⟩ ∈ Word 𝑃 → ⟨“𝐴𝐵𝐶𝐷”⟩:(0..^(♯‘⟨“𝐴𝐵𝐶𝐷”⟩))⟶𝑃)
15	13, 14	syl 17	. . . 4 ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷”⟩:(0..^(♯‘⟨“𝐴𝐵𝐶𝐷”⟩))⟶𝑃)
16		s4len 14612	. . . . . 6 ⊢ (♯‘⟨“𝐴𝐵𝐶𝐷”⟩) = 4
17	16	oveq2i 7286	. . . . 5 ⊢ (0..^(♯‘⟨“𝐴𝐵𝐶𝐷”⟩)) = (0..^4)
18	17	feq2i 6592	. . . 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 14586	. . . . 5 ⊢ (𝜑 → ⟨“𝑊𝑋𝑌𝑍”⟩ ∈ Word 𝑃)
25		wrdf 14222	. . . . 5 ⊢ (⟨“𝑊𝑋𝑌𝑍”⟩ ∈ Word 𝑃 → ⟨“𝑊𝑋𝑌𝑍”⟩:(0..^(♯‘⟨“𝑊𝑋𝑌𝑍”⟩))⟶𝑃)
26	24, 25	syl 17	. . . 4 ⊢ (𝜑 → ⟨“𝑊𝑋𝑌𝑍”⟩:(0..^(♯‘⟨“𝑊𝑋𝑌𝑍”⟩))⟶𝑃)
27		s4len 14612	. . . . . 6 ⊢ (♯‘⟨“𝑊𝑋𝑌𝑍”⟩) = 4
28	27	oveq2i 7286	. . . . 5 ⊢ (0..^(♯‘⟨“𝑊𝑋𝑌𝑍”⟩)) = (0..^4)
29	28	feq2i 6592	. . . 4 ⊢ (⟨“𝑊𝑋𝑌𝑍”⟩:(0..^(♯‘⟨“𝑊𝑋𝑌𝑍”⟩))⟶𝑃 ↔ ⟨“𝑊𝑋𝑌𝑍”⟩:(0..^4)⟶𝑃)
30	26, 29	sylib 217	. . 3 ⊢ (𝜑 → ⟨“𝑊𝑋𝑌𝑍”⟩:(0..^4)⟶𝑃)
31	1, 2, 3, 4, 8, 19, 30	iscgrglt 26875	. 2 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶𝐷”⟩ ∼ ⟨“𝑊𝑋𝑌𝑍”⟩ ↔ ∀𝑖 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩∀𝑗 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗)))))
32	19	fdmd 6611	. . . . . . 7 ⊢ (𝜑 → dom ⟨“𝐴𝐵𝐶𝐷”⟩ = (0..^4))
33		3p1e4 12118	. . . . . . . . 9 ⊢ (3 + 1) = 4
34	33	oveq2i 7286	. . . . . . . 8 ⊢ (0..^(3 + 1)) = (0..^4)
35		3nn0 12251	. . . . . . . . . 10 ⊢ 3 ∈ ℕ₀
36		nn0uz 12620	. . . . . . . . . 10 ⊢ ℕ₀ = (ℤ_≥‘0)
37	35, 36	eleqtri 2837	. . . . . . . . 9 ⊢ 3 ∈ (ℤ_≥‘0)
38		fzosplitsn 13495	. . . . . . . . 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 2768	. . . . . . 7 ⊢ (0..^4) = ((0..^3) ∪ {3})
41	32, 40	eqtrdi 2794	. . . . . 6 ⊢ (𝜑 → dom ⟨“𝐴𝐵𝐶𝐷”⟩ = ((0..^3) ∪ {3}))
42	41	raleqdv 3348	. . . . 5 ⊢ (𝜑 → (∀𝑗 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ∀𝑗 ∈ ((0..^3) ∪ {3})(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗)))))
43		breq2 5078	. . . . . . . 8 ⊢ (𝑗 = 3 → (𝑖 < 𝑗 ↔ 𝑖 < 3))
44		fveq2 6774	. . . . . . . . . 10 ⊢ (𝑗 = 3 → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗) = (⟨“𝐴𝐵𝐶𝐷”⟩‘3))
45	44	oveq2d 7291	. . . . . . . . 9 ⊢ (𝑗 = 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)))
46		fveq2 6774	. . . . . . . . . 10 ⊢ (𝑗 = 3 → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗) = (⟨“𝑊𝑋𝑌𝑍”⟩‘3))
47	46	oveq2d 7291	. . . . . . . . 9 ⊢ (𝑗 = 3 → ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))
48	45, 47	eqeq12d 2754	. . . . . . . 8 ⊢ (𝑗 = 3 → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗)) ↔ ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))
49	43, 48	imbi12d 345	. . . . . . 7 ⊢ (𝑗 = 3 → ((𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))))
50	49	ralunsn 4825	. . . . . 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 3112	. . 3 ⊢ (𝜑 → (∀𝑖 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩∀𝑗 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ∀𝑖 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))))
54	41	raleqdv 3348	. . . 4 ⊢ (𝜑 → (∀𝑖 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ↔ ∀𝑖 ∈ ((0..^3) ∪ {3})(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))))
55		fzo0ssnn0 13468	. . . . . . . . . . . . . . . 16 ⊢ (0..^3) ⊆ ℕ₀
56	55, 6	sstri 3930	. . . . . . . . . . . . . . 15 ⊢ (0..^3) ⊆ ℝ
57		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑗 ∈ (0..^3))
58	56, 57	sselid 3919	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑗 ∈ ℝ)
59		simpl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑖 = 3)
60		3re 12053	. . . . . . . . . . . . . . 15 ⊢ 3 ∈ ℝ
61	59, 60	eqeltrdi 2847	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑖 ∈ ℝ)
62		elfzolt2 13396	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0..^3) → 𝑗 < 3)
63	62	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑗 < 3)
64	63, 59	breqtrrd 5102	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → 𝑗 < 𝑖)
65	58, 61, 64	ltnsymd 11124	. . . . . . . . . . . . 13 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → ¬ 𝑖 < 𝑗)
66	65	pm2.21d 121	. . . . . . . . . . . 12 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → (𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))))
67		tbtru 1547	. . . . . . . . . . . 12 ⊢ ((𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ((𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ⊤))
68	66, 67	sylib 217	. . . . . . . . . . 11 ⊢ ((𝑖 = 3 ∧ 𝑗 ∈ (0..^3)) → ((𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ⊤))
69	68	ralbidva 3111	. . . . . . . . . 10 ⊢ (𝑖 = 3 → (∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ∀𝑗 ∈ (0..^3)⊤))
70		3nn 12052	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℕ
71		lbfzo0 13427	. . . . . . . . . . . . 13 ⊢ (0 ∈ (0..^3) ↔ 3 ∈ ℕ)
72	70, 71	mpbir 230	. . . . . . . . . . . 12 ⊢ 0 ∈ (0..^3)
73	72	ne0ii 4271	. . . . . . . . . . 11 ⊢ (0..^3) ≠ ∅
74		r19.3rzv 4429	. . . . . . . . . . 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 5077	. . . . . . . . . . . 12 ⊢ (𝑖 = 3 → (𝑖 < 3 ↔ 3 < 3))
78	60	ltnri 11084	. . . . . . . . . . . . 13 ⊢ ¬ 3 < 3
79	78	bifal 1555	. . . . . . . . . . . 12 ⊢ (3 < 3 ↔ ⊥)
80	77, 79	bitrdi 287	. . . . . . . . . . 11 ⊢ (𝑖 = 3 → (𝑖 < 3 ↔ ⊥))
81	80	imbi1d 342	. . . . . . . . . 10 ⊢ (𝑖 = 3 → ((𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ (⊥ → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))))
82		falim 1556	. . . . . . . . . . 11 ⊢ (⊥ → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))
83	82	bitru 1548	. . . . . . . . . 10 ⊢ ((⊥ → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ ⊤)
84	81, 83	bitrdi 287	. . . . . . . . 9 ⊢ (𝑖 = 3 → ((𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ ⊤))
85	76, 84	anbi12d 631	. . . . . . . 8 ⊢ (𝑖 = 3 → ((∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ↔ (⊤ ∧ ⊤)))
86		anidm 565	. . . . . . . 8 ⊢ ((⊤ ∧ ⊤) ↔ ⊤)
87	85, 86	bitrdi 287	. . . . . . 7 ⊢ (𝑖 = 3 → ((∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ↔ ⊤))
88	87	ralunsn 4825	. . . . . 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 461	. . . . 5 ⊢ ((∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ∧ ⊤) ↔ (⊤ ∧ ∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))))
91		truan 1550	. . . . 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 278	. 2 ⊢ (𝜑 → (∀𝑖 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩∀𝑗 ∈ dom ⟨“𝐴𝐵𝐶𝐷”⟩(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))))
95		r19.26 3095	. . 3 ⊢ (∀𝑖 ∈ (0..^3)(∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ↔ (∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ ∀𝑖 ∈ (0..^3)(𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))))
96	9, 10, 11	s3cld 14585	. . . . . . . . 9 ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∈ Word 𝑃)
97		wrdf 14222	. . . . . . . . 9 ⊢ (⟨“𝐴𝐵𝐶”⟩ ∈ Word 𝑃 → ⟨“𝐴𝐵𝐶”⟩:(0..^(♯‘⟨“𝐴𝐵𝐶”⟩))⟶𝑃)
98	96, 97	syl 17	. . . . . . . 8 ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩:(0..^(♯‘⟨“𝐴𝐵𝐶”⟩))⟶𝑃)
99		s3len 14607	. . . . . . . . . 10 ⊢ (♯‘⟨“𝐴𝐵𝐶”⟩) = 3
100	99	oveq2i 7286	. . . . . . . . 9 ⊢ (0..^(♯‘⟨“𝐴𝐵𝐶”⟩)) = (0..^3)
101	100	feq2i 6592	. . . . . . . 8 ⊢ (⟨“𝐴𝐵𝐶”⟩:(0..^(♯‘⟨“𝐴𝐵𝐶”⟩))⟶𝑃 ↔ ⟨“𝐴𝐵𝐶”⟩:(0..^3)⟶𝑃)
102	98, 101	sylib 217	. . . . . . 7 ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩:(0..^3)⟶𝑃)
103	102	fdmd 6611	. . . . . 6 ⊢ (𝜑 → dom ⟨“𝐴𝐵𝐶”⟩ = (0..^3))
104	103	raleqdv 3348	. . . . . 6 ⊢ (𝜑 → (∀𝑗 ∈ dom ⟨“𝐴𝐵𝐶”⟩(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗))) ↔ ∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗)))))
105	103, 104	raleqbidv 3336	. . . . 5 ⊢ (𝜑 → (∀𝑖 ∈ dom ⟨“𝐴𝐵𝐶”⟩∀𝑗 ∈ dom ⟨“𝐴𝐵𝐶”⟩(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗))) ↔ ∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗)))))
106	56	a1i 11	. . . . . 6 ⊢ (𝜑 → (0..^3) ⊆ ℝ)
107	20, 21, 22	s3cld 14585	. . . . . . . 8 ⊢ (𝜑 → ⟨“𝑊𝑋𝑌”⟩ ∈ Word 𝑃)
108		wrdf 14222	. . . . . . . 8 ⊢ (⟨“𝑊𝑋𝑌”⟩ ∈ Word 𝑃 → ⟨“𝑊𝑋𝑌”⟩:(0..^(♯‘⟨“𝑊𝑋𝑌”⟩))⟶𝑃)
109	107, 108	syl 17	. . . . . . 7 ⊢ (𝜑 → ⟨“𝑊𝑋𝑌”⟩:(0..^(♯‘⟨“𝑊𝑋𝑌”⟩))⟶𝑃)
110		s3len 14607	. . . . . . . . 9 ⊢ (♯‘⟨“𝑊𝑋𝑌”⟩) = 3
111	110	oveq2i 7286	. . . . . . . 8 ⊢ (0..^(♯‘⟨“𝑊𝑋𝑌”⟩)) = (0..^3)
112	111	feq2i 6592	. . . . . . 7 ⊢ (⟨“𝑊𝑋𝑌”⟩:(0..^(♯‘⟨“𝑊𝑋𝑌”⟩))⟶𝑃 ↔ ⟨“𝑊𝑋𝑌”⟩:(0..^3)⟶𝑃)
113	109, 112	sylib 217	. . . . . 6 ⊢ (𝜑 → ⟨“𝑊𝑋𝑌”⟩:(0..^3)⟶𝑃)
114	1, 2, 3, 4, 106, 102, 113	iscgrglt 26875	. . . . 5 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝑊𝑋𝑌”⟩ ↔ ∀𝑖 ∈ dom ⟨“𝐴𝐵𝐶”⟩∀𝑗 ∈ dom ⟨“𝐴𝐵𝐶”⟩(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗)))))
115		df-s4 14563	. . . . . . . . . . 11 ⊢ ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
116	115	fveq1i 6775	. . . . . . . . . 10 ⊢ (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) = ((⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)‘𝑖)
117	9	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝐴 ∈ 𝑃)
118	10	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝐵 ∈ 𝑃)
119	11	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝐶 ∈ 𝑃)
120	117, 118, 119	s3cld 14585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ⟨“𝐴𝐵𝐶”⟩ ∈ Word 𝑃)
121	12	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝐷 ∈ 𝑃)
122	121	s1cld 14308	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ⟨“𝐷”⟩ ∈ Word 𝑃)
123		simprl 768	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑖 ∈ (0..^3))
124	123, 100	eleqtrrdi 2850	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑖 ∈ (0..^(♯‘⟨“𝐴𝐵𝐶”⟩)))
125		ccatval1 14281	. . . . . . . . . . 11 ⊢ ((⟨“𝐴𝐵𝐶”⟩ ∈ Word 𝑃 ∧ ⟨“𝐷”⟩ ∈ Word 𝑃 ∧ 𝑖 ∈ (0..^(♯‘⟨“𝐴𝐵𝐶”⟩))) → ((⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)‘𝑖) = (⟨“𝐴𝐵𝐶”⟩‘𝑖))
126	120, 122, 124, 125	syl3anc 1370	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)‘𝑖) = (⟨“𝐴𝐵𝐶”⟩‘𝑖))
127	116, 126	eqtrid 2790	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) = (⟨“𝐴𝐵𝐶”⟩‘𝑖))
128	115	fveq1i 6775	. . . . . . . . . 10 ⊢ (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗) = ((⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)‘𝑗)
129		simprr 770	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑗 ∈ (0..^3))
130	129, 100	eleqtrrdi 2850	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑗 ∈ (0..^(♯‘⟨“𝐴𝐵𝐶”⟩)))
131		ccatval1 14281	. . . . . . . . . . 11 ⊢ ((⟨“𝐴𝐵𝐶”⟩ ∈ Word 𝑃 ∧ ⟨“𝐷”⟩ ∈ Word 𝑃 ∧ 𝑗 ∈ (0..^(♯‘⟨“𝐴𝐵𝐶”⟩))) → ((⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)‘𝑗) = (⟨“𝐴𝐵𝐶”⟩‘𝑗))
132	120, 122, 130, 131	syl3anc 1370	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)‘𝑗) = (⟨“𝐴𝐵𝐶”⟩‘𝑗))
133	128, 132	eqtrid 2790	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗) = (⟨“𝐴𝐵𝐶”⟩‘𝑗))
134	127, 133	oveq12d 7293	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)))
135		df-s4 14563	. . . . . . . . . . 11 ⊢ ⟨“𝑊𝑋𝑌𝑍”⟩ = (⟨“𝑊𝑋𝑌”⟩ ++ ⟨“𝑍”⟩)
136	135	fveq1i 6775	. . . . . . . . . 10 ⊢ (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) = ((⟨“𝑊𝑋𝑌”⟩ ++ ⟨“𝑍”⟩)‘𝑖)
137	20	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑊 ∈ 𝑃)
138	21	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑋 ∈ 𝑃)
139	22	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑌 ∈ 𝑃)
140	137, 138, 139	s3cld 14585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ⟨“𝑊𝑋𝑌”⟩ ∈ Word 𝑃)
141	23	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑍 ∈ 𝑃)
142	141	s1cld 14308	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ⟨“𝑍”⟩ ∈ Word 𝑃)
143	123, 111	eleqtrrdi 2850	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑖 ∈ (0..^(♯‘⟨“𝑊𝑋𝑌”⟩)))
144		ccatval1 14281	. . . . . . . . . . 11 ⊢ ((⟨“𝑊𝑋𝑌”⟩ ∈ Word 𝑃 ∧ ⟨“𝑍”⟩ ∈ Word 𝑃 ∧ 𝑖 ∈ (0..^(♯‘⟨“𝑊𝑋𝑌”⟩))) → ((⟨“𝑊𝑋𝑌”⟩ ++ ⟨“𝑍”⟩)‘𝑖) = (⟨“𝑊𝑋𝑌”⟩‘𝑖))
145	140, 142, 143, 144	syl3anc 1370	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((⟨“𝑊𝑋𝑌”⟩ ++ ⟨“𝑍”⟩)‘𝑖) = (⟨“𝑊𝑋𝑌”⟩‘𝑖))
146	136, 145	eqtrid 2790	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) = (⟨“𝑊𝑋𝑌”⟩‘𝑖))
147	135	fveq1i 6775	. . . . . . . . . 10 ⊢ (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗) = ((⟨“𝑊𝑋𝑌”⟩ ++ ⟨“𝑍”⟩)‘𝑗)
148	129, 111	eleqtrrdi 2850	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → 𝑗 ∈ (0..^(♯‘⟨“𝑊𝑋𝑌”⟩)))
149		ccatval1 14281	. . . . . . . . . . 11 ⊢ ((⟨“𝑊𝑋𝑌”⟩ ∈ Word 𝑃 ∧ ⟨“𝑍”⟩ ∈ Word 𝑃 ∧ 𝑗 ∈ (0..^(♯‘⟨“𝑊𝑋𝑌”⟩))) → ((⟨“𝑊𝑋𝑌”⟩ ++ ⟨“𝑍”⟩)‘𝑗) = (⟨“𝑊𝑋𝑌”⟩‘𝑗))
150	140, 142, 148, 149	syl3anc 1370	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((⟨“𝑊𝑋𝑌”⟩ ++ ⟨“𝑍”⟩)‘𝑗) = (⟨“𝑊𝑋𝑌”⟩‘𝑗))
151	147, 150	eqtrid 2790	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗) = (⟨“𝑊𝑋𝑌”⟩‘𝑗))
152	146, 151	oveq12d 7293	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗)))
153	134, 152	eqeq12d 2754	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗)) ↔ ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗))))
154	153	imbi2d 341	. . . . . 6 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^3) ∧ 𝑗 ∈ (0..^3))) → ((𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ (𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗)))))
155	154	2ralbidva 3128	. . . . 5 ⊢ (𝜑 → (∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶”⟩‘𝑖) − (⟨“𝐴𝐵𝐶”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌”⟩‘𝑖) − (⟨“𝑊𝑋𝑌”⟩‘𝑗)))))
156	105, 114, 155	3bitr4rd 312	. . . 4 ⊢ (𝜑 → (∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ↔ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝑊𝑋𝑌”⟩))
157		fzo0to3tp 13473	. . . . . 6 ⊢ (0..^3) = {0, 1, 2}
158	157	raleqi 3346	. . . . 5 ⊢ (∀𝑖 ∈ (0..^3)(𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ ∀𝑖 ∈ {0, 1, 2} (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))))
159		3pos 12078	. . . . . . . . . 10 ⊢ 0 < 3
160		breq1 5077	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (𝑖 < 3 ↔ 0 < 3))
161	159, 160	mpbiri 257	. . . . . . . . 9 ⊢ (𝑖 = 0 → 𝑖 < 3)
162	161	adantl 482	. . . . . . . 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 6774	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) = (⟨“𝐴𝐵𝐶𝐷”⟩‘0))
166		s4fv0 14608	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑃 → (⟨“𝐴𝐵𝐶𝐷”⟩‘0) = 𝐴)
167	9, 166	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶𝐷”⟩‘0) = 𝐴)
168	165, 167	sylan9eqr 2800	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 0) → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) = 𝐴)
169		s4fv3 14611	. . . . . . . . . . 11 ⊢ (𝐷 ∈ 𝑃 → (⟨“𝐴𝐵𝐶𝐷”⟩‘3) = 𝐷)
170	12, 169	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶𝐷”⟩‘3) = 𝐷)
171	170	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 0) → (⟨“𝐴𝐵𝐶𝐷”⟩‘3) = 𝐷)
172	168, 171	oveq12d 7293	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 0) → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = (𝐴 − 𝐷))
173		fveq2 6774	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) = (⟨“𝑊𝑋𝑌𝑍”⟩‘0))
174		s4fv0 14608	. . . . . . . . . . 11 ⊢ (𝑊 ∈ 𝑃 → (⟨“𝑊𝑋𝑌𝑍”⟩‘0) = 𝑊)
175	20, 174	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝑊𝑋𝑌𝑍”⟩‘0) = 𝑊)
176	173, 175	sylan9eqr 2800	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 0) → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) = 𝑊)
177		s4fv3 14611	. . . . . . . . . . 11 ⊢ (𝑍 ∈ 𝑃 → (⟨“𝑊𝑋𝑌𝑍”⟩‘3) = 𝑍)
178	23, 177	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝑊𝑋𝑌𝑍”⟩‘3) = 𝑍)
179	178	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 0) → (⟨“𝑊𝑋𝑌𝑍”⟩‘3) = 𝑍)
180	176, 179	oveq12d 7293	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 0) → ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) = (𝑊 − 𝑍))
181	172, 180	eqeq12d 2754	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = 0) → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) ↔ (𝐴 − 𝐷) = (𝑊 − 𝑍)))
182	164, 181	bitr3d 280	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ (𝐴 − 𝐷) = (𝑊 − 𝑍)))
183		1lt3 12146	. . . . . . . . . 10 ⊢ 1 < 3
184		breq1 5077	. . . . . . . . . 10 ⊢ (𝑖 = 1 → (𝑖 < 3 ↔ 1 < 3))
185	183, 184	mpbiri 257	. . . . . . . . 9 ⊢ (𝑖 = 1 → 𝑖 < 3)
186	185	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 1) → 𝑖 < 3)
187	186, 163	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = 1) → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) ↔ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))))
188		fveq2 6774	. . . . . . . . . 10 ⊢ (𝑖 = 1 → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) = (⟨“𝐴𝐵𝐶𝐷”⟩‘1))
189		s4fv1 14609	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑃 → (⟨“𝐴𝐵𝐶𝐷”⟩‘1) = 𝐵)
190	10, 189	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶𝐷”⟩‘1) = 𝐵)
191	188, 190	sylan9eqr 2800	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 1) → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) = 𝐵)
192	170	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 1) → (⟨“𝐴𝐵𝐶𝐷”⟩‘3) = 𝐷)
193	191, 192	oveq12d 7293	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 1) → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = (𝐵 − 𝐷))
194		fveq2 6774	. . . . . . . . . 10 ⊢ (𝑖 = 1 → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) = (⟨“𝑊𝑋𝑌𝑍”⟩‘1))
195		s4fv1 14609	. . . . . . . . . . 11 ⊢ (𝑋 ∈ 𝑃 → (⟨“𝑊𝑋𝑌𝑍”⟩‘1) = 𝑋)
196	21, 195	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝑊𝑋𝑌𝑍”⟩‘1) = 𝑋)
197	194, 196	sylan9eqr 2800	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 1) → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) = 𝑋)
198	178	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 1) → (⟨“𝑊𝑋𝑌𝑍”⟩‘3) = 𝑍)
199	197, 198	oveq12d 7293	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 1) → ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) = (𝑋 − 𝑍))
200	193, 199	eqeq12d 2754	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = 1) → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) ↔ (𝐵 − 𝐷) = (𝑋 − 𝑍)))
201	187, 200	bitr3d 280	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 = 1) → ((𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ (𝐵 − 𝐷) = (𝑋 − 𝑍)))
202		2lt3 12145	. . . . . . . . . 10 ⊢ 2 < 3
203		breq1 5077	. . . . . . . . . 10 ⊢ (𝑖 = 2 → (𝑖 < 3 ↔ 2 < 3))
204	202, 203	mpbiri 257	. . . . . . . . 9 ⊢ (𝑖 = 2 → 𝑖 < 3)
205	204	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 2) → 𝑖 < 3)
206	205, 163	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = 2) → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) ↔ (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))))
207		fveq2 6774	. . . . . . . . . 10 ⊢ (𝑖 = 2 → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) = (⟨“𝐴𝐵𝐶𝐷”⟩‘2))
208		s4fv2 14610	. . . . . . . . . . 11 ⊢ (𝐶 ∈ 𝑃 → (⟨“𝐴𝐵𝐶𝐷”⟩‘2) = 𝐶)
209	11, 208	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶𝐷”⟩‘2) = 𝐶)
210	207, 209	sylan9eqr 2800	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 2) → (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) = 𝐶)
211	170	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 2) → (⟨“𝐴𝐵𝐶𝐷”⟩‘3) = 𝐷)
212	210, 211	oveq12d 7293	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 2) → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = (𝐶 − 𝐷))
213		fveq2 6774	. . . . . . . . . 10 ⊢ (𝑖 = 2 → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) = (⟨“𝑊𝑋𝑌𝑍”⟩‘2))
214		s4fv2 14610	. . . . . . . . . . 11 ⊢ (𝑌 ∈ 𝑃 → (⟨“𝑊𝑋𝑌𝑍”⟩‘2) = 𝑌)
215	22, 214	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (⟨“𝑊𝑋𝑌𝑍”⟩‘2) = 𝑌)
216	213, 215	sylan9eqr 2800	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 2) → (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) = 𝑌)
217	178	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 = 2) → (⟨“𝑊𝑋𝑌𝑍”⟩‘3) = 𝑍)
218	216, 217	oveq12d 7293	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 2) → ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) = (𝑌 − 𝑍))
219	212, 218	eqeq12d 2754	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = 2) → (((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)) ↔ (𝐶 − 𝐷) = (𝑌 − 𝑍)))
220	206, 219	bitr3d 280	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 = 2) → ((𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ (𝐶 − 𝐷) = (𝑌 − 𝑍)))
221		0red 10978	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℝ)
222		1red 10976	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℝ)
223		2re 12047	. . . . . . 7 ⊢ 2 ∈ ℝ
224	223	a1i 11	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℝ)
225	182, 201, 220, 221, 222, 224	raltpd 4717	. . . . 5 ⊢ (𝜑 → (∀𝑖 ∈ {0, 1, 2} (𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍))))
226	158, 225	bitrid 282	. . . 4 ⊢ (𝜑 → (∀𝑖 ∈ (0..^3)(𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3))) ↔ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍))))
227	156, 226	anbi12d 631	. . 3 ⊢ (𝜑 → ((∀𝑖 ∈ (0..^3)∀𝑗 ∈ (0..^3)(𝑖 < 𝑗 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘𝑗)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘𝑗))) ∧ ∀𝑖 ∈ (0..^3)(𝑖 < 3 → ((⟨“𝐴𝐵𝐶𝐷”⟩‘𝑖) − (⟨“𝐴𝐵𝐶𝐷”⟩‘3)) = ((⟨“𝑊𝑋𝑌𝑍”⟩‘𝑖) − (⟨“𝑊𝑋𝑌𝑍”⟩‘3)))) ↔ (⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝑊𝑋𝑌”⟩ ∧ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍)))))
228	95, 227	bitrid 282	. 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 396 ∧ w3a 1086 = wceq 1539 ⊤wtru 1540 ⊥wfal 1551 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∪ cun 3885 ⊆ wss 3887 ∅c0 4256 {csn 4561 {ctp 4565 class class class wbr 5074 dom cdm 5589 ⟶wf 6429 ‘cfv 6433 (class class class)co 7275 ℝcr 10870 0cc0 10871 1c1 10872 + caddc 10874 < clt 11009 ℕcn 11973 2c2 12028 3c3 12029 4c4 12030 ℕ₀cn0 12233 ℤ_≥cuz 12582 ..^cfzo 13382 ♯chash 14044 Word cword 14217 ++ cconcat 14273 ⟨“cs1 14300 ⟨“cs3 14555 ⟨“cs4 14556 Basecbs 16912 distcds 16971 TarskiGcstrkg 26788 Itvcitv 26794 cgrGccgrg 26871

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-tp 4566 df-op 4568 df-uni 4840 df-int 4880 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-1st 7831 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-er 8498 df-pm 8618 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-card 9697 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-nn 11974 df-2 12036 df-3 12037 df-4 12038 df-n0 12234 df-z 12320 df-uz 12583 df-fz 13240 df-fzo 13383 df-hash 14045 df-word 14218 df-concat 14274 df-s1 14301 df-s2 14561 df-s3 14562 df-s4 14563 df-trkgc 26809 df-trkgcb 26811 df-trkg 26814 df-cgrg 26872

This theorem is referenced by: cgrg3col4 27214

W3C validator