Theorem istrkgl

Description: Building lines from the segment property. (Contributed by Thierry Arnoux, 14-Mar-2019)

	Ref	Expression
Hypotheses	istrkg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	istrkg.d	⊢ − = ( dist ‘ 𝐺 )
	istrkg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
Assertion	istrkgl	⊢ ( 𝐺 ∈ { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) } ↔ ( 𝐺 ∈ V ∧ ( LineG ‘ 𝐺 ) = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		istrkg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		istrkg.d	⊢ − = ( dist ‘ 𝐺 )
3		istrkg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		simpl	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → 𝑝 = 𝑃 )
5	4	eqcomd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → 𝑃 = 𝑝 )
6	5	adantr	⊢ ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) → 𝑃 = 𝑝 )
7	6	difeq1d	⊢ ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) → ( 𝑃 ∖ { 𝑥 } ) = ( 𝑝 ∖ { 𝑥 } ) )
8		simpr	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → 𝑖 = 𝐼 )
9	8	eqcomd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → 𝐼 = 𝑖 )
10	9	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑥 𝐼 𝑦 ) = ( 𝑥 𝑖 𝑦 ) )
11	10	eleq2d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ↔ 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ) )
12	9	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑧 𝐼 𝑦 ) = ( 𝑧 𝑖 𝑦 ) )
13	12	eleq2d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ↔ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ) )
14	9	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑥 𝐼 𝑧 ) = ( 𝑥 𝑖 𝑧 ) )
15	14	eleq2d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ↔ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) )
16	11 13 15	3orbi123d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ↔ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) )
17	5 16	rabeqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } = { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } )
18	17	adantr	⊢ ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ) → { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } = { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } )
19	5 7 18	mpoeq123dva	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) = ( 𝑥 ∈ 𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) )
20	19	eqeq2d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ↔ ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ) )
21	1 3 20	sbcie2s	⊢ ( 𝑓 = 𝐺 → ( [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ↔ ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ) )
22		fveqeq2	⊢ ( 𝑓 = 𝐺 → ( ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ↔ ( LineG ‘ 𝐺 ) = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ) )
23	21 22	bitrd	⊢ ( 𝑓 = 𝐺 → ( [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ↔ ( LineG ‘ 𝐺 ) = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ) )
24		eqid	⊢ { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) } = { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) }
25	23 24	elab4g	⊢ ( 𝐺 ∈ { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) } ↔ ( 𝐺 ∈ V ∧ ( LineG ‘ 𝐺 ) = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ) )