Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  tnglem Structured version   Visualization version   GIF version

Theorem tnglem 23347
 Description: Lemma for tngbas 23348 and similar theorems. (Contributed by Mario Carneiro, 2-Oct-2015.)
Hypotheses
Ref Expression
tngbas.t 𝑇 = (𝐺 toNrmGrp 𝑁)
tnglem.2 𝐸 = Slot 𝐾
tnglem.3 𝐾 ∈ ℕ
tnglem.4 𝐾 < 9
Assertion
Ref Expression
tnglem (𝑁𝑉 → (𝐸𝐺) = (𝐸𝑇))

Proof of Theorem tnglem
StepHypRef Expression
1 tnglem.2 . . . . . 6 𝐸 = Slot 𝐾
2 tnglem.3 . . . . . 6 𝐾 ∈ ℕ
31, 2ndxid 16572 . . . . 5 𝐸 = Slot (𝐸‘ndx)
41, 2ndxarg 16571 . . . . . . . 8 (𝐸‘ndx) = 𝐾
52nnrei 11688 . . . . . . . 8 𝐾 ∈ ℝ
64, 5eqeltri 2848 . . . . . . 7 (𝐸‘ndx) ∈ ℝ
7 tnglem.4 . . . . . . . . 9 𝐾 < 9
84, 7eqbrtri 5056 . . . . . . . 8 (𝐸‘ndx) < 9
9 1nn 11690 . . . . . . . . 9 1 ∈ ℕ
10 2nn0 11956 . . . . . . . . 9 2 ∈ ℕ0
11 9nn0 11963 . . . . . . . . 9 9 ∈ ℕ0
12 9lt10 12273 . . . . . . . . 9 9 < 10
139, 10, 11, 12declti 12180 . . . . . . . 8 9 < 12
14 9re 11778 . . . . . . . . 9 9 ∈ ℝ
15 1nn0 11955 . . . . . . . . . . 11 1 ∈ ℕ0
1615, 10deccl 12157 . . . . . . . . . 10 12 ∈ ℕ0
1716nn0rei 11950 . . . . . . . . 9 12 ∈ ℝ
186, 14, 17lttri 10809 . . . . . . . 8 (((𝐸‘ndx) < 9 ∧ 9 < 12) → (𝐸‘ndx) < 12)
198, 13, 18mp2an 691 . . . . . . 7 (𝐸‘ndx) < 12
206, 19ltneii 10796 . . . . . 6 (𝐸‘ndx) ≠ 12
21 dsndx 16738 . . . . . 6 (dist‘ndx) = 12
2220, 21neeqtrri 3024 . . . . 5 (𝐸‘ndx) ≠ (dist‘ndx)
233, 22setsnid 16602 . . . 4 (𝐸𝐺) = (𝐸‘(𝐺 sSet ⟨(dist‘ndx), (𝑁 ∘ (-g𝐺))⟩))
246, 8ltneii 10796 . . . . . 6 (𝐸‘ndx) ≠ 9
25 tsetndx 16722 . . . . . 6 (TopSet‘ndx) = 9
2624, 25neeqtrri 3024 . . . . 5 (𝐸‘ndx) ≠ (TopSet‘ndx)
273, 26setsnid 16602 . . . 4 (𝐸‘(𝐺 sSet ⟨(dist‘ndx), (𝑁 ∘ (-g𝐺))⟩)) = (𝐸‘((𝐺 sSet ⟨(dist‘ndx), (𝑁 ∘ (-g𝐺))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑁 ∘ (-g𝐺)))⟩))
2823, 27eqtri 2781 . . 3 (𝐸𝐺) = (𝐸‘((𝐺 sSet ⟨(dist‘ndx), (𝑁 ∘ (-g𝐺))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑁 ∘ (-g𝐺)))⟩))
29 tngbas.t . . . . 5 𝑇 = (𝐺 toNrmGrp 𝑁)
30 eqid 2758 . . . . 5 (-g𝐺) = (-g𝐺)
31 eqid 2758 . . . . 5 (𝑁 ∘ (-g𝐺)) = (𝑁 ∘ (-g𝐺))
32 eqid 2758 . . . . 5 (MetOpen‘(𝑁 ∘ (-g𝐺))) = (MetOpen‘(𝑁 ∘ (-g𝐺)))
3329, 30, 31, 32tngval 23346 . . . 4 ((𝐺 ∈ V ∧ 𝑁𝑉) → 𝑇 = ((𝐺 sSet ⟨(dist‘ndx), (𝑁 ∘ (-g𝐺))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑁 ∘ (-g𝐺)))⟩))
3433fveq2d 6666 . . 3 ((𝐺 ∈ V ∧ 𝑁𝑉) → (𝐸𝑇) = (𝐸‘((𝐺 sSet ⟨(dist‘ndx), (𝑁 ∘ (-g𝐺))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑁 ∘ (-g𝐺)))⟩)))
3528, 34eqtr4id 2812 . 2 ((𝐺 ∈ V ∧ 𝑁𝑉) → (𝐸𝐺) = (𝐸𝑇))
361str0 16598 . . 3 ∅ = (𝐸‘∅)
37 fvprc 6654 . . . 4 𝐺 ∈ V → (𝐸𝐺) = ∅)
3837adantr 484 . . 3 ((¬ 𝐺 ∈ V ∧ 𝑁𝑉) → (𝐸𝐺) = ∅)
39 reldmtng 23345 . . . . . . 7 Rel dom toNrmGrp
4039ovprc1 7194 . . . . . 6 𝐺 ∈ V → (𝐺 toNrmGrp 𝑁) = ∅)
4140adantr 484 . . . . 5 ((¬ 𝐺 ∈ V ∧ 𝑁𝑉) → (𝐺 toNrmGrp 𝑁) = ∅)
4229, 41syl5eq 2805 . . . 4 ((¬ 𝐺 ∈ V ∧ 𝑁𝑉) → 𝑇 = ∅)
4342fveq2d 6666 . . 3 ((¬ 𝐺 ∈ V ∧ 𝑁𝑉) → (𝐸𝑇) = (𝐸‘∅))
4436, 38, 433eqtr4a 2819 . 2 ((¬ 𝐺 ∈ V ∧ 𝑁𝑉) → (𝐸𝐺) = (𝐸𝑇))
4535, 44pm2.61ian 811 1 (𝑁𝑉 → (𝐸𝐺) = (𝐸𝑇))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  Vcvv 3409  ∅c0 4227  ⟨cop 4531   class class class wbr 5035   ∘ ccom 5531  ‘cfv 6339  (class class class)co 7155  ℝcr 10579  1c1 10581   < clt 10718  ℕcn 11679  2c2 11734  9c9 11741  ;cdc 12142  ndxcnx 16543   sSet csts 16544  Slot cslot 16545  TopSetcts 16634  distcds 16637  -gcsg 18176  MetOpencmopn 20161   toNrmGrp ctng 23285 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5172  ax-nul 5179  ax-pow 5237  ax-pr 5301  ax-un 7464  ax-cnex 10636  ax-resscn 10637  ax-1cn 10638  ax-icn 10639  ax-addcl 10640  ax-addrcl 10641  ax-mulcl 10642  ax-mulrcl 10643  ax-mulcom 10644  ax-addass 10645  ax-mulass 10646  ax-distr 10647  ax-i2m1 10648  ax-1ne0 10649  ax-1rid 10650  ax-rnegex 10651  ax-rrecex 10652  ax-cnre 10653  ax-pre-lttri 10654  ax-pre-lttrn 10655  ax-pre-ltadd 10656  ax-pre-mulgt0 10657 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-iun 4888  df-br 5036  df-opab 5098  df-mpt 5116  df-tr 5142  df-id 5433  df-eprel 5438  df-po 5446  df-so 5447  df-fr 5486  df-we 5488  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-riota 7113  df-ov 7158  df-oprab 7159  df-mpo 7160  df-om 7585  df-wrecs 7962  df-recs 8023  df-rdg 8061  df-er 8304  df-en 8533  df-dom 8534  df-sdom 8535  df-pnf 10720  df-mnf 10721  df-xr 10722  df-ltxr 10723  df-le 10724  df-sub 10915  df-neg 10916  df-nn 11680  df-2 11742  df-3 11743  df-4 11744  df-5 11745  df-6 11746  df-7 11747  df-8 11748  df-9 11749  df-n0 11940  df-z 12026  df-dec 12143  df-ndx 16549  df-slot 16550  df-sets 16553  df-tset 16647  df-ds 16650  df-tng 23291 This theorem is referenced by:  tngbas  23348  tngplusg  23349  tngmulr  23351  tngsca  23352  tngvsca  23353  tngip  23354
 Copyright terms: Public domain W3C validator