# Metamath Proof Explorer

## Theorem ttglem

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

Ref Expression
Hypotheses ttgval.n ${⊢}{G}={to𝒢}_{\mathrm{Tarski}}\left({H}\right)$
ttglem.2 ${⊢}{E}=\mathrm{Slot}{N}$
ttglem.3 ${⊢}{N}\in ℕ$
ttglem.4 ${⊢}{N}<16$
Assertion ttglem ${⊢}{E}\left({H}\right)={E}\left({G}\right)$

### Proof

Step Hyp Ref Expression
1 ttgval.n ${⊢}{G}={to𝒢}_{\mathrm{Tarski}}\left({H}\right)$
2 ttglem.2 ${⊢}{E}=\mathrm{Slot}{N}$
3 ttglem.3 ${⊢}{N}\in ℕ$
4 ttglem.4 ${⊢}{N}<16$
5 2 3 ndxid ${⊢}{E}=\mathrm{Slot}{E}\left(\mathrm{ndx}\right)$
6 3 nnrei ${⊢}{N}\in ℝ$
7 6 4 ltneii ${⊢}{N}\ne 16$
8 2 3 ndxarg ${⊢}{E}\left(\mathrm{ndx}\right)={N}$
9 itvndx ${⊢}\mathrm{Itv}\left(\mathrm{ndx}\right)=16$
10 8 9 neeq12i ${⊢}{E}\left(\mathrm{ndx}\right)\ne \mathrm{Itv}\left(\mathrm{ndx}\right)↔{N}\ne 16$
11 7 10 mpbir ${⊢}{E}\left(\mathrm{ndx}\right)\ne \mathrm{Itv}\left(\mathrm{ndx}\right)$
12 5 11 setsnid ${⊢}{E}\left({H}\right)={E}\left({H}\mathrm{sSet}⟨\mathrm{Itv}\left(\mathrm{ndx}\right),\left({x}\in {\mathrm{Base}}_{{H}},{y}\in {\mathrm{Base}}_{{H}}⟼\left\{{z}\in {\mathrm{Base}}_{{H}}|\exists {k}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}{z}{-}_{{H}}{x}={k}{\cdot }_{{H}}\left({y}{-}_{{H}}{x}\right)\right\}\right)⟩\right)$
13 1nn0 ${⊢}1\in {ℕ}_{0}$
14 6nn0 ${⊢}6\in {ℕ}_{0}$
15 7nn ${⊢}7\in ℕ$
16 6lt7 ${⊢}6<7$
17 13 14 15 16 declt ${⊢}16<17$
18 6nn ${⊢}6\in ℕ$
19 13 18 decnncl ${⊢}16\in ℕ$
20 19 nnrei ${⊢}16\in ℝ$
21 13 15 decnncl ${⊢}17\in ℕ$
22 21 nnrei ${⊢}17\in ℝ$
23 6 20 22 lttri ${⊢}\left({N}<16\wedge 16<17\right)\to {N}<17$
24 4 17 23 mp2an ${⊢}{N}<17$
25 6 24 ltneii ${⊢}{N}\ne 17$
26 lngndx ${⊢}{Line}_{𝒢}\left(\mathrm{ndx}\right)=17$
27 8 26 neeq12i ${⊢}{E}\left(\mathrm{ndx}\right)\ne {Line}_{𝒢}\left(\mathrm{ndx}\right)↔{N}\ne 17$
28 25 27 mpbir ${⊢}{E}\left(\mathrm{ndx}\right)\ne {Line}_{𝒢}\left(\mathrm{ndx}\right)$
29 5 28 setsnid ${⊢}{E}\left({H}\mathrm{sSet}⟨\mathrm{Itv}\left(\mathrm{ndx}\right),\left({x}\in {\mathrm{Base}}_{{H}},{y}\in {\mathrm{Base}}_{{H}}⟼\left\{{z}\in {\mathrm{Base}}_{{H}}|\exists {k}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}{z}{-}_{{H}}{x}={k}{\cdot }_{{H}}\left({y}{-}_{{H}}{x}\right)\right\}\right)⟩\right)={E}\left(\left({H}\mathrm{sSet}⟨\mathrm{Itv}\left(\mathrm{ndx}\right),\left({x}\in {\mathrm{Base}}_{{H}},{y}\in {\mathrm{Base}}_{{H}}⟼\left\{{z}\in {\mathrm{Base}}_{{H}}|\exists {k}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}{z}{-}_{{H}}{x}={k}{\cdot }_{{H}}\left({y}{-}_{{H}}{x}\right)\right\}\right)⟩\right)\mathrm{sSet}⟨{Line}_{𝒢}\left(\mathrm{ndx}\right),\left({x}\in {\mathrm{Base}}_{{H}},{y}\in {\mathrm{Base}}_{{H}}⟼\left\{{z}\in {\mathrm{Base}}_{{H}}|\left({z}\in \left({x}\mathrm{Itv}\left({G}\right){y}\right)\vee {x}\in \left({z}\mathrm{Itv}\left({G}\right){y}\right)\vee {y}\in \left({x}\mathrm{Itv}\left({G}\right){z}\right)\right)\right\}\right)⟩\right)$
30 12 29 eqtri ${⊢}{E}\left({H}\right)={E}\left(\left({H}\mathrm{sSet}⟨\mathrm{Itv}\left(\mathrm{ndx}\right),\left({x}\in {\mathrm{Base}}_{{H}},{y}\in {\mathrm{Base}}_{{H}}⟼\left\{{z}\in {\mathrm{Base}}_{{H}}|\exists {k}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}{z}{-}_{{H}}{x}={k}{\cdot }_{{H}}\left({y}{-}_{{H}}{x}\right)\right\}\right)⟩\right)\mathrm{sSet}⟨{Line}_{𝒢}\left(\mathrm{ndx}\right),\left({x}\in {\mathrm{Base}}_{{H}},{y}\in {\mathrm{Base}}_{{H}}⟼\left\{{z}\in {\mathrm{Base}}_{{H}}|\left({z}\in \left({x}\mathrm{Itv}\left({G}\right){y}\right)\vee {x}\in \left({z}\mathrm{Itv}\left({G}\right){y}\right)\vee {y}\in \left({x}\mathrm{Itv}\left({G}\right){z}\right)\right)\right\}\right)⟩\right)$
31 eqid ${⊢}{\mathrm{Base}}_{{H}}={\mathrm{Base}}_{{H}}$
32 eqid ${⊢}{-}_{{H}}={-}_{{H}}$
33 eqid ${⊢}{\cdot }_{{H}}={\cdot }_{{H}}$
34 eqid ${⊢}\mathrm{Itv}\left({G}\right)=\mathrm{Itv}\left({G}\right)$
35 1 31 32 33 34 ttgval ${⊢}{H}\in \mathrm{V}\to \left({G}=\left({H}\mathrm{sSet}⟨\mathrm{Itv}\left(\mathrm{ndx}\right),\left({x}\in {\mathrm{Base}}_{{H}},{y}\in {\mathrm{Base}}_{{H}}⟼\left\{{z}\in {\mathrm{Base}}_{{H}}|\exists {k}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}{z}{-}_{{H}}{x}={k}{\cdot }_{{H}}\left({y}{-}_{{H}}{x}\right)\right\}\right)⟩\right)\mathrm{sSet}⟨{Line}_{𝒢}\left(\mathrm{ndx}\right),\left({x}\in {\mathrm{Base}}_{{H}},{y}\in {\mathrm{Base}}_{{H}}⟼\left\{{z}\in {\mathrm{Base}}_{{H}}|\left({z}\in \left({x}\mathrm{Itv}\left({G}\right){y}\right)\vee {x}\in \left({z}\mathrm{Itv}\left({G}\right){y}\right)\vee {y}\in \left({x}\mathrm{Itv}\left({G}\right){z}\right)\right)\right\}\right)⟩\wedge \mathrm{Itv}\left({G}\right)=\left({x}\in {\mathrm{Base}}_{{H}},{y}\in {\mathrm{Base}}_{{H}}⟼\left\{{z}\in {\mathrm{Base}}_{{H}}|\exists {k}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}{z}{-}_{{H}}{x}={k}{\cdot }_{{H}}\left({y}{-}_{{H}}{x}\right)\right\}\right)\right)$
36 35 simpld ${⊢}{H}\in \mathrm{V}\to {G}=\left({H}\mathrm{sSet}⟨\mathrm{Itv}\left(\mathrm{ndx}\right),\left({x}\in {\mathrm{Base}}_{{H}},{y}\in {\mathrm{Base}}_{{H}}⟼\left\{{z}\in {\mathrm{Base}}_{{H}}|\exists {k}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}{z}{-}_{{H}}{x}={k}{\cdot }_{{H}}\left({y}{-}_{{H}}{x}\right)\right\}\right)⟩\right)\mathrm{sSet}⟨{Line}_{𝒢}\left(\mathrm{ndx}\right),\left({x}\in {\mathrm{Base}}_{{H}},{y}\in {\mathrm{Base}}_{{H}}⟼\left\{{z}\in {\mathrm{Base}}_{{H}}|\left({z}\in \left({x}\mathrm{Itv}\left({G}\right){y}\right)\vee {x}\in \left({z}\mathrm{Itv}\left({G}\right){y}\right)\vee {y}\in \left({x}\mathrm{Itv}\left({G}\right){z}\right)\right)\right\}\right)⟩$
37 36 fveq2d ${⊢}{H}\in \mathrm{V}\to {E}\left({G}\right)={E}\left(\left({H}\mathrm{sSet}⟨\mathrm{Itv}\left(\mathrm{ndx}\right),\left({x}\in {\mathrm{Base}}_{{H}},{y}\in {\mathrm{Base}}_{{H}}⟼\left\{{z}\in {\mathrm{Base}}_{{H}}|\exists {k}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}{z}{-}_{{H}}{x}={k}{\cdot }_{{H}}\left({y}{-}_{{H}}{x}\right)\right\}\right)⟩\right)\mathrm{sSet}⟨{Line}_{𝒢}\left(\mathrm{ndx}\right),\left({x}\in {\mathrm{Base}}_{{H}},{y}\in {\mathrm{Base}}_{{H}}⟼\left\{{z}\in {\mathrm{Base}}_{{H}}|\left({z}\in \left({x}\mathrm{Itv}\left({G}\right){y}\right)\vee {x}\in \left({z}\mathrm{Itv}\left({G}\right){y}\right)\vee {y}\in \left({x}\mathrm{Itv}\left({G}\right){z}\right)\right)\right\}\right)⟩\right)$
38 30 37 eqtr4id ${⊢}{H}\in \mathrm{V}\to {E}\left({H}\right)={E}\left({G}\right)$
39 2 str0 ${⊢}\varnothing ={E}\left(\varnothing \right)$
40 fvprc ${⊢}¬{H}\in \mathrm{V}\to {E}\left({H}\right)=\varnothing$
41 fvprc ${⊢}¬{H}\in \mathrm{V}\to {to𝒢}_{\mathrm{Tarski}}\left({H}\right)=\varnothing$
42 1 41 syl5eq ${⊢}¬{H}\in \mathrm{V}\to {G}=\varnothing$
43 42 fveq2d ${⊢}¬{H}\in \mathrm{V}\to {E}\left({G}\right)={E}\left(\varnothing \right)$
44 39 40 43 3eqtr4a ${⊢}¬{H}\in \mathrm{V}\to {E}\left({H}\right)={E}\left({G}\right)$
45 38 44 pm2.61i ${⊢}{E}\left({H}\right)={E}\left({G}\right)$