ttgval - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ttgval		Structured version Visualization version GIF version

Theorem ttgval 28848

Description: Define a function to augment a subcomplex Hilbert space with betweenness and a line definition. (Contributed by Thierry Arnoux, 25-Mar-2019.) (Proof shortened by AV, 9-Nov-2024.)

**Hypotheses**
Ref	Expression
ttgval.n	⊢ 𝐺 = (toTG‘𝐻)
ttgval.b	⊢ 𝐵 = (Base‘𝐻)
ttgval.m	⊢ − = (-_g‘𝐻)
ttgval.s	⊢ · = ( ·_𝑠 ‘𝐻)
ttgval.i	⊢ 𝐼 = (Itv‘𝐺)

**Assertion**
Ref	Expression
ttgval	⊢ (𝐻 ∈ 𝑉 → (𝐺 = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})⟩) ∧ 𝐼 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})))

Distinct variable groups: 𝑥,𝑘,𝑦,𝑧 𝑥,𝐵,𝑦,𝑧 𝑘,𝐻,𝑥,𝑦,𝑧 𝑥,𝑉,𝑦,𝑧 𝑥, − ,𝑦,𝑧 𝑥, · ,𝑦,𝑧 Allowed substitution hints: 𝐵(𝑘) · (𝑘) 𝐺(𝑥,𝑦,𝑧,𝑘) 𝐼(𝑥,𝑦,𝑧,𝑘) − (𝑘) 𝑉(𝑘)

Proof of Theorem ttgval Dummy variables 𝑎 𝑏 𝑐 𝑖 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ttgval.n	. . . . 5 ⊢ 𝐺 = (toTG‘𝐻)
2	1	a1i 11	. . . 4 ⊢ (𝐻 ∈ 𝑉 → 𝐺 = (toTG‘𝐻))
3		elex 3457	. . . . 5 ⊢ (𝐻 ∈ 𝑉 → 𝐻 ∈ V)
4		fveq2 6817	. . . . . . . . 9 ⊢ (𝑤 = 𝐻 → (Base‘𝑤) = (Base‘𝐻))
5		ttgval.b	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝐻)
6	4, 5	eqtr4di 2784	. . . . . . . 8 ⊢ (𝑤 = 𝐻 → (Base‘𝑤) = 𝐵)
7		fveq2 6817	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝐻 → (-_g‘𝑤) = (-_g‘𝐻))
8		ttgval.m	. . . . . . . . . . . . 13 ⊢ − = (-_g‘𝐻)
9	7, 8	eqtr4di 2784	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝐻 → (-_g‘𝑤) = − )
10	9	oveqd 7358	. . . . . . . . . . 11 ⊢ (𝑤 = 𝐻 → (𝑧(-_g‘𝑤)𝑥) = (𝑧 − 𝑥))
11		fveq2 6817	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝐻 → ( ·_𝑠 ‘𝑤) = ( ·_𝑠 ‘𝐻))
12		ttgval.s	. . . . . . . . . . . . 13 ⊢ · = ( ·_𝑠 ‘𝐻)
13	11, 12	eqtr4di 2784	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝐻 → ( ·_𝑠 ‘𝑤) = · )
14		eqidd 2732	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝐻 → 𝑘 = 𝑘)
15	9	oveqd 7358	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝐻 → (𝑦(-_g‘𝑤)𝑥) = (𝑦 − 𝑥))
16	13, 14, 15	oveq123d 7362	. . . . . . . . . . 11 ⊢ (𝑤 = 𝐻 → (𝑘( ·_𝑠 ‘𝑤)(𝑦(-_g‘𝑤)𝑥)) = (𝑘 · (𝑦 − 𝑥)))
17	10, 16	eqeq12d 2747	. . . . . . . . . 10 ⊢ (𝑤 = 𝐻 → ((𝑧(-_g‘𝑤)𝑥) = (𝑘( ·_𝑠 ‘𝑤)(𝑦(-_g‘𝑤)𝑥)) ↔ (𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))))
18	17	rexbidv 3156	. . . . . . . . 9 ⊢ (𝑤 = 𝐻 → (∃𝑘 ∈ (0[,]1)(𝑧(-_g‘𝑤)𝑥) = (𝑘( ·_𝑠 ‘𝑤)(𝑦(-_g‘𝑤)𝑥)) ↔ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))))
19	6, 18	rabeqbidv 3413	. . . . . . . 8 ⊢ (𝑤 = 𝐻 → {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-_g‘𝑤)𝑥) = (𝑘( ·_𝑠 ‘𝑤)(𝑦(-_g‘𝑤)𝑥))} = {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})
20	6, 6, 19	mpoeq123dv 7416	. . . . . . 7 ⊢ (𝑤 = 𝐻 → (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-_g‘𝑤)𝑥) = (𝑘( ·_𝑠 ‘𝑤)(𝑦(-_g‘𝑤)𝑥))}) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}))
21		oveq1 7348	. . . . . . . 8 ⊢ (𝑤 = 𝐻 → (𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) = (𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩))
22	6	rabeqdv 3410	. . . . . . . . . 10 ⊢ (𝑤 = 𝐻 → {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))} = {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})
23	6, 6, 22	mpoeq123dv 7416	. . . . . . . . 9 ⊢ (𝑤 = 𝐻 → (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}))
24	23	opeq2d 4827	. . . . . . . 8 ⊢ (𝑤 = 𝐻 → ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩ = ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩)
25	21, 24	oveq12d 7359	. . . . . . 7 ⊢ (𝑤 = 𝐻 → ((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) = ((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
26	20, 25	csbeq12dv 3854	. . . . . 6 ⊢ (𝑤 = 𝐻 → ⦋(𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-_g‘𝑤)𝑥) = (𝑘( ·_𝑠 ‘𝑤)(𝑦(-_g‘𝑤)𝑥))}) / 𝑖⦌((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) = ⦋(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) / 𝑖⦌((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
27		df-ttg 28847	. . . . . 6 ⊢ toTG = (𝑤 ∈ V ↦ ⦋(𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-_g‘𝑤)𝑥) = (𝑘( ·_𝑠 ‘𝑤)(𝑦(-_g‘𝑤)𝑥))}) / 𝑖⦌((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
28		ovex 7374	. . . . . . 7 ⊢ ((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) ∈ V
29	28	csbex 5244	. . . . . 6 ⊢ ⦋(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) / 𝑖⦌((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) ∈ V
30	26, 27, 29	fvmpt 6924	. . . . 5 ⊢ (𝐻 ∈ V → (toTG‘𝐻) = ⦋(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) / 𝑖⦌((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
31	3, 30	syl 17	. . . 4 ⊢ (𝐻 ∈ 𝑉 → (toTG‘𝐻) = ⦋(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) / 𝑖⦌((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
32	5	fvexi 6831	. . . . . . 7 ⊢ 𝐵 ∈ V
33	32, 32	mpoex 8006	. . . . . 6 ⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) ∈ V
34	33	a1i 11	. . . . 5 ⊢ (𝐻 ∈ 𝑉 → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) ∈ V)
35		simpr 484	. . . . . . 7 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})) → 𝑖 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}))
36		oveq2 7349	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑥 → (𝑐 − 𝑎) = (𝑐 − 𝑥))
37		oveq2 7349	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑥 → (𝑏 − 𝑎) = (𝑏 − 𝑥))
38	37	oveq2d 7357	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑥 → (𝑘 · (𝑏 − 𝑎)) = (𝑘 · (𝑏 − 𝑥)))
39	36, 38	eqeq12d 2747	. . . . . . . . . 10 ⊢ (𝑎 = 𝑥 → ((𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎)) ↔ (𝑐 − 𝑥) = (𝑘 · (𝑏 − 𝑥))))
40	39	rexbidv 3156	. . . . . . . . 9 ⊢ (𝑎 = 𝑥 → (∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎)) ↔ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑏 − 𝑥))))
41	40	rabbidv 3402	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))} = {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑏 − 𝑥))})
42		oveq1 7348	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑦 → (𝑏 − 𝑥) = (𝑦 − 𝑥))
43	42	oveq2d 7357	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑦 → (𝑘 · (𝑏 − 𝑥)) = (𝑘 · (𝑦 − 𝑥)))
44	43	eqeq2d 2742	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑦 → ((𝑐 − 𝑥) = (𝑘 · (𝑏 − 𝑥)) ↔ (𝑐 − 𝑥) = (𝑘 · (𝑦 − 𝑥))))
45	44	rexbidv 3156	. . . . . . . . . 10 ⊢ (𝑏 = 𝑦 → (∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑏 − 𝑥)) ↔ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑦 − 𝑥))))
46	45	rabbidv 3402	. . . . . . . . 9 ⊢ (𝑏 = 𝑦 → {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑏 − 𝑥))} = {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})
47		oveq1 7348	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑧 → (𝑐 − 𝑥) = (𝑧 − 𝑥))
48	47	eqeq1d 2733	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑧 → ((𝑐 − 𝑥) = (𝑘 · (𝑦 − 𝑥)) ↔ (𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))))
49	48	rexbidv 3156	. . . . . . . . . 10 ⊢ (𝑐 = 𝑧 → (∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑦 − 𝑥)) ↔ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))))
50	49	cbvrabv 3405	. . . . . . . . 9 ⊢ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑦 − 𝑥))} = {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}
51	46, 50	eqtrdi 2782	. . . . . . . 8 ⊢ (𝑏 = 𝑦 → {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑏 − 𝑥))} = {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})
52	41, 51	cbvmpov 7436	. . . . . . 7 ⊢ (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))}) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})
53	35, 52	eqtr4di 2784	. . . . . 6 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})) → 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))}))
54		simpr 484	. . . . . . . . . 10 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))}))
55	54, 52	eqtrdi 2782	. . . . . . . . 9 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → 𝑖 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}))
56	55	opeq2d 4827	. . . . . . . 8 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → ⟨(Itv‘ndx), 𝑖⟩ = ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩)
57	56	oveq2d 7357	. . . . . . 7 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → (𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) = (𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩))
58	55	oveqd 7358	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → (𝑥𝑖𝑦) = (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦))
59	58	eleq2d 2817	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → (𝑧 ∈ (𝑥𝑖𝑦) ↔ 𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦)))
60	55	oveqd 7358	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → (𝑧𝑖𝑦) = (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦))
61	60	eleq2d 2817	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → (𝑥 ∈ (𝑧𝑖𝑦) ↔ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦)))
62	55	oveqd 7358	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → (𝑥𝑖𝑧) = (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))
63	62	eleq2d 2817	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → (𝑦 ∈ (𝑥𝑖𝑧) ↔ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧)))
64	59, 61, 63	3orbi123d 1437	. . . . . . . . . 10 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → ((𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)) ↔ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))))
65	64	rabbidv 3402	. . . . . . . . 9 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))} = {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})
66	65	mpoeq3dv 7420	. . . . . . . 8 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))}))
67	66	opeq2d 4827	. . . . . . 7 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩ = ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})⟩)
68	57, 67	oveq12d 7359	. . . . . 6 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → ((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})⟩))
69	53, 68	syldan 591	. . . . 5 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})) → ((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})⟩))
70	34, 69	csbied 3881	. . . 4 ⊢ (𝐻 ∈ 𝑉 → ⦋(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) / 𝑖⦌((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})⟩))
71	2, 31, 70	3eqtrd 2770	. . 3 ⊢ (𝐻 ∈ 𝑉 → 𝐺 = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})⟩))
72	71	fveq2d 6821	. . . . . . . . . . . 12 ⊢ (𝐻 ∈ 𝑉 → (Itv‘𝐺) = (Itv‘((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})⟩)))
73		itvid 28412	. . . . . . . . . . . . 13 ⊢ Itv = Slot (Itv‘ndx)
74		lngndxnitvndx 28416	. . . . . . . . . . . . . 14 ⊢ (LineG‘ndx) ≠ (Itv‘ndx)
75	74	necomi 2982	. . . . . . . . . . . . 13 ⊢ (Itv‘ndx) ≠ (LineG‘ndx)
76	73, 75	setsnid 17114	. . . . . . . . . . . 12 ⊢ (Itv‘(𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩)) = (Itv‘((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})⟩))
77	72, 76	eqtr4di 2784	. . . . . . . . . . 11 ⊢ (𝐻 ∈ 𝑉 → (Itv‘𝐺) = (Itv‘(𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩)))
78		ttgval.i	. . . . . . . . . . . 12 ⊢ 𝐼 = (Itv‘𝐺)
79	78	a1i 11	. . . . . . . . . . 11 ⊢ (𝐻 ∈ 𝑉 → 𝐼 = (Itv‘𝐺))
80	73	setsid 17113	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ 𝑉 ∧ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) ∈ V) → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) = (Itv‘(𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩)))
81	33, 80	mpan2 691	. . . . . . . . . . 11 ⊢ (𝐻 ∈ 𝑉 → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) = (Itv‘(𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩)))
82	77, 79, 81	3eqtr4d 2776	. . . . . . . . . 10 ⊢ (𝐻 ∈ 𝑉 → 𝐼 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}))
83	82	oveqd 7358	. . . . . . . . 9 ⊢ (𝐻 ∈ 𝑉 → (𝑥𝐼𝑦) = (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦))
84	83	eleq2d 2817	. . . . . . . 8 ⊢ (𝐻 ∈ 𝑉 → (𝑧 ∈ (𝑥𝐼𝑦) ↔ 𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦)))
85	82	oveqd 7358	. . . . . . . . 9 ⊢ (𝐻 ∈ 𝑉 → (𝑧𝐼𝑦) = (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦))
86	85	eleq2d 2817	. . . . . . . 8 ⊢ (𝐻 ∈ 𝑉 → (𝑥 ∈ (𝑧𝐼𝑦) ↔ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦)))
87	82	oveqd 7358	. . . . . . . . 9 ⊢ (𝐻 ∈ 𝑉 → (𝑥𝐼𝑧) = (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))
88	87	eleq2d 2817	. . . . . . . 8 ⊢ (𝐻 ∈ 𝑉 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧)))
89	84, 86, 88	3orbi123d 1437	. . . . . . 7 ⊢ (𝐻 ∈ 𝑉 → ((𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))))
90	89	rabbidv 3402	. . . . . 6 ⊢ (𝐻 ∈ 𝑉 → {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))} = {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})
91	90	mpoeq3dv 7420	. . . . 5 ⊢ (𝐻 ∈ 𝑉 → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))}) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))}))
92	91	opeq2d 4827	. . . 4 ⊢ (𝐻 ∈ 𝑉 → ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})⟩ = ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})⟩)
93	92	oveq2d 7357	. . 3 ⊢ (𝐻 ∈ 𝑉 → ((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})⟩) = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})⟩))
94	71, 93	eqtr4d 2769	. 2 ⊢ (𝐻 ∈ 𝑉 → 𝐺 = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})⟩))
95	94, 82	jca 511	1 ⊢ (𝐻 ∈ 𝑉 → (𝐺 = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})⟩) ∧ 𝐼 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∨ w3o 1085 = wceq 1541 ∈ wcel 2111 ∃wrex 3056 {crab 3395 Vcvv 3436 ⦋csb 3845 ⟨cop 4577 ‘cfv 6476 (class class class)co 7341 ∈ cmpo 7343 0cc0 11001 1c1 11002 [,]cicc 13243 sSet csts 17069 ndxcnx 17099 Basecbs 17115 ·_𝑠 cvsca 17160 -_gcsg 18843 Itvcitv 28406 LineGclng 28407 toTGcttg 28846

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 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5212 ax-sep 5229 ax-nul 5239 ax-pow 5298 ax-pr 5365 ax-un 7663 ax-cnex 11057 ax-resscn 11058 ax-1cn 11059 ax-icn 11060 ax-addcl 11061 ax-addrcl 11062 ax-mulcl 11063 ax-mulrcl 11064 ax-mulcom 11065 ax-addass 11066 ax-mulass 11067 ax-distr 11068 ax-i2m1 11069 ax-1ne0 11070 ax-1rid 11071 ax-rnegex 11072 ax-rrecex 11073 ax-cnre 11074 ax-pre-lttri 11075 ax-pre-lttrn 11076 ax-pre-ltadd 11077 ax-pre-mulgt0 11078

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4279 df-if 4471 df-pw 4547 df-sn 4572 df-pr 4574 df-op 4578 df-uni 4855 df-iun 4938 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5506 df-eprel 5511 df-po 5519 df-so 5520 df-fr 5564 df-we 5566 df-xp 5617 df-rel 5618 df-cnv 5619 df-co 5620 df-dm 5621 df-rn 5622 df-res 5623 df-ima 5624 df-pred 6243 df-ord 6304 df-on 6305 df-lim 6306 df-suc 6307 df-iota 6432 df-fun 6478 df-fn 6479 df-f 6480 df-f1 6481 df-fo 6482 df-f1o 6483 df-fv 6484 df-riota 7298 df-ov 7344 df-oprab 7345 df-mpo 7346 df-om 7792 df-1st 7916 df-2nd 7917 df-frecs 8206 df-wrecs 8237 df-recs 8286 df-rdg 8324 df-er 8617 df-en 8865 df-dom 8866 df-sdom 8867 df-pnf 11143 df-mnf 11144 df-xr 11145 df-ltxr 11146 df-le 11147 df-sub 11341 df-neg 11342 df-nn 12121 df-2 12183 df-3 12184 df-4 12185 df-5 12186 df-6 12187 df-7 12188 df-8 12189 df-9 12190 df-n0 12377 df-dec 12584 df-sets 17070 df-slot 17088 df-ndx 17100 df-itv 28408 df-lng 28409 df-ttg 28847

This theorem is referenced by: ttglem 28849 ttgitvval 28855

W3C validator