Theorem tglngval

Description: The line going through points X and Y . (Contributed by Thierry Arnoux, 28-Mar-2019)

	Ref	Expression
Hypotheses	tglngval.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tglngval.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tglngval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tglngval.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tglngval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	tglngval.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
	tglngval.z	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
Assertion	tglngval	⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) = { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		tglngval.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tglngval.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
3		tglngval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		tglngval.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		tglngval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
6		tglngval.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
7		tglngval.z	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
8	1 2 3	tglng	⊢ ( 𝐺 ∈ TarskiG → 𝐿 = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) )
9	4 8	syl	⊢ ( 𝜑 → 𝐿 = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) )
10	9	oveqd	⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) = ( 𝑋 ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) 𝑌 ) )
11	7	necomd	⊢ ( 𝜑 → 𝑌 ≠ 𝑋 )
12		eldifsn	⊢ ( 𝑌 ∈ ( 𝑃 ∖ { 𝑋 } ) ↔ ( 𝑌 ∈ 𝑃 ∧ 𝑌 ≠ 𝑋 ) )
13	6 11 12	sylanbrc	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑃 ∖ { 𝑋 } ) )
14	1	fvexi	⊢ 𝑃 ∈ V
15	14	rabex	⊢ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) } ∈ V
16	15	a1i	⊢ ( 𝜑 → { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) } ∈ V )
17		oveq12	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑥 𝐼 𝑦 ) = ( 𝑋 𝐼 𝑌 ) )
18	17	eleq2d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ↔ 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ) )
19		simpl	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑥 = 𝑋 )
20		simpr	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑦 = 𝑌 )
21	20	oveq2d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑧 𝐼 𝑦 ) = ( 𝑧 𝐼 𝑌 ) )
22	19 21	eleq12d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ↔ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ) )
23	19	oveq1d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑥 𝐼 𝑧 ) = ( 𝑋 𝐼 𝑧 ) )
24	20 23	eleq12d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ↔ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) )
25	18 22 24	3orbi123d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ↔ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ) )
26	25	rabbidv	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } = { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) } )
27		sneq	⊢ ( 𝑥 = 𝑋 → { 𝑥 } = { 𝑋 } )
28	27	difeq2d	⊢ ( 𝑥 = 𝑋 → ( 𝑃 ∖ { 𝑥 } ) = ( 𝑃 ∖ { 𝑋 } ) )
29		eqid	⊢ ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } )
30	26 28 29	ovmpox	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ ( 𝑃 ∖ { 𝑋 } ) ∧ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) } ∈ V ) → ( 𝑋 ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) 𝑌 ) = { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) } )
31	5 13 16 30	syl3anc	⊢ ( 𝜑 → ( 𝑋 ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) 𝑌 ) = { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) } )
32	10 31	eqtrd	⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) = { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) } )