Theorem tnglem

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

	Ref	Expression
Hypotheses	tngbas.t	⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
	tnglem.2	⊢ 𝐸 = Slot 𝐾
	tnglem.3	⊢ 𝐾 ∈ ℕ
	tnglem.4	⊢ 𝐾 < 9
Assertion	tnglem	⊢ ( 𝑁 ∈ 𝑉 → ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		tngbas.t	⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2		tnglem.2	⊢ 𝐸 = Slot 𝐾
3		tnglem.3	⊢ 𝐾 ∈ ℕ
4		tnglem.4	⊢ 𝐾 < 9
5	2 3	ndxid	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
6	2 3	ndxarg	⊢ ( 𝐸 ‘ ndx ) = 𝐾
7	3	nnrei	⊢ 𝐾 ∈ ℝ
8	6 7	eqeltri	⊢ ( 𝐸 ‘ ndx ) ∈ ℝ
9	6 4	eqbrtri	⊢ ( 𝐸 ‘ ndx ) < 9
10		1nn	⊢ 1 ∈ ℕ
11		2nn0	⊢ 2 ∈ ℕ0
12		9nn0	⊢ 9 ∈ ℕ0
13		9lt10	⊢ 9 < ; 1 0
14	10 11 12 13	declti	⊢ 9 < ; 1 2
15		9re	⊢ 9 ∈ ℝ
16		1nn0	⊢ 1 ∈ ℕ0
17	16 11	deccl	⊢ ; 1 2 ∈ ℕ0
18	17	nn0rei	⊢ ; 1 2 ∈ ℝ
19	8 15 18	lttri	⊢ ( ( ( 𝐸 ‘ ndx ) < 9 ∧ 9 < ; 1 2 ) → ( 𝐸 ‘ ndx ) < ; 1 2 )
20	9 14 19	mp2an	⊢ ( 𝐸 ‘ ndx ) < ; 1 2
21	8 20	ltneii	⊢ ( 𝐸 ‘ ndx ) ≠ ; 1 2
22		dsndx	⊢ ( dist ‘ ndx ) = ; 1 2
23	21 22	neeqtrri	⊢ ( 𝐸 ‘ ndx ) ≠ ( dist ‘ ndx )
24	5 23	setsnid	⊢ ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ⟩ ) )
25	8 9	ltneii	⊢ ( 𝐸 ‘ ndx ) ≠ 9
26		tsetndx	⊢ ( TopSet ‘ ndx ) = 9
27	25 26	neeqtrri	⊢ ( 𝐸 ‘ ndx ) ≠ ( TopSet ‘ ndx )
28	5 27	setsnid	⊢ ( 𝐸 ‘ ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ⟩ ) ) = ( 𝐸 ‘ ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ) ⟩ ) )
29	24 28	eqtri	⊢ ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ) ⟩ ) )
30		eqid	⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
31		eqid	⊢ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) = ( 𝑁 ∘ ( -g ‘ 𝐺 ) )
32		eqid	⊢ ( MetOpen ‘ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ) = ( MetOpen ‘ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) )
33	1 30 31 32	tngval	⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → 𝑇 = ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ) ⟩ ) )
34	33	fveq2d	⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑇 ) = ( 𝐸 ‘ ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ) ⟩ ) ) )
35	29 34	eqtr4id	⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ 𝑇 ) )
36	2	str0	⊢ ∅ = ( 𝐸 ‘ ∅ )
37		fvprc	⊢ ( ¬ 𝐺 ∈ V → ( 𝐸 ‘ 𝐺 ) = ∅ )
38	37	adantr	⊢ ( ( ¬ 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → ( 𝐸 ‘ 𝐺 ) = ∅ )
39		reldmtng	⊢ Rel dom toNrmGrp
40	39	ovprc1	⊢ ( ¬ 𝐺 ∈ V → ( 𝐺 toNrmGrp 𝑁 ) = ∅ )
41	40	adantr	⊢ ( ( ¬ 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 toNrmGrp 𝑁 ) = ∅ )
42	1 41	syl5eq	⊢ ( ( ¬ 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → 𝑇 = ∅ )
43	42	fveq2d	⊢ ( ( ¬ 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑇 ) = ( 𝐸 ‘ ∅ ) )
44	36 38 43	3eqtr4a	⊢ ( ( ¬ 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ 𝑇 ) )
45	35 44	pm2.61ian	⊢ ( 𝑁 ∈ 𝑉 → ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ 𝑇 ) )