Theorem istrkgl 28778

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

Hypotheses

Ref	Expression
istrkg.p	⊢ 𝑃 = (Base‘𝐺)
istrkg.d	⊢ − = (dist‘𝐺)
istrkg.i	⊢ 𝐼 = (Itv‘𝐺)

Assertion

Ref	Expression
istrkgl	⊢ (𝐺 ∈ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})} ↔ (𝐺 ∈ V ∧ (LineG‘𝐺) = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})))

Distinct variable groups:   𝑓,𝑖,𝑝,𝐺   𝑥,𝑓,𝑦,𝑧,𝐼,𝑖,𝑝   𝑃,𝑓,𝑖,𝑝,𝑥,𝑦,𝑧   − ,𝑓,𝑖,𝑝,𝑥,𝑦,𝑧

Allowed substitution hints:   𝐺(𝑥, 𝑦, 𝑧)

Proof of Theorem istrkgl

Step	Hyp	Ref	Expression
1		istrkg.p	. . . 4 ⊢ 𝑃 = (Base‘𝐺)
2		istrkg.i	. . . 4 ⊢ 𝐼 = (Itv‘𝐺)
3		simpl 488	. . . . . 6 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → 𝑝 = 𝑃)
4	3	difeq1d 4080	. . . . . 6 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑝 ∖ {𝑥}) = (𝑃 ∖ {𝑥}))
5		simpr 490	. . . . . . . . . 10 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → 𝑖 = 𝐼)
6	5	oveqd 7436	. . . . . . . . 9 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑥𝑖𝑦) = (𝑥𝐼𝑦))
7	6	eleq2d 2851	. . . . . . . 8 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑧 ∈ (𝑥𝑖𝑦) ↔ 𝑧 ∈ (𝑥𝐼𝑦)))
8	5	oveqd 7436	. . . . . . . . 9 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑧𝑖𝑦) = (𝑧𝐼𝑦))
9	8	eleq2d 2851	. . . . . . . 8 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑥 ∈ (𝑧𝑖𝑦) ↔ 𝑥 ∈ (𝑧𝐼𝑦)))
10	5	oveqd 7436	. . . . . . . . 9 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑥𝑖𝑧) = (𝑥𝐼𝑧))
11	10	eleq2d 2851	. . . . . . . 8 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑦 ∈ (𝑥𝑖𝑧) ↔ 𝑦 ∈ (𝑥𝐼𝑧)))
12	7, 9, 11	3orbi123d 1463	. . . . . . 7 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → ((𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)) ↔ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))
13	3, 12	rabeqbidv 3436	. . . . . 6 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))} = {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})
14	3, 4, 13	mpoeq123dv 7494	. . . . 5 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}) = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))}))
15	14	eqeq2d 2776	. . . 4 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → ((LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}) ↔ (LineG‘𝑓) = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})))
16	1, 2, 15	sbcie2s 17243	. . 3 ⊢ (𝑓 = 𝐺 → ([(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}) ↔ (LineG‘𝑓) = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})))
17		fveqeq2 6894	. . 3 ⊢ (𝑓 = 𝐺 → ((LineG‘𝑓) = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))}) ↔ (LineG‘𝐺) = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})))
18	16, 17	bitrd 282	. 2 ⊢ (𝑓 = 𝐺 → ([(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}) ↔ (LineG‘𝐺) = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})))
19		eqid 2765	. 2 ⊢ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})} = {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}
20	18, 19	elab4g 3644	1 ⊢ (𝐺 ∈ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})} ↔ (𝐺 ∈ V ∧ (LineG‘𝐺) = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∨ w3o 1102   = wceq 1570   ∈ wcel 2146  {cab 2743  {crab 3418  Vcvv 3457  [wsbc 3746   ∖ cdif 3903  {csn 4591  ‘cfv 6540  (class class class)co 7419   ∈ cmpo 7421  Basecbs 17291  distcds 17341  Itvcitv 28753  LineGclng 28754

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-nul 5271

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-rab 3419  df-v 3459  df-sbc 3747  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-oprab 7423  df-mpo 7424

This theorem is used by:  tglng  28866  f1otrg  29275  eengtrkg  29391