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 29205

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 3476	. . . . 5 ⊢ (𝐻 ∈ 𝑉 → 𝐻 ∈ V)
4		fveq2 6883	. . . . . . . . 9 ⊢ (𝑤 = 𝐻 → (Base‘𝑤) = (Base‘𝐻))
5		ttgval.b	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝐻)
6	4, 5	eqtr4di 2816	. . . . . . . 8 ⊢ (𝑤 = 𝐻 → (Base‘𝑤) = 𝐵)
7		fveq2 6883	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝐻 → (-_g‘𝑤) = (-_g‘𝐻))
8		ttgval.m	. . . . . . . . . . . . 13 ⊢ − = (-_g‘𝐻)
9	7, 8	eqtr4di 2816	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝐻 → (-_g‘𝑤) = − )
10	9	oveqd 7429	. . . . . . . . . . 11 ⊢ (𝑤 = 𝐻 → (𝑧(-_g‘𝑤)𝑥) = (𝑧 − 𝑥))
11		fveq2 6883	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝐻 → ( ·_𝑠 ‘𝑤) = ( ·_𝑠 ‘𝐻))
12		ttgval.s	. . . . . . . . . . . . 13 ⊢ · = ( ·_𝑠 ‘𝐻)
13	11, 12	eqtr4di 2816	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝐻 → ( ·_𝑠 ‘𝑤) = · )
14		eqidd 2764	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝐻 → 𝑘 = 𝑘)
15	9	oveqd 7429	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝐻 → (𝑦(-_g‘𝑤)𝑥) = (𝑦 − 𝑥))
16	13, 14, 15	oveq123d 7433	. . . . . . . . . . 11 ⊢ (𝑤 = 𝐻 → (𝑘( ·_𝑠 ‘𝑤)(𝑦(-_g‘𝑤)𝑥)) = (𝑘 · (𝑦 − 𝑥)))
17	10, 16	eqeq12d 2779	. . . . . . . . . 10 ⊢ (𝑤 = 𝐻 → ((𝑧(-_g‘𝑤)𝑥) = (𝑘( ·_𝑠 ‘𝑤)(𝑦(-_g‘𝑤)𝑥)) ↔ (𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))))
18	17	rexbidv 3189	. . . . . . . . 9 ⊢ (𝑤 = 𝐻 → (∃𝑘 ∈ (0[,]1)(𝑧(-_g‘𝑤)𝑥) = (𝑘( ·_𝑠 ‘𝑤)(𝑦(-_g‘𝑤)𝑥)) ↔ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))))
19	6, 18	rabeqbidv 3434	. . . . . . . 8 ⊢ (𝑤 = 𝐻 → {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-_g‘𝑤)𝑥) = (𝑘( ·_𝑠 ‘𝑤)(𝑦(-_g‘𝑤)𝑥))} = {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})
20	6, 6, 19	mpoeq123dv 7487	. . . . . . 7 ⊢ (𝑤 = 𝐻 → (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-_g‘𝑤)𝑥) = (𝑘( ·_𝑠 ‘𝑤)(𝑦(-_g‘𝑤)𝑥))}) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}))
21		oveq1 7419	. . . . . . . 8 ⊢ (𝑤 = 𝐻 → (𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) = (𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩))
22	6	rabeqdv 3431	. . . . . . . . . 10 ⊢ (𝑤 = 𝐻 → {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))} = {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})
23	6, 6, 22	mpoeq123dv 7487	. . . . . . . . 9 ⊢ (𝑤 = 𝐻 → (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}))
24	23	opeq2d 4846	. . . . . . . 8 ⊢ (𝑤 = 𝐻 → ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩ = ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩)
25	21, 24	oveq12d 7430	. . . . . . 7 ⊢ (𝑤 = 𝐻 → ((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) = ((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
26	20, 25	csbeq12dv 3863	. . . . . 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 29204	. . . . . 6 ⊢ toTG = (𝑤 ∈ V ↦ ⦋(𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-_g‘𝑤)𝑥) = (𝑘( ·_𝑠 ‘𝑤)(𝑦(-_g‘𝑤)𝑥))}) / 𝑖⦌((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
28		ovex 7445	. . . . . . 7 ⊢ ((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) ∈ V
29	28	csbex 5275	. . . . . 6 ⊢ ⦋(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) / 𝑖⦌((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) ∈ V
30	26, 27, 29	fvmpt 6991	. . . . 5 ⊢ (𝐻 ∈ V → (toTG‘𝐻) = ⦋(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) / 𝑖⦌((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
31	3, 30	syl 18	. . . 4 ⊢ (𝐻 ∈ 𝑉 → (toTG‘𝐻) = ⦋(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) / 𝑖⦌((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
32	5	fvexi 6897	. . . . . . 7 ⊢ 𝐵 ∈ V
33	32, 32	mpoex 8077	. . . . . 6 ⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) ∈ V
34	33	a1i 11	. . . . 5 ⊢ (𝐻 ∈ 𝑉 → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) ∈ V)
35		simpr 489	. . . . . . 7 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})) → 𝑖 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}))
36		oveq2 7420	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑥 → (𝑐 − 𝑎) = (𝑐 − 𝑥))
37		oveq2 7420	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑥 → (𝑏 − 𝑎) = (𝑏 − 𝑥))
38	37	oveq2d 7428	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑥 → (𝑘 · (𝑏 − 𝑎)) = (𝑘 · (𝑏 − 𝑥)))
39	36, 38	eqeq12d 2779	. . . . . . . . . 10 ⊢ (𝑎 = 𝑥 → ((𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎)) ↔ (𝑐 − 𝑥) = (𝑘 · (𝑏 − 𝑥))))
40	39	rexbidv 3189	. . . . . . . . 9 ⊢ (𝑎 = 𝑥 → (∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎)) ↔ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑏 − 𝑥))))
41	40	rabbidv 3423	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))} = {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑏 − 𝑥))})
42		oveq1 7419	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑦 → (𝑏 − 𝑥) = (𝑦 − 𝑥))
43	42	oveq2d 7428	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑦 → (𝑘 · (𝑏 − 𝑥)) = (𝑘 · (𝑦 − 𝑥)))
44	43	eqeq2d 2774	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑦 → ((𝑐 − 𝑥) = (𝑘 · (𝑏 − 𝑥)) ↔ (𝑐 − 𝑥) = (𝑘 · (𝑦 − 𝑥))))
45	44	rexbidv 3189	. . . . . . . . . 10 ⊢ (𝑏 = 𝑦 → (∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑏 − 𝑥)) ↔ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑦 − 𝑥))))
46	45	rabbidv 3423	. . . . . . . . 9 ⊢ (𝑏 = 𝑦 → {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑏 − 𝑥))} = {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})
47		oveq1 7419	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑧 → (𝑐 − 𝑥) = (𝑧 − 𝑥))
48	47	eqeq1d 2765	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑧 → ((𝑐 − 𝑥) = (𝑘 · (𝑦 − 𝑥)) ↔ (𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))))
49	48	rexbidv 3189	. . . . . . . . . 10 ⊢ (𝑐 = 𝑧 → (∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑦 − 𝑥)) ↔ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))))
50	49	cbvrabv 3426	. . . . . . . . 9 ⊢ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑦 − 𝑥))} = {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}
51	46, 50	eqtrdi 2814	. . . . . . . 8 ⊢ (𝑏 = 𝑦 → {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑏 − 𝑥))} = {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})
52	41, 51	cbvmpov 7507	. . . . . . 7 ⊢ (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))}) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})
53	35, 52	eqtr4di 2816	. . . . . 6 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})) → 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))}))
54		simpr 489	. . . . . . . . . 10 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))}))
55	54, 52	eqtrdi 2814	. . . . . . . . 9 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → 𝑖 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}))
56	55	opeq2d 4846	. . . . . . . 8 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → ⟨(Itv‘ndx), 𝑖⟩ = ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩)
57	56	oveq2d 7428	. . . . . . 7 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → (𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) = (𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩))
58	55	oveqd 7429	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → (𝑥𝑖𝑦) = (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦))
59	58	eleq2d 2849	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → (𝑧 ∈ (𝑥𝑖𝑦) ↔ 𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦)))
60	55	oveqd 7429	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → (𝑧𝑖𝑦) = (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦))
61	60	eleq2d 2849	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → (𝑥 ∈ (𝑧𝑖𝑦) ↔ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦)))
62	55	oveqd 7429	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → (𝑥𝑖𝑧) = (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))
63	62	eleq2d 2849	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → (𝑦 ∈ (𝑥𝑖𝑧) ↔ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧)))
64	59, 61, 63	3orbi123d 1463	. . . . . . . . . 10 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → ((𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)) ↔ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))))
65	64	rabbidv 3423	. . . . . . . . 9 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))} = {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})
66	65	mpoeq3dv 7491	. . . . . . . 8 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))}))
67	66	opeq2d 4846	. . . . . . 7 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩ = ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})⟩)
68	57, 67	oveq12d 7430	. . . . . 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 602	. . . . 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 3890	. . . 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 2802	. . 3 ⊢ (𝐻 ∈ 𝑉 → 𝐺 = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})⟩))
72	71	fveq2d 6887	. . . . . . . . . . . 12 ⊢ (𝐻 ∈ 𝑉 → (Itv‘𝐺) = (Itv‘((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})⟩)))
73		itvid 28689	. . . . . . . . . . . . 13 ⊢ Itv = Slot (Itv‘ndx)
74		lngndxnitvndx 28693	. . . . . . . . . . . . . 14 ⊢ (LineG‘ndx) ≠ (Itv‘ndx)
75	74	necomi 3012	. . . . . . . . . . . . 13 ⊢ (Itv‘ndx) ≠ (LineG‘ndx)
76	73, 75	setsnid 17269	. . . . . . . . . . . 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 2816	. . . . . . . . . . 11 ⊢ (𝐻 ∈ 𝑉 → (Itv‘𝐺) = (Itv‘(𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩)))
78		ttgval.i	. . . . . . . . . . . 12 ⊢ 𝐼 = (Itv‘𝐺)
79	78	a1i 11	. . . . . . . . . . 11 ⊢ (𝐻 ∈ 𝑉 → 𝐼 = (Itv‘𝐺))
80	73	setsid 17268	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ 𝑉 ∧ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) ∈ V) → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) = (Itv‘(𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩)))
81	33, 80	mpan2 703	. . . . . . . . . . 11 ⊢ (𝐻 ∈ 𝑉 → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) = (Itv‘(𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩)))
82	77, 79, 81	3eqtr4d 2808	. . . . . . . . . 10 ⊢ (𝐻 ∈ 𝑉 → 𝐼 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}))
83	82	oveqd 7429	. . . . . . . . 9 ⊢ (𝐻 ∈ 𝑉 → (𝑥𝐼𝑦) = (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦))
84	83	eleq2d 2849	. . . . . . . 8 ⊢ (𝐻 ∈ 𝑉 → (𝑧 ∈ (𝑥𝐼𝑦) ↔ 𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦)))
85	82	oveqd 7429	. . . . . . . . 9 ⊢ (𝐻 ∈ 𝑉 → (𝑧𝐼𝑦) = (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦))
86	85	eleq2d 2849	. . . . . . . 8 ⊢ (𝐻 ∈ 𝑉 → (𝑥 ∈ (𝑧𝐼𝑦) ↔ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦)))
87	82	oveqd 7429	. . . . . . . . 9 ⊢ (𝐻 ∈ 𝑉 → (𝑥𝐼𝑧) = (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))
88	87	eleq2d 2849	. . . . . . . 8 ⊢ (𝐻 ∈ 𝑉 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧)))
89	84, 86, 88	3orbi123d 1463	. . . . . . 7 ⊢ (𝐻 ∈ 𝑉 → ((𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))))
90	89	rabbidv 3423	. . . . . 6 ⊢ (𝐻 ∈ 𝑉 → {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))} = {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})
91	90	mpoeq3dv 7491	. . . . 5 ⊢ (𝐻 ∈ 𝑉 → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))}) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))}))
92	91	opeq2d 4846	. . . 4 ⊢ (𝐻 ∈ 𝑉 → ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})⟩ = ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})⟩)
93	92	oveq2d 7428	. . 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 2801	. 2 ⊢ (𝐻 ∈ 𝑉 → 𝐺 = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})⟩))
95	94, 82	jca 520	1 ⊢ (𝐻 ∈ 𝑉 → (𝐺 = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})⟩) ∧ 𝐼 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 ∨ w3o 1102 = wceq 1570 ∈ wcel 2143 ∃wrex 3089 {crab 3416 Vcvv 3455 ⦋csb 3854 ⟨cop 4596 ‘cfv 6538 (class class class)co 7412 ∈ cmpo 7414 0cc0 11101 1c1 11102 [,]cicc 13376 sSet csts 17224 ndxcnx 17254 Basecbs 17270 ·_𝑠 cvsca 17315 -_gcsg 19003 Itvcitv 28683 LineGclng 28684 toTGcttg 29203

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5239 ax-sep 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734 ax-cnex 11157 ax-resscn 11158 ax-1cn 11159 ax-icn 11160 ax-addcl 11161 ax-addrcl 11162 ax-mulcl 11163 ax-mulrcl 11164 ax-mulcom 11165 ax-addass 11166 ax-mulass 11167 ax-distr 11168 ax-i2m1 11169 ax-1ne0 11170 ax-1rid 11171 ax-rnegex 11172 ax-rrecex 11173 ax-cnre 11174 ax-pre-lttri 11175 ax-pre-lttrn 11176 ax-pre-ltadd 11177 ax-pre-mulgt0 11178

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4874 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7864 df-1st 7987 df-2nd 7988 df-frecs 8279 df-wrecs 8310 df-recs 8359 df-rdg 8398 df-er 8695 df-en 8945 df-dom 8946 df-sdom 8947 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11444 df-neg 11445 df-nn 12235 df-2 12304 df-3 12305 df-4 12306 df-5 12307 df-6 12308 df-7 12309 df-8 12310 df-9 12311 df-n0 12506 df-dec 12713 df-sets 17225 df-slot 17243 df-ndx 17255 df-itv 28685 df-lng 28686 df-ttg 29204

This theorem is referenced by: ttglem 29206 ttgitvval 29212

W3C validator