Theorem ttglem

Description: Lemma for ttgbas , ttgvsca etc. (Contributed by Thierry Arnoux, 15-Apr-2019) (Revised by AV, 29-Oct-2024)

	Ref	Expression
Hypotheses	ttgval.n	⊢ 𝐺 = ( toTG ‘ 𝐻 )
	ttglem.e	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
	ttglem.l	⊢ ( 𝐸 ‘ ndx ) ≠ ( LineG ‘ ndx )
	ttglem.i	⊢ ( 𝐸 ‘ ndx ) ≠ ( Itv ‘ ndx )
Assertion	ttglem	⊢ ( 𝐸 ‘ 𝐻 ) = ( 𝐸 ‘ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		ttgval.n	⊢ 𝐺 = ( toTG ‘ 𝐻 )
2		ttglem.e	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
3		ttglem.l	⊢ ( 𝐸 ‘ ndx ) ≠ ( LineG ‘ ndx )
4		ttglem.i	⊢ ( 𝐸 ‘ ndx ) ≠ ( Itv ‘ ndx )
5	2 4	setsnid	⊢ ( 𝐸 ‘ 𝐻 ) = ( 𝐸 ‘ ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐻 ) , 𝑦 ∈ ( Base ‘ 𝐻 ) ↦ { 𝑧 ∈ ( Base ‘ 𝐻 ) ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 ( -g ‘ 𝐻 ) 𝑥 ) = ( 𝑘 ( ·𝑠 ‘ 𝐻 ) ( 𝑦 ( -g ‘ 𝐻 ) 𝑥 ) ) } ) ⟩ ) )
6	2 3	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 ‘ 𝐺 ) 𝑧 ) ) } ) ⟩ ) )
7	5 6	eqtri	⊢ ( 𝐸 ‘ 𝐻 ) = ( 𝐸 ‘ ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐻 ) , 𝑦 ∈ ( Base ‘ 𝐻 ) ↦ { 𝑧 ∈ ( Base ‘ 𝐻 ) ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 ( -g ‘ 𝐻 ) 𝑥 ) = ( 𝑘 ( ·𝑠 ‘ 𝐻 ) ( 𝑦 ( -g ‘ 𝐻 ) 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐻 ) , 𝑦 ∈ ( Base ‘ 𝐻 ) ↦ { 𝑧 ∈ ( Base ‘ 𝐻 ) ∣ ( 𝑧 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑧 ) ) } ) ⟩ ) )
8		eqid	⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
9		eqid	⊢ ( -g ‘ 𝐻 ) = ( -g ‘ 𝐻 )
10		eqid	⊢ ( ·𝑠 ‘ 𝐻 ) = ( ·𝑠 ‘ 𝐻 )
11		eqid	⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
12	1 8 9 10 11	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 ‘ 𝐻 ) 𝑥 ) ) } ) ) )
13	12	simpld	⊢ ( 𝐻 ∈ V → 𝐺 = ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐻 ) , 𝑦 ∈ ( Base ‘ 𝐻 ) ↦ { 𝑧 ∈ ( Base ‘ 𝐻 ) ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 ( -g ‘ 𝐻 ) 𝑥 ) = ( 𝑘 ( ·𝑠 ‘ 𝐻 ) ( 𝑦 ( -g ‘ 𝐻 ) 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐻 ) , 𝑦 ∈ ( Base ‘ 𝐻 ) ↦ { 𝑧 ∈ ( Base ‘ 𝐻 ) ∣ ( 𝑧 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑧 ) ) } ) ⟩ ) )
14	13	fveq2d	⊢ ( 𝐻 ∈ V → ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐻 ) , 𝑦 ∈ ( Base ‘ 𝐻 ) ↦ { 𝑧 ∈ ( Base ‘ 𝐻 ) ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 ( -g ‘ 𝐻 ) 𝑥 ) = ( 𝑘 ( ·𝑠 ‘ 𝐻 ) ( 𝑦 ( -g ‘ 𝐻 ) 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐻 ) , 𝑦 ∈ ( Base ‘ 𝐻 ) ↦ { 𝑧 ∈ ( Base ‘ 𝐻 ) ∣ ( 𝑧 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑧 ) ) } ) ⟩ ) ) )
15	7 14	eqtr4id	⊢ ( 𝐻 ∈ V → ( 𝐸 ‘ 𝐻 ) = ( 𝐸 ‘ 𝐺 ) )
16	2	str0	⊢ ∅ = ( 𝐸 ‘ ∅ )
17	16	eqcomi	⊢ ( 𝐸 ‘ ∅ ) = ∅
18	17 1	fveqprc	⊢ ( ¬ 𝐻 ∈ V → ( 𝐸 ‘ 𝐻 ) = ( 𝐸 ‘ 𝐺 ) )
19	15 18	pm2.61i	⊢ ( 𝐸 ‘ 𝐻 ) = ( 𝐸 ‘ 𝐺 )