Theorem istrkgl 28144

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 482	. . . . . 6 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → 𝑝 = 𝑃)
4	3	difeq1d 4121	. . . . . 6 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑝 ∖ {𝑥}) = (𝑃 ∖ {𝑥}))
5		simpr 484	. . . . . . . . . 10 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → 𝑖 = 𝐼)
6	5	oveqd 7429	. . . . . . . . 9 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑥𝑖𝑦) = (𝑥𝐼𝑦))
7	6	eleq2d 2818	. . . . . . . 8 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑧 ∈ (𝑥𝑖𝑦) ↔ 𝑧 ∈ (𝑥𝐼𝑦)))
8	5	oveqd 7429	. . . . . . . . 9 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑧𝑖𝑦) = (𝑧𝐼𝑦))
9	8	eleq2d 2818	. . . . . . . 8 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑥 ∈ (𝑧𝑖𝑦) ↔ 𝑥 ∈ (𝑧𝐼𝑦)))
10	5	oveqd 7429	. . . . . . . . 9 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑥𝑖𝑧) = (𝑥𝐼𝑧))
11	10	eleq2d 2818	. . . . . . . 8 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑦 ∈ (𝑥𝑖𝑧) ↔ 𝑦 ∈ (𝑥𝐼𝑧)))
12	7, 9, 11	3orbi123d 1434	. . . . . . 7 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → ((𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)) ↔ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))
13	3, 12	rabeqbidv 3448	. . . . . 6 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))} = {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})
14	3, 4, 13	mpoeq123dv 7487	. . . . 5 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}) = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))}))
15	14	eqeq2d 2742	. . . 4 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → ((LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}) ↔ (LineG‘𝑓) = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})))
16	1, 2, 15	sbcie2s 17101	. . 3 ⊢ (𝑓 = 𝐺 → ([(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}) ↔ (LineG‘𝑓) = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})))
17		fveqeq2 6900	. . 3 ⊢ (𝑓 = 𝐺 → ((LineG‘𝑓) = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))}) ↔ (LineG‘𝐺) = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})))
18	16, 17	bitrd 279	. 2 ⊢ (𝑓 = 𝐺 → ([(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}) ↔ (LineG‘𝐺) = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})))
19		eqid 2731	. 2 ⊢ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})} = {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}
20	18, 19	elab4g 3673	1 ⊢ (𝐺 ∈ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})} ↔ (𝐺 ∈ V ∧ (LineG‘𝐺) = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})))

Syntax hints:   ↔ wb 205   ∧ wa 395   ∨ w3o 1085   = wceq 1540   ∈ wcel 2105  {cab 2708  {crab 3431  Vcvv 3473  [wsbc 3777   ∖ cdif 3945  {csn 4628  ‘cfv 6543  (class class class)co 7412   ∈ cmpo 7414  Basecbs 17151  distcds 17213  Itvcitv 28119  LineGclng 28120

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-rab 3432  df-v 3475  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7415  df-oprab 7416  df-mpo 7417

This theorem is referenced by:  tglng  28232  f1otrg  28557  eengtrkg  28679