Theorem tnglem

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

	Ref	Expression
Hypotheses	tngbas.t	$$⊢T=G\mathrm{toNrmGrp}N$$
	tnglem.2	$$⊢E=\mathrm{Slot}K$$
	tnglem.3	$$⊢K\in \mathbb{N}$$
	tnglem.4	$$⊢K<9$$
Assertion	tnglem	$$⊢N\in V\to E\left(G\right)=E\left(T\right)$$

Proof

Step	Hyp	Ref	Expression
1		tngbas.t	$$⊢T=G\mathrm{toNrmGrp}N$$
2		tnglem.2	$$⊢E=\mathrm{Slot}K$$
3		tnglem.3	$$⊢K\in \mathbb{N}$$
4		tnglem.4	$$⊢K<9$$
5	2 3	ndxid	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
6	2 3	ndxarg	$$⊢E\left(\mathrm{ndx}\right)=K$$
7	3	nnrei	$$⊢K\in ℝ$$
8	6 7	eqeltri	$$⊢E\left(\mathrm{ndx}\right)\in ℝ$$
9	6 4	eqbrtri	$$⊢E\left(\mathrm{ndx}\right)<9$$
10		1nn	$$⊢1\in \mathbb{N}$$
11		2nn0	$$⊢2\in {\mathbb{N}}_0$$
12		9nn0	$$⊢9\in {\mathbb{N}}_0$$
13		9lt10	$$⊢9<10$$
14	10 11 12 13	declti	$$⊢9<12$$
15		9re	$$⊢9\in ℝ$$
16		1nn0	$$⊢1\in {\mathbb{N}}_0$$
17	16 11	deccl	$$⊢12\in {\mathbb{N}}_0$$
18	17	nn0rei	$$⊢12\in ℝ$$
19	8 15 18	lttri	$$⊢\left(E\left(\mathrm{ndx}\right)<9\wedge 9<12\right)\to E\left(\mathrm{ndx}\right)<12$$
20	9 14 19	mp2an	$$⊢E\left(\mathrm{ndx}\right)<12$$
21	8 20	ltneii	$$⊢E\left(\mathrm{ndx}\right)\ne 12$$
22		dsndx	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)=12$$
23	21 22	neeqtrri	$$⊢E\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
24	5 23	setsnid	$$⊢E\left(G\right)=E\left(G\mathrm{sSet}⟨\mathrm{dist}\left(\mathrm{ndx}\right),N\circ {-}_G⟩\right)$$
25	8 9	ltneii	$$⊢E\left(\mathrm{ndx}\right)\ne 9$$
26		tsetndx	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)=9$$
27	25 26	neeqtrri	$$⊢E\left(\mathrm{ndx}\right)\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
28	5 27	setsnid	$$⊢E\left(G\mathrm{sSet}⟨\mathrm{dist}\left(\mathrm{ndx}\right),N\circ {-}_G⟩\right)=E\left(\left(G\mathrm{sSet}⟨\mathrm{dist}\left(\mathrm{ndx}\right),N\circ {-}_G⟩\right)\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(N\circ {-}_G\right)⟩\right)$$
29	24 28	eqtri	$$⊢E\left(G\right)=E\left(\left(G\mathrm{sSet}⟨\mathrm{dist}\left(\mathrm{ndx}\right),N\circ {-}_G⟩\right)\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(N\circ {-}_G\right)⟩\right)$$
30		eqid	$$⊢{-}_G={-}_G$$
31		eqid	$$⊢N\circ {-}_G=N\circ {-}_G$$
32		eqid	$$⊢\mathrm{MetOpen}\left(N\circ {-}_G\right)=\mathrm{MetOpen}\left(N\circ {-}_G\right)$$
33	1 30 31 32	tngval	$$⊢\left(G\in \mathrm{V}\wedge N\in V\right)\to T=\left(G\mathrm{sSet}⟨\mathrm{dist}\left(\mathrm{ndx}\right),N\circ {-}_G⟩\right)\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(N\circ {-}_G\right)⟩$$
34	33	fveq2d	$$⊢\left(G\in \mathrm{V}\wedge N\in V\right)\to E\left(T\right)=E\left(\left(G\mathrm{sSet}⟨\mathrm{dist}\left(\mathrm{ndx}\right),N\circ {-}_G⟩\right)\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(N\circ {-}_G\right)⟩\right)$$
35	29 34	eqtr4id	$$⊢\left(G\in \mathrm{V}\wedge N\in V\right)\to E\left(G\right)=E\left(T\right)$$
36	2	str0	$$⊢\varnothing =E\left(\varnothing \right)$$
37		fvprc	$$⊢\neg G\in \mathrm{V}\to E\left(G\right)=\varnothing$$
38	37	adantr	$$⊢\left(\neg G\in \mathrm{V}\wedge N\in V\right)\to E\left(G\right)=\varnothing$$
39		reldmtng	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{toNrmGrp}$$
40	39	ovprc1	$$⊢\neg G\in \mathrm{V}\to G\mathrm{toNrmGrp}N=\varnothing$$
41	40	adantr	$$⊢\left(\neg G\in \mathrm{V}\wedge N\in V\right)\to G\mathrm{toNrmGrp}N=\varnothing$$
42	1 41	syl5eq	$$⊢\left(\neg G\in \mathrm{V}\wedge N\in V\right)\to T=\varnothing$$
43	42	fveq2d	$$⊢\left(\neg G\in \mathrm{V}\wedge N\in V\right)\to E\left(T\right)=E\left(\varnothing \right)$$
44	36 38 43	3eqtr4a	$$⊢\left(\neg G\in \mathrm{V}\wedge N\in V\right)\to E\left(G\right)=E\left(T\right)$$
45	35 44	pm2.61ian	$$⊢N\in V\to E\left(G\right)=E\left(T\right)$$