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 41960

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 2760	. . . 4 ⊢ ((EDRing‘𝐾)‘𝑊) = ((EDRing‘𝐾)‘𝑊)
5		dvhvbase.u	. . . 4 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
6	1, 2, 3, 4, 5	dvhset 41954	. . 3 ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → 𝑈 = ({⟨(Base‘ndx), (𝑇 × 𝐸)⟩, ⟨(+_g‘ndx), (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ ⟨((1^st ‘𝑓) ∘ (1^st ‘𝑔)), (ℎ ∈ 𝑇 ↦ (((2^nd ‘𝑓)‘ℎ) ∘ ((2^nd ‘𝑔)‘ℎ)))⟩)⟩, ⟨(Scalar‘ndx), ((EDRing‘𝐾)‘𝑊)⟩} ∪ {⟨( ·_𝑠 ‘ndx), (𝑠 ∈ 𝐸, 𝑓 ∈ (𝑇 × 𝐸) ↦ ⟨(𝑠‘(1^st ‘𝑓)), (𝑠 ∘ (2^nd ‘𝑓))⟩)⟩}))
7	6	fveq2d 6882	. 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 6892	. . . 4 ⊢ 𝑇 ∈ V
10	3	fvexi 6892	. . . 4 ⊢ 𝐸 ∈ V
11	9, 10	xpex 7752	. . 3 ⊢ (𝑇 × 𝐸) ∈ V
12		eqid 2760	. . . 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 17411	. . 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 2820	1 ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → 𝑉 = (𝑇 × 𝐸))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2145 Vcvv 3450 ∪ cun 3897 {csn 4584 {ctp 4588 ⟨cop 4590 ↦ cmpt 5186 × cxp 5653 ∘ ccom 5659 ‘cfv 6533 ∈ cmpo 7415 1^st c1st 7984 2^nd c2nd 7985 ndxcnx 17285 Basecbs 17301 +_gcplusg 17342 Scalarcsca 17345 ·_𝑠 cvsca 17346 LHypclh 40857 LTrncltrn 40974 TEndoctendo 41625 EDRingcedring 41626 DVecHcdvh 41951

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7736 ax-cnex 11180 ax-resscn 11181 ax-1cn 11182 ax-icn 11183 ax-addcl 11184 ax-addrcl 11185 ax-mulcl 11186 ax-mulrcl 11187 ax-mulcom 11188 ax-addass 11189 ax-mulass 11190 ax-distr 11191 ax-i2m1 11192 ax-1ne0 11193 ax-1rid 11194 ax-rnegex 11195 ax-rrecex 11196 ax-cnre 11197 ax-pre-lttri 11198 ax-pre-lttrn 11199 ax-pre-ltadd 11200 ax-pre-mulgt0 11201

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-om 7863 df-1st 7986 df-2nd 7987 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-1o 8455 df-er 8696 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-pnf 11269 df-mnf 11270 df-xr 11271 df-ltxr 11272 df-le 11273 df-sub 11467 df-neg 11468 df-nn 12258 df-2 12327 df-3 12328 df-4 12329 df-5 12330 df-6 12331 df-n0 12529 df-z 12616 df-uz 12888 df-fz 13562 df-struct 17239 df-slot 17274 df-ndx 17286 df-base 17302 df-plusg 17355 df-sca 17358 df-vsca 17359 df-dvech 41952

This theorem is used by: dvhelvbasei 41961 dvhgrp 41980 dvhlveclem 41981 dvhopellsm 41990 dibss 42042 diblss 42043 dicssdvh 42059 dicelval1stN 42061 dicelval2nd 42062 dicvaddcl 42063 dicvscacl 42064 diclss 42066 dihssxp 42125 dihvalrel 42152 dih1 42159 dih1dimatlem 42202

W3C validator