Metamath Proof Explorer

Theorem tnglem

Description: Lemma for tngbas and similar theorems. (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by AV, 31-Oct-2024)

Ref Expression
Hypotheses tngbas.t ⊢ T = G toNrmGrp N
tnglem.e ⊢ E = Slot E ⁡ ndx
tnglem.t ⊢ E ⁡ ndx ≠ TopSet ⁡ ndx
tnglem.d ⊢ E ⁡ ndx ≠ dist ⁡ ndx
Assertion tnglem ⊢ N ∈ V → E ⁡ G = E ⁡ T

Proof

Step Hyp Ref Expression
1 tngbas.t ⊢ T = G toNrmGrp N
2 tnglem.e ⊢ E = Slot E ⁡ ndx
3 tnglem.t ⊢ E ⁡ ndx ≠ TopSet ⁡ ndx
4 tnglem.d ⊢ E ⁡ ndx ≠ dist ⁡ ndx
5 2 4 setsnid ⊢ E ⁡ G = E ⁡ G sSet dist ⁡ ndx N ∘ - G
6 2 3 setsnid ⊢ E ⁡ G sSet dist ⁡ ndx N ∘ - G = E ⁡ G sSet dist ⁡ ndx N ∘ - G sSet TopSet ⁡ ndx MetOpen ⁡ N ∘ - G
7 5 6 eqtri ⊢ E ⁡ G = E ⁡ G sSet dist ⁡ ndx N ∘ - G sSet TopSet ⁡ ndx MetOpen ⁡ N ∘ - G
8 eqid ⊢ - G = - G
9 eqid ⊢ N ∘ - G = N ∘ - G
10 eqid ⊢ MetOpen ⁡ N ∘ - G = MetOpen ⁡ N ∘ - G
11 1 8 9 10 tngval ⊢ G ∈ V ∧ N ∈ V → T = G sSet dist ⁡ ndx N ∘ - G sSet TopSet ⁡ ndx MetOpen ⁡ N ∘ - G
12 11 fveq2d ⊢ G ∈ V ∧ N ∈ V → E ⁡ T = E ⁡ G sSet dist ⁡ ndx N ∘ - G sSet TopSet ⁡ ndx MetOpen ⁡ N ∘ - G
13 7 12 eqtr4id ⊢ G ∈ V ∧ N ∈ V → E ⁡ G = E ⁡ T
14 2 str0 ⊢ ∅ = E ⁡ ∅
15 14 eqcomi ⊢ E ⁡ ∅ = ∅
16 reldmtng ⊢ Rel ⁡ dom ⁡ toNrmGrp
17 15 1 16 oveqprc ⊢ ¬ G ∈ V → E ⁡ G = E ⁡ T
18 17 adantr ⊢ ¬ G ∈ V ∧ N ∈ V → E ⁡ G = E ⁡ T
19 13 18 pm2.61ian ⊢ N ∈ V → E ⁡ G = E ⁡ T