This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
tnglem.e ⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
tnglem.t ⊢ ( 𝐸 ‘ ndx ) ≠ ( TopSet ‘ ndx )
tnglem.d ⊢ ( 𝐸 ‘ ndx ) ≠ ( dist ‘ ndx )
Assertion tnglem ( 𝑁 ∈ 𝑉 → ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 tngbas.t ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2 tnglem.e ⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
3 tnglem.t ⊢ ( 𝐸 ‘ ndx ) ≠ ( TopSet ‘ ndx )
4 tnglem.d ⊢ ( 𝐸 ‘ ndx ) ≠ ( dist ‘ ndx )
5 2 4 setsnid ⊢ ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ⟩ ) )
6 2 3 setsnid ⊢ ( 𝐸 ‘ ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ⟩ ) ) = ( 𝐸 ‘ ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ) ⟩ ) )
7 5 6 eqtri ⊢ ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ) ⟩ ) )
8 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
9 eqid ⊢ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) = ( 𝑁 ∘ ( -g ‘ 𝐺 ) )
10 eqid ⊢ ( MetOpen ‘ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ) = ( MetOpen ‘ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) )
11 1 8 9 10 tngval ⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → 𝑇 = ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ) ⟩ ) )
12 11 fveq2d ⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑇 ) = ( 𝐸 ‘ ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ) ⟩ ) ) )
13 7 12 eqtr4id ⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ 𝑇 ) )
14 2 str0 ⊢ ∅ = ( 𝐸 ‘ ∅ )
15 14 eqcomi ⊢ ( 𝐸 ‘ ∅ ) = ∅
16 reldmtng ⊢ Rel dom toNrmGrp
17 15 1 16 oveqprc ⊢ ( ¬ 𝐺 ∈ V → ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ 𝑇 ) )
18 17 adantr ⊢ ( ( ¬ 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ 𝑇 ) )
19 13 18 pm2.61ian ⊢ ( 𝑁 ∈ 𝑉 → ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ 𝑇 ) )