dvhvbase - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dvhvbase		Structured version Visualization version GIF version

Theorem dvhvbase 41126

Description: The vectors (vector base set) of the constructed full vector space H are all translations (for a fiducial co-atom 𝑊). (Contributed by NM, 2-Nov-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)

**Hypotheses**
Ref	Expression
dvhvbase.h	⊢ 𝐻 = (LHyp‘𝐾)
dvhvbase.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
dvhvbase.e	⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
dvhvbase.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
dvhvbase.v	⊢ 𝑉 = (Base‘𝑈)

**Assertion**
Ref	Expression
dvhvbase	⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → 𝑉 = (𝑇 × 𝐸))

Proof of Theorem dvhvbase Dummy variables 𝑓 𝑔 ℎ 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dvhvbase.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
2		dvhvbase.t	. . . 4 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
3		dvhvbase.e	. . . 4 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
4		eqid 2731	. . . 4 ⊢ ((EDRing‘𝐾)‘𝑊) = ((EDRing‘𝐾)‘𝑊)
5		dvhvbase.u	. . . 4 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
6	1, 2, 3, 4, 5	dvhset 41120	. . 3 ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → 𝑈 = ({⟨(Base‘ndx), (𝑇 × 𝐸)⟩, ⟨(+_g‘ndx), (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ ⟨((1^st ‘𝑓) ∘ (1^st ‘𝑔)), (ℎ ∈ 𝑇 ↦ (((2^nd ‘𝑓)‘ℎ) ∘ ((2^nd ‘𝑔)‘ℎ)))⟩)⟩, ⟨(Scalar‘ndx), ((EDRing‘𝐾)‘𝑊)⟩} ∪ {⟨( ·_𝑠 ‘ndx), (𝑠 ∈ 𝐸, 𝑓 ∈ (𝑇 × 𝐸) ↦ ⟨(𝑠‘(1^st ‘𝑓)), (𝑠 ∘ (2^nd ‘𝑓))⟩)⟩}))
7	6	fveq2d 6821	. 2 ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → (Base‘𝑈) = (Base‘({⟨(Base‘ndx), (𝑇 × 𝐸)⟩, ⟨(+_g‘ndx), (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ ⟨((1^st ‘𝑓) ∘ (1^st ‘𝑔)), (ℎ ∈ 𝑇 ↦ (((2^nd ‘𝑓)‘ℎ) ∘ ((2^nd ‘𝑔)‘ℎ)))⟩)⟩, ⟨(Scalar‘ndx), ((EDRing‘𝐾)‘𝑊)⟩} ∪ {⟨( ·_𝑠 ‘ndx), (𝑠 ∈ 𝐸, 𝑓 ∈ (𝑇 × 𝐸) ↦ ⟨(𝑠‘(1^st ‘𝑓)), (𝑠 ∘ (2^nd ‘𝑓))⟩)⟩})))
8		dvhvbase.v	. 2 ⊢ 𝑉 = (Base‘𝑈)
9	2	fvexi 6831	. . . 4 ⊢ 𝑇 ∈ V
10	3	fvexi 6831	. . . 4 ⊢ 𝐸 ∈ V
11	9, 10	xpex 7681	. . 3 ⊢ (𝑇 × 𝐸) ∈ V
12		eqid 2731	. . . 4 ⊢ ({⟨(Base‘ndx), (𝑇 × 𝐸)⟩, ⟨(+_g‘ndx), (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ ⟨((1^st ‘𝑓) ∘ (1^st ‘𝑔)), (ℎ ∈ 𝑇 ↦ (((2^nd ‘𝑓)‘ℎ) ∘ ((2^nd ‘𝑔)‘ℎ)))⟩)⟩, ⟨(Scalar‘ndx), ((EDRing‘𝐾)‘𝑊)⟩} ∪ {⟨( ·_𝑠 ‘ndx), (𝑠 ∈ 𝐸, 𝑓 ∈ (𝑇 × 𝐸) ↦ ⟨(𝑠‘(1^st ‘𝑓)), (𝑠 ∘ (2^nd ‘𝑓))⟩)⟩}) = ({⟨(Base‘ndx), (𝑇 × 𝐸)⟩, ⟨(+_g‘ndx), (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ ⟨((1^st ‘𝑓) ∘ (1^st ‘𝑔)), (ℎ ∈ 𝑇 ↦ (((2^nd ‘𝑓)‘ℎ) ∘ ((2^nd ‘𝑔)‘ℎ)))⟩)⟩, ⟨(Scalar‘ndx), ((EDRing‘𝐾)‘𝑊)⟩} ∪ {⟨( ·_𝑠 ‘ndx), (𝑠 ∈ 𝐸, 𝑓 ∈ (𝑇 × 𝐸) ↦ ⟨(𝑠‘(1^st ‘𝑓)), (𝑠 ∘ (2^nd ‘𝑓))⟩)⟩})
13	12	lmodbase 17225	. . 3 ⊢ ((𝑇 × 𝐸) ∈ V → (𝑇 × 𝐸) = (Base‘({⟨(Base‘ndx), (𝑇 × 𝐸)⟩, ⟨(+_g‘ndx), (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ ⟨((1^st ‘𝑓) ∘ (1^st ‘𝑔)), (ℎ ∈ 𝑇 ↦ (((2^nd ‘𝑓)‘ℎ) ∘ ((2^nd ‘𝑔)‘ℎ)))⟩)⟩, ⟨(Scalar‘ndx), ((EDRing‘𝐾)‘𝑊)⟩} ∪ {⟨( ·_𝑠 ‘ndx), (𝑠 ∈ 𝐸, 𝑓 ∈ (𝑇 × 𝐸) ↦ ⟨(𝑠‘(1^st ‘𝑓)), (𝑠 ∘ (2^nd ‘𝑓))⟩)⟩})))
14	11, 13	ax-mp 5	. 2 ⊢ (𝑇 × 𝐸) = (Base‘({⟨(Base‘ndx), (𝑇 × 𝐸)⟩, ⟨(+_g‘ndx), (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ ⟨((1^st ‘𝑓) ∘ (1^st ‘𝑔)), (ℎ ∈ 𝑇 ↦ (((2^nd ‘𝑓)‘ℎ) ∘ ((2^nd ‘𝑔)‘ℎ)))⟩)⟩, ⟨(Scalar‘ndx), ((EDRing‘𝐾)‘𝑊)⟩} ∪ {⟨( ·_𝑠 ‘ndx), (𝑠 ∈ 𝐸, 𝑓 ∈ (𝑇 × 𝐸) ↦ ⟨(𝑠‘(1^st ‘𝑓)), (𝑠 ∘ (2^nd ‘𝑓))⟩)⟩}))
15	7, 8, 14	3eqtr4g 2791	1 ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → 𝑉 = (𝑇 × 𝐸))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1541 ∈ wcel 2111 Vcvv 3436 ∪ cun 3895 {csn 4571 {ctp 4575 ⟨cop 4577 ↦ cmpt 5167 × cxp 5609 ∘ ccom 5615 ‘cfv 6476 ∈ cmpo 7343 1^st c1st 7914 2^nd c2nd 7915 ndxcnx 17099 Basecbs 17115 +_gcplusg 17156 Scalarcsca 17159 ·_𝑠 cvsca 17160 LHypclh 40023 LTrncltrn 40140 TEndoctendo 40791 EDRingcedring 40792 DVecHcdvh 41117

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5212 ax-sep 5229 ax-nul 5239 ax-pow 5298 ax-pr 5365 ax-un 7663 ax-cnex 11057 ax-resscn 11058 ax-1cn 11059 ax-icn 11060 ax-addcl 11061 ax-addrcl 11062 ax-mulcl 11063 ax-mulrcl 11064 ax-mulcom 11065 ax-addass 11066 ax-mulass 11067 ax-distr 11068 ax-i2m1 11069 ax-1ne0 11070 ax-1rid 11071 ax-rnegex 11072 ax-rrecex 11073 ax-cnre 11074 ax-pre-lttri 11075 ax-pre-lttrn 11076 ax-pre-ltadd 11077 ax-pre-mulgt0 11078

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4279 df-if 4471 df-pw 4547 df-sn 4572 df-pr 4574 df-tp 4576 df-op 4578 df-uni 4855 df-iun 4938 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5506 df-eprel 5511 df-po 5519 df-so 5520 df-fr 5564 df-we 5566 df-xp 5617 df-rel 5618 df-cnv 5619 df-co 5620 df-dm 5621 df-rn 5622 df-res 5623 df-ima 5624 df-pred 6243 df-ord 6304 df-on 6305 df-lim 6306 df-suc 6307 df-iota 6432 df-fun 6478 df-fn 6479 df-f 6480 df-f1 6481 df-fo 6482 df-f1o 6483 df-fv 6484 df-riota 7298 df-ov 7344 df-oprab 7345 df-mpo 7346 df-om 7792 df-1st 7916 df-2nd 7917 df-frecs 8206 df-wrecs 8237 df-recs 8286 df-rdg 8324 df-1o 8380 df-er 8617 df-en 8865 df-dom 8866 df-sdom 8867 df-fin 8868 df-pnf 11143 df-mnf 11144 df-xr 11145 df-ltxr 11146 df-le 11147 df-sub 11341 df-neg 11342 df-nn 12121 df-2 12183 df-3 12184 df-4 12185 df-5 12186 df-6 12187 df-n0 12377 df-z 12464 df-uz 12728 df-fz 13403 df-struct 17053 df-slot 17088 df-ndx 17100 df-base 17116 df-plusg 17169 df-sca 17172 df-vsca 17173 df-dvech 41118

This theorem is referenced by: dvhelvbasei 41127 dvhgrp 41146 dvhlveclem 41147 dvhopellsm 41156 dibss 41208 diblss 41209 dicssdvh 41225 dicelval1stN 41227 dicelval2nd 41228 dicvaddcl 41229 dicvscacl 41230 diclss 41232 dihssxp 41291 dihvalrel 41318 dih1 41325 dih1dimatlem 41368

W3C validator