Theorem ttglemOLD

Description: Obsolete version of ttglem as of 29-Oct-2024. Lemma for ttgbas and ttgvsca . (Contributed by Thierry Arnoux, 15-Apr-2019) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ttgval.n	⊢ 𝐺 = ( toTG ‘ 𝐻 )
	ttglemOLD.2	⊢ 𝐸 = Slot 𝑁
	ttglemOLD.3	⊢ 𝑁 ∈ ℕ
	ttglemOLD.4	⊢ 𝑁 < ; 1 6
Assertion	ttglemOLD	⊢ ( 𝐸 ‘ 𝐻 ) = ( 𝐸 ‘ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		ttgval.n	⊢ 𝐺 = ( toTG ‘ 𝐻 )
2		ttglemOLD.2	⊢ 𝐸 = Slot 𝑁
3		ttglemOLD.3	⊢ 𝑁 ∈ ℕ
4		ttglemOLD.4	⊢ 𝑁 < ; 1 6
5	2 3	ndxid	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
6	3	nnrei	⊢ 𝑁 ∈ ℝ
7	6 4	ltneii	⊢ 𝑁 ≠ ; 1 6
8	2 3	ndxarg	⊢ ( 𝐸 ‘ ndx ) = 𝑁
9		itvndx	⊢ ( Itv ‘ ndx ) = ; 1 6
10	8 9	neeq12i	⊢ ( ( 𝐸 ‘ ndx ) ≠ ( Itv ‘ ndx ) ↔ 𝑁 ≠ ; 1 6 )
11	7 10	mpbir	⊢ ( 𝐸 ‘ ndx ) ≠ ( Itv ‘ ndx )
12	5 11	setsnid	⊢ ( 𝐸 ‘ 𝐻 ) = ( 𝐸 ‘ ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐻 ) , 𝑦 ∈ ( Base ‘ 𝐻 ) ↦ { 𝑧 ∈ ( Base ‘ 𝐻 ) ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 ( -g ‘ 𝐻 ) 𝑥 ) = ( 𝑘 ( ·𝑠 ‘ 𝐻 ) ( 𝑦 ( -g ‘ 𝐻 ) 𝑥 ) ) } ) ⟩ ) )
13		1nn0	⊢ 1 ∈ ℕ0
14		6nn0	⊢ 6 ∈ ℕ0
15		7nn	⊢ 7 ∈ ℕ
16		6lt7	⊢ 6 < 7
17	13 14 15 16	declt	⊢ ; 1 6 < ; 1 7
18		6nn	⊢ 6 ∈ ℕ
19	13 18	decnncl	⊢ ; 1 6 ∈ ℕ
20	19	nnrei	⊢ ; 1 6 ∈ ℝ
21	13 15	decnncl	⊢ ; 1 7 ∈ ℕ
22	21	nnrei	⊢ ; 1 7 ∈ ℝ
23	6 20 22	lttri	⊢ ( ( 𝑁 < ; 1 6 ∧ ; 1 6 < ; 1 7 ) → 𝑁 < ; 1 7 )
24	4 17 23	mp2an	⊢ 𝑁 < ; 1 7
25	6 24	ltneii	⊢ 𝑁 ≠ ; 1 7
26		lngndx	⊢ ( LineG ‘ ndx ) = ; 1 7
27	8 26	neeq12i	⊢ ( ( 𝐸 ‘ ndx ) ≠ ( LineG ‘ ndx ) ↔ 𝑁 ≠ ; 1 7 )
28	25 27	mpbir	⊢ ( 𝐸 ‘ ndx ) ≠ ( LineG ‘ ndx )
29	5 28	setsnid	⊢ ( 𝐸 ‘ ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐻 ) , 𝑦 ∈ ( Base ‘ 𝐻 ) ↦ { 𝑧 ∈ ( Base ‘ 𝐻 ) ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 ( -g ‘ 𝐻 ) 𝑥 ) = ( 𝑘 ( ·𝑠 ‘ 𝐻 ) ( 𝑦 ( -g ‘ 𝐻 ) 𝑥 ) ) } ) ⟩ ) ) = ( 𝐸 ‘ ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐻 ) , 𝑦 ∈ ( Base ‘ 𝐻 ) ↦ { 𝑧 ∈ ( Base ‘ 𝐻 ) ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 ( -g ‘ 𝐻 ) 𝑥 ) = ( 𝑘 ( ·𝑠 ‘ 𝐻 ) ( 𝑦 ( -g ‘ 𝐻 ) 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐻 ) , 𝑦 ∈ ( Base ‘ 𝐻 ) ↦ { 𝑧 ∈ ( Base ‘ 𝐻 ) ∣ ( 𝑧 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑧 ) ) } ) ⟩ ) )
30	12 29	eqtri	⊢ ( 𝐸 ‘ 𝐻 ) = ( 𝐸 ‘ ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐻 ) , 𝑦 ∈ ( Base ‘ 𝐻 ) ↦ { 𝑧 ∈ ( Base ‘ 𝐻 ) ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 ( -g ‘ 𝐻 ) 𝑥 ) = ( 𝑘 ( ·𝑠 ‘ 𝐻 ) ( 𝑦 ( -g ‘ 𝐻 ) 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐻 ) , 𝑦 ∈ ( Base ‘ 𝐻 ) ↦ { 𝑧 ∈ ( Base ‘ 𝐻 ) ∣ ( 𝑧 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑧 ) ) } ) ⟩ ) )
31		eqid	⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
32		eqid	⊢ ( -g ‘ 𝐻 ) = ( -g ‘ 𝐻 )
33		eqid	⊢ ( ·𝑠 ‘ 𝐻 ) = ( ·𝑠 ‘ 𝐻 )
34		eqid	⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
35	1 31 32 33 34	ttgval	⊢ ( 𝐻 ∈ V → ( 𝐺 = ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐻 ) , 𝑦 ∈ ( Base ‘ 𝐻 ) ↦ { 𝑧 ∈ ( Base ‘ 𝐻 ) ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 ( -g ‘ 𝐻 ) 𝑥 ) = ( 𝑘 ( ·𝑠 ‘ 𝐻 ) ( 𝑦 ( -g ‘ 𝐻 ) 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐻 ) , 𝑦 ∈ ( Base ‘ 𝐻 ) ↦ { 𝑧 ∈ ( Base ‘ 𝐻 ) ∣ ( 𝑧 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑧 ) ) } ) ⟩ ) ∧ ( Itv ‘ 𝐺 ) = ( 𝑥 ∈ ( Base ‘ 𝐻 ) , 𝑦 ∈ ( Base ‘ 𝐻 ) ↦ { 𝑧 ∈ ( Base ‘ 𝐻 ) ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 ( -g ‘ 𝐻 ) 𝑥 ) = ( 𝑘 ( ·𝑠 ‘ 𝐻 ) ( 𝑦 ( -g ‘ 𝐻 ) 𝑥 ) ) } ) ) )
36	35	simpld	⊢ ( 𝐻 ∈ V → 𝐺 = ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐻 ) , 𝑦 ∈ ( Base ‘ 𝐻 ) ↦ { 𝑧 ∈ ( Base ‘ 𝐻 ) ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 ( -g ‘ 𝐻 ) 𝑥 ) = ( 𝑘 ( ·𝑠 ‘ 𝐻 ) ( 𝑦 ( -g ‘ 𝐻 ) 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐻 ) , 𝑦 ∈ ( Base ‘ 𝐻 ) ↦ { 𝑧 ∈ ( Base ‘ 𝐻 ) ∣ ( 𝑧 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑧 ) ) } ) ⟩ ) )
37	36	fveq2d	⊢ ( 𝐻 ∈ V → ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐻 ) , 𝑦 ∈ ( Base ‘ 𝐻 ) ↦ { 𝑧 ∈ ( Base ‘ 𝐻 ) ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 ( -g ‘ 𝐻 ) 𝑥 ) = ( 𝑘 ( ·𝑠 ‘ 𝐻 ) ( 𝑦 ( -g ‘ 𝐻 ) 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐻 ) , 𝑦 ∈ ( Base ‘ 𝐻 ) ↦ { 𝑧 ∈ ( Base ‘ 𝐻 ) ∣ ( 𝑧 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑧 ) ) } ) ⟩ ) ) )
38	30 37	eqtr4id	⊢ ( 𝐻 ∈ V → ( 𝐸 ‘ 𝐻 ) = ( 𝐸 ‘ 𝐺 ) )
39	2	str0	⊢ ∅ = ( 𝐸 ‘ ∅ )
40		fvprc	⊢ ( ¬ 𝐻 ∈ V → ( 𝐸 ‘ 𝐻 ) = ∅ )
41		fvprc	⊢ ( ¬ 𝐻 ∈ V → ( toTG ‘ 𝐻 ) = ∅ )
42	1 41	syl5eq	⊢ ( ¬ 𝐻 ∈ V → 𝐺 = ∅ )
43	42	fveq2d	⊢ ( ¬ 𝐻 ∈ V → ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ ∅ ) )
44	39 40 43	3eqtr4a	⊢ ( ¬ 𝐻 ∈ V → ( 𝐸 ‘ 𝐻 ) = ( 𝐸 ‘ 𝐺 ) )
45	38 44	pm2.61i	⊢ ( 𝐸 ‘ 𝐻 ) = ( 𝐸 ‘ 𝐺 )