Metamath Proof Explorer

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 ⊒G=to𝒒Tarski⁑H
ttglem.e ⊒E=SlotE⁑ndx
ttglem.l ⊒E⁑ndxβ‰ Line𝒒⁑ndx
ttglem.i ⊒E⁑ndxβ‰ Itv⁑ndx
Assertion ttglem ⊒E⁑H=E⁑G

Proof

Step Hyp Ref Expression
1 ttgval.n ⊒G=to𝒒Tarski⁑H
2 ttglem.e ⊒E=SlotE⁑ndx
3 ttglem.l ⊒E⁑ndxβ‰ Line𝒒⁑ndx
4 ttglem.i ⊒E⁑ndxβ‰ Itv⁑ndx
5 2 4 setsnid ⊒E⁑H=E⁑HsSetItv⁑ndxx∈BaseH,y∈BaseH⟼z∈BaseH|βˆƒk∈01z-Hx=kβ‹…Hy-Hx
6 2 3 setsnid ⊒E⁑HsSetItv⁑ndxx∈BaseH,y∈BaseH⟼z∈BaseH|βˆƒk∈01z-Hx=kβ‹…Hy-Hx=E⁑HsSetItv⁑ndxx∈BaseH,y∈BaseH⟼z∈BaseH|βˆƒk∈01z-Hx=kβ‹…Hy-HxsSetLine𝒒⁑ndxx∈BaseH,y∈BaseH⟼z∈BaseH|z∈xItv⁑Gy∨x∈zItv⁑Gy∨y∈xItv⁑Gz
7 5 6 eqtri ⊒E⁑H=E⁑HsSetItv⁑ndxx∈BaseH,y∈BaseH⟼z∈BaseH|βˆƒk∈01z-Hx=kβ‹…Hy-HxsSetLine𝒒⁑ndxx∈BaseH,y∈BaseH⟼z∈BaseH|z∈xItv⁑Gy∨x∈zItv⁑Gy∨y∈xItv⁑Gz
8 eqid ⊒BaseH=BaseH
9 eqid ⊒-H=-H
10 eqid βŠ’β‹…H=β‹…H
11 eqid ⊒Itv⁑G=Itv⁑G
12 1 8 9 10 11 ttgval ⊒H∈Vβ†’G=HsSetItv⁑ndxx∈BaseH,y∈BaseH⟼z∈BaseH|βˆƒk∈01z-Hx=kβ‹…Hy-HxsSetLine𝒒⁑ndxx∈BaseH,y∈BaseH⟼z∈BaseH|z∈xItv⁑Gy∨x∈zItv⁑Gy∨y∈xItv⁑Gz∧Itv⁑G=x∈BaseH,y∈BaseH⟼z∈BaseH|βˆƒk∈01z-Hx=kβ‹…Hy-Hx
13 12 simpld ⊒H∈Vβ†’G=HsSetItv⁑ndxx∈BaseH,y∈BaseH⟼z∈BaseH|βˆƒk∈01z-Hx=kβ‹…Hy-HxsSetLine𝒒⁑ndxx∈BaseH,y∈BaseH⟼z∈BaseH|z∈xItv⁑Gy∨x∈zItv⁑Gy∨y∈xItv⁑Gz
14 13 fveq2d ⊒H∈Vβ†’E⁑G=E⁑HsSetItv⁑ndxx∈BaseH,y∈BaseH⟼z∈BaseH|βˆƒk∈01z-Hx=kβ‹…Hy-HxsSetLine𝒒⁑ndxx∈BaseH,y∈BaseH⟼z∈BaseH|z∈xItv⁑Gy∨x∈zItv⁑Gy∨y∈xItv⁑Gz
15 7 14 eqtr4id ⊒H∈Vβ†’E⁑H=E⁑G
16 2 str0 βŠ’βˆ…=Eβ‘βˆ…
17 16 eqcomi ⊒Eβ‘βˆ…=βˆ…
18 17 1 fveqprc ⊒¬H∈Vβ†’E⁑H=E⁑G
19 15 18 pm2.61i ⊒E⁑H=E⁑G