Metamath Proof Explorer

Theorem ttglem

Description: Lemma for ttgbas and ttgvsca . (Contributed by Thierry Arnoux, 15-Apr-2019)

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

Proof

Step Hyp Ref Expression
1 ttgval.n ⊢ 𝐺 = ( toTG ‘ 𝐻 )
2 ttglem.2 ⊢ 𝐸 = Slot 𝑁
3 ttglem.3 ⊢ 𝑁 ∈ ℕ
4 ttglem.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 ⊢ ( 𝐸 ‘ 𝐻 ) = ( 𝐸 ‘ 𝐺 )