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	⊢ ( 𝑁 ∈ 𝑉 → ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ 𝑇 ) )