Theorem axtgupdim2ALTV

Description: Alternate version of axtgupdim2 . (Contributed by Thierry Arnoux, 29-May-2019) (New usage is discouraged.)

	Ref	Expression
Hypotheses	istrkg2d.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	istrkg2d.d	⊢ − = ( dist ‘ 𝐺 )
	istrkg2d.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	axtgupdim2ALTV.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	axtgupdim2ALTV.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
	axtgupdim2ALTV.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
	axtgupdim2ALTV.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
	axtgupdim2ALTV.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
	axtgupdim2ALTV.0	⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
	axtgupdim2ALTV.1	⊢ ( 𝜑 → ( 𝑋 − 𝑈 ) = ( 𝑋 − 𝑉 ) )
	axtgupdim2ALTV.2	⊢ ( 𝜑 → ( 𝑌 − 𝑈 ) = ( 𝑌 − 𝑉 ) )
	axtgupdim2ALTV.3	⊢ ( 𝜑 → ( 𝑍 − 𝑈 ) = ( 𝑍 − 𝑉 ) )
	axtgupdim2ALTV.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG2D )
Assertion	axtgupdim2ALTV	⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) )

Proof

Step	Hyp	Ref	Expression
1		istrkg2d.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		istrkg2d.d	⊢ − = ( dist ‘ 𝐺 )
3		istrkg2d.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		axtgupdim2ALTV.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
5		axtgupdim2ALTV.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
6		axtgupdim2ALTV.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
7		axtgupdim2ALTV.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
8		axtgupdim2ALTV.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
9		axtgupdim2ALTV.0	⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
10		axtgupdim2ALTV.1	⊢ ( 𝜑 → ( 𝑋 − 𝑈 ) = ( 𝑋 − 𝑉 ) )
11		axtgupdim2ALTV.2	⊢ ( 𝜑 → ( 𝑌 − 𝑈 ) = ( 𝑌 − 𝑉 ) )
12		axtgupdim2ALTV.3	⊢ ( 𝜑 → ( 𝑍 − 𝑈 ) = ( 𝑍 − 𝑉 ) )
13		axtgupdim2ALTV.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG2D )
14	10 11 12	3jca	⊢ ( 𝜑 → ( ( 𝑋 − 𝑈 ) = ( 𝑋 − 𝑉 ) ∧ ( 𝑌 − 𝑈 ) = ( 𝑌 − 𝑉 ) ∧ ( 𝑍 − 𝑈 ) = ( 𝑍 − 𝑉 ) ) )
15	1 2 3	istrkg2d	⊢ ( 𝐺 ∈ TarskiG2D ↔ ( 𝐺 ∈ V ∧ ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( ( 𝑥 − 𝑢 ) = ( 𝑥 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑦 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )
16	13 15	sylib	⊢ ( 𝜑 → ( 𝐺 ∈ V ∧ ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( ( 𝑥 − 𝑢 ) = ( 𝑥 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑦 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )
17	16	simprrd	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( ( 𝑥 − 𝑢 ) = ( 𝑥 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑦 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) )
18		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 − 𝑢 ) = ( 𝑋 − 𝑢 ) )
19		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 − 𝑣 ) = ( 𝑋 − 𝑣 ) )
20	18 19	eqeq12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 − 𝑢 ) = ( 𝑥 − 𝑣 ) ↔ ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ) )
21	20	3anbi1d	⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑥 − 𝑢 ) = ( 𝑥 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑦 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ↔ ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑦 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ) )
22	21	anbi1d	⊢ ( 𝑥 = 𝑋 → ( ( ( ( 𝑥 − 𝑢 ) = ( 𝑥 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑦 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) ↔ ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑦 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) ) )
23		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐼 𝑦 ) = ( 𝑋 𝐼 𝑦 ) )
24	23	eleq2d	⊢ ( 𝑥 = 𝑋 → ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ↔ 𝑧 ∈ ( 𝑋 𝐼 𝑦 ) ) )
25		eleq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ↔ 𝑋 ∈ ( 𝑧 𝐼 𝑦 ) ) )
26		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐼 𝑧 ) = ( 𝑋 𝐼 𝑧 ) )
27	26	eleq2d	⊢ ( 𝑥 = 𝑋 → ( 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ↔ 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ) )
28	24 25 27	3orbi123d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ↔ ( 𝑧 ∈ ( 𝑋 𝐼 𝑦 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ) ) )
29	22 28	imbi12d	⊢ ( 𝑥 = 𝑋 → ( ( ( ( ( 𝑥 − 𝑢 ) = ( 𝑥 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑦 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ( ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑦 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑋 𝐼 𝑦 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ) ) ) )
30	29	2ralbidv	⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( ( 𝑥 − 𝑢 ) = ( 𝑥 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑦 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑦 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑋 𝐼 𝑦 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ) ) ) )
31		oveq1	⊢ ( 𝑦 = 𝑌 → ( 𝑦 − 𝑢 ) = ( 𝑌 − 𝑢 ) )
32		oveq1	⊢ ( 𝑦 = 𝑌 → ( 𝑦 − 𝑣 ) = ( 𝑌 − 𝑣 ) )
33	31 32	eqeq12d	⊢ ( 𝑦 = 𝑌 → ( ( 𝑦 − 𝑢 ) = ( 𝑦 − 𝑣 ) ↔ ( 𝑌 − 𝑢 ) = ( 𝑌 − 𝑣 ) ) )
34	33	3anbi2d	⊢ ( 𝑦 = 𝑌 → ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑦 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ↔ ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑢 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ) )
35	34	anbi1d	⊢ ( 𝑦 = 𝑌 → ( ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑦 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) ↔ ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑢 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) ) )
36		oveq2	⊢ ( 𝑦 = 𝑌 → ( 𝑋 𝐼 𝑦 ) = ( 𝑋 𝐼 𝑌 ) )
37	36	eleq2d	⊢ ( 𝑦 = 𝑌 → ( 𝑧 ∈ ( 𝑋 𝐼 𝑦 ) ↔ 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ) )
38		oveq2	⊢ ( 𝑦 = 𝑌 → ( 𝑧 𝐼 𝑦 ) = ( 𝑧 𝐼 𝑌 ) )
39	38	eleq2d	⊢ ( 𝑦 = 𝑌 → ( 𝑋 ∈ ( 𝑧 𝐼 𝑦 ) ↔ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ) )
40		eleq1	⊢ ( 𝑦 = 𝑌 → ( 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ↔ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) )
41	37 39 40	3orbi123d	⊢ ( 𝑦 = 𝑌 → ( ( 𝑧 ∈ ( 𝑋 𝐼 𝑦 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ) ↔ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ) )
42	35 41	imbi12d	⊢ ( 𝑦 = 𝑌 → ( ( ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑦 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑋 𝐼 𝑦 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ) ) ↔ ( ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑢 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ) ) )
43	42	2ralbidv	⊢ ( 𝑦 = 𝑌 → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑦 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑋 𝐼 𝑦 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ) ) ↔ ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑢 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ) ) )
44		oveq1	⊢ ( 𝑧 = 𝑍 → ( 𝑧 − 𝑢 ) = ( 𝑍 − 𝑢 ) )
45		oveq1	⊢ ( 𝑧 = 𝑍 → ( 𝑧 − 𝑣 ) = ( 𝑍 − 𝑣 ) )
46	44 45	eqeq12d	⊢ ( 𝑧 = 𝑍 → ( ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ↔ ( 𝑍 − 𝑢 ) = ( 𝑍 − 𝑣 ) ) )
47	46	3anbi3d	⊢ ( 𝑧 = 𝑍 → ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑢 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ↔ ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑢 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑍 − 𝑢 ) = ( 𝑍 − 𝑣 ) ) ) )
48	47	anbi1d	⊢ ( 𝑧 = 𝑍 → ( ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑢 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) ↔ ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑢 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑍 − 𝑢 ) = ( 𝑍 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) ) )
49		eleq1	⊢ ( 𝑧 = 𝑍 → ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ↔ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) )
50		oveq1	⊢ ( 𝑧 = 𝑍 → ( 𝑧 𝐼 𝑌 ) = ( 𝑍 𝐼 𝑌 ) )
51	50	eleq2d	⊢ ( 𝑧 = 𝑍 → ( 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ↔ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ) )
52		oveq2	⊢ ( 𝑧 = 𝑍 → ( 𝑋 𝐼 𝑧 ) = ( 𝑋 𝐼 𝑍 ) )
53	52	eleq2d	⊢ ( 𝑧 = 𝑍 → ( 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ↔ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) )
54	49 51 53	3orbi123d	⊢ ( 𝑧 = 𝑍 → ( ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ↔ ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) )
55	48 54	imbi12d	⊢ ( 𝑧 = 𝑍 → ( ( ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑢 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ) ↔ ( ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑢 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑍 − 𝑢 ) = ( 𝑍 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) ) )
56	55	2ralbidv	⊢ ( 𝑧 = 𝑍 → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑢 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ) ↔ ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑢 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑍 − 𝑢 ) = ( 𝑍 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) ) )
57	30 43 56	rspc3v	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ) → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( ( 𝑥 − 𝑢 ) = ( 𝑥 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑦 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) → ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑢 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑍 − 𝑢 ) = ( 𝑍 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) ) )
58	4 5 6 57	syl3anc	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( ( 𝑥 − 𝑢 ) = ( 𝑥 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑦 − 𝑣 ) ∧ ( 𝑧 − 𝑢 ) = ( 𝑧 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) → ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑢 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑍 − 𝑢 ) = ( 𝑍 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) ) )
59	17 58	mpd	⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑢 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑍 − 𝑢 ) = ( 𝑍 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) )
60		oveq2	⊢ ( 𝑢 = 𝑈 → ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑈 ) )
61	60	eqeq1d	⊢ ( 𝑢 = 𝑈 → ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ↔ ( 𝑋 − 𝑈 ) = ( 𝑋 − 𝑣 ) ) )
62		oveq2	⊢ ( 𝑢 = 𝑈 → ( 𝑌 − 𝑢 ) = ( 𝑌 − 𝑈 ) )
63	62	eqeq1d	⊢ ( 𝑢 = 𝑈 → ( ( 𝑌 − 𝑢 ) = ( 𝑌 − 𝑣 ) ↔ ( 𝑌 − 𝑈 ) = ( 𝑌 − 𝑣 ) ) )
64		oveq2	⊢ ( 𝑢 = 𝑈 → ( 𝑍 − 𝑢 ) = ( 𝑍 − 𝑈 ) )
65	64	eqeq1d	⊢ ( 𝑢 = 𝑈 → ( ( 𝑍 − 𝑢 ) = ( 𝑍 − 𝑣 ) ↔ ( 𝑍 − 𝑈 ) = ( 𝑍 − 𝑣 ) ) )
66	61 63 65	3anbi123d	⊢ ( 𝑢 = 𝑈 → ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑢 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑍 − 𝑢 ) = ( 𝑍 − 𝑣 ) ) ↔ ( ( 𝑋 − 𝑈 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑈 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑍 − 𝑈 ) = ( 𝑍 − 𝑣 ) ) ) )
67		neeq1	⊢ ( 𝑢 = 𝑈 → ( 𝑢 ≠ 𝑣 ↔ 𝑈 ≠ 𝑣 ) )
68	66 67	anbi12d	⊢ ( 𝑢 = 𝑈 → ( ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑢 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑍 − 𝑢 ) = ( 𝑍 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) ↔ ( ( ( 𝑋 − 𝑈 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑈 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑍 − 𝑈 ) = ( 𝑍 − 𝑣 ) ) ∧ 𝑈 ≠ 𝑣 ) ) )
69	68	imbi1d	⊢ ( 𝑢 = 𝑈 → ( ( ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑢 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑍 − 𝑢 ) = ( 𝑍 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) ↔ ( ( ( ( 𝑋 − 𝑈 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑈 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑍 − 𝑈 ) = ( 𝑍 − 𝑣 ) ) ∧ 𝑈 ≠ 𝑣 ) → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) ) )
70		oveq2	⊢ ( 𝑣 = 𝑉 → ( 𝑋 − 𝑣 ) = ( 𝑋 − 𝑉 ) )
71	70	eqeq2d	⊢ ( 𝑣 = 𝑉 → ( ( 𝑋 − 𝑈 ) = ( 𝑋 − 𝑣 ) ↔ ( 𝑋 − 𝑈 ) = ( 𝑋 − 𝑉 ) ) )
72		oveq2	⊢ ( 𝑣 = 𝑉 → ( 𝑌 − 𝑣 ) = ( 𝑌 − 𝑉 ) )
73	72	eqeq2d	⊢ ( 𝑣 = 𝑉 → ( ( 𝑌 − 𝑈 ) = ( 𝑌 − 𝑣 ) ↔ ( 𝑌 − 𝑈 ) = ( 𝑌 − 𝑉 ) ) )
74		oveq2	⊢ ( 𝑣 = 𝑉 → ( 𝑍 − 𝑣 ) = ( 𝑍 − 𝑉 ) )
75	74	eqeq2d	⊢ ( 𝑣 = 𝑉 → ( ( 𝑍 − 𝑈 ) = ( 𝑍 − 𝑣 ) ↔ ( 𝑍 − 𝑈 ) = ( 𝑍 − 𝑉 ) ) )
76	71 73 75	3anbi123d	⊢ ( 𝑣 = 𝑉 → ( ( ( 𝑋 − 𝑈 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑈 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑍 − 𝑈 ) = ( 𝑍 − 𝑣 ) ) ↔ ( ( 𝑋 − 𝑈 ) = ( 𝑋 − 𝑉 ) ∧ ( 𝑌 − 𝑈 ) = ( 𝑌 − 𝑉 ) ∧ ( 𝑍 − 𝑈 ) = ( 𝑍 − 𝑉 ) ) ) )
77		neeq2	⊢ ( 𝑣 = 𝑉 → ( 𝑈 ≠ 𝑣 ↔ 𝑈 ≠ 𝑉 ) )
78	76 77	anbi12d	⊢ ( 𝑣 = 𝑉 → ( ( ( ( 𝑋 − 𝑈 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑈 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑍 − 𝑈 ) = ( 𝑍 − 𝑣 ) ) ∧ 𝑈 ≠ 𝑣 ) ↔ ( ( ( 𝑋 − 𝑈 ) = ( 𝑋 − 𝑉 ) ∧ ( 𝑌 − 𝑈 ) = ( 𝑌 − 𝑉 ) ∧ ( 𝑍 − 𝑈 ) = ( 𝑍 − 𝑉 ) ) ∧ 𝑈 ≠ 𝑉 ) ) )
79	78	imbi1d	⊢ ( 𝑣 = 𝑉 → ( ( ( ( ( 𝑋 − 𝑈 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑈 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑍 − 𝑈 ) = ( 𝑍 − 𝑣 ) ) ∧ 𝑈 ≠ 𝑣 ) → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) ↔ ( ( ( ( 𝑋 − 𝑈 ) = ( 𝑋 − 𝑉 ) ∧ ( 𝑌 − 𝑈 ) = ( 𝑌 − 𝑉 ) ∧ ( 𝑍 − 𝑈 ) = ( 𝑍 − 𝑉 ) ) ∧ 𝑈 ≠ 𝑉 ) → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) ) )
80	69 79	rspc2v	⊢ ( ( 𝑈 ∈ 𝑃 ∧ 𝑉 ∈ 𝑃 ) → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑢 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑍 − 𝑢 ) = ( 𝑍 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) → ( ( ( ( 𝑋 − 𝑈 ) = ( 𝑋 − 𝑉 ) ∧ ( 𝑌 − 𝑈 ) = ( 𝑌 − 𝑉 ) ∧ ( 𝑍 − 𝑈 ) = ( 𝑍 − 𝑉 ) ) ∧ 𝑈 ≠ 𝑉 ) → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) ) )
81	7 8 80	syl2anc	⊢ ( 𝜑 → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( ( 𝑋 − 𝑢 ) = ( 𝑋 − 𝑣 ) ∧ ( 𝑌 − 𝑢 ) = ( 𝑌 − 𝑣 ) ∧ ( 𝑍 − 𝑢 ) = ( 𝑍 − 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) → ( ( ( ( 𝑋 − 𝑈 ) = ( 𝑋 − 𝑉 ) ∧ ( 𝑌 − 𝑈 ) = ( 𝑌 − 𝑉 ) ∧ ( 𝑍 − 𝑈 ) = ( 𝑍 − 𝑉 ) ) ∧ 𝑈 ≠ 𝑉 ) → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) ) )
82	59 81	mpd	⊢ ( 𝜑 → ( ( ( ( 𝑋 − 𝑈 ) = ( 𝑋 − 𝑉 ) ∧ ( 𝑌 − 𝑈 ) = ( 𝑌 − 𝑉 ) ∧ ( 𝑍 − 𝑈 ) = ( 𝑍 − 𝑉 ) ) ∧ 𝑈 ≠ 𝑉 ) → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) )
83	14 9 82	mp2and	⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) )