Theorem 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	⊢ 𝑃 = ( 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	tgcgr4	⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ∼ ⟨“ 𝑊 𝑋 𝑌 𝑍 ”⟩ ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝑊 𝑋 𝑌 ”⟩ ∧ ( ( 𝐴 − 𝐷 ) = ( 𝑊 − 𝑍 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑋 − 𝑍 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝑌 − 𝑍 ) ) ) ) )

Proof

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