mapdrvallem3 - Mathbox for Norm Megill

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

Theorem mapdrvallem3 37421

Description: Lemma for mapdrval 37422. (Contributed by NM, 2-Feb-2015.)

**Hypotheses**
Ref	Expression
mapdrval.h	⊢ 𝐻 = (LHyp‘𝐾)
mapdrval.o	⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)
mapdrval.m	⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
mapdrval.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
mapdrval.s	⊢ 𝑆 = (LSubSp‘𝑈)
mapdrval.f	⊢ 𝐹 = (LFnl‘𝑈)
mapdrval.l	⊢ 𝐿 = (LKer‘𝑈)
mapdrval.d	⊢ 𝐷 = (LDual‘𝑈)
mapdrval.t	⊢ 𝑇 = (LSubSp‘𝐷)
mapdrval.c	⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)}
mapdrval.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
mapdrval.r	⊢ (𝜑 → 𝑅 ∈ 𝑇)
mapdrval.e	⊢ (𝜑 → 𝑅 ⊆ 𝐶)
mapdrval.q	⊢ 𝑄 = ∪ ℎ ∈ 𝑅 (𝑂‘(𝐿‘ℎ))
mapdrval.v	⊢ 𝑉 = (Base‘𝑈)
mapdrvallem2.a	⊢ 𝐴 = (LSAtoms‘𝑈)
mapdrvallem2.n	⊢ 𝑁 = (LSpan‘𝑈)
mapdrvallem2.z	⊢ 0 = (0_g‘𝑈)
mapdrvallem2.y	⊢ 𝑌 = (0_g‘𝐷)

**Assertion**
Ref	Expression
mapdrvallem3	⊢ (𝜑 → {𝑓 ∈ 𝐶 ∣ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑄} = 𝑅)

Distinct variable groups: 𝐶,𝑓 𝑓,𝑔,𝐹 𝑓,𝐾 𝑔,ℎ,𝐿 𝑔,𝑂,ℎ 𝑄,𝑓,ℎ 𝑅,𝑓,ℎ 𝑈,𝑔 𝑓,𝑊 𝜑,𝑓 𝐶,ℎ ℎ,𝑁 𝑄,ℎ 𝑈,ℎ ℎ,𝑉 ℎ,𝑌 0 ,ℎ 𝜑,ℎ Allowed substitution hints: 𝜑(𝑔) 𝐴(𝑓,𝑔,ℎ) 𝐶(𝑔) 𝐷(𝑓,𝑔,ℎ) 𝑄(𝑔) 𝑅(𝑔) 𝑆(𝑓,𝑔,ℎ) 𝑇(𝑓,𝑔,ℎ) 𝑈(𝑓) 𝐹(ℎ) 𝐻(𝑓,𝑔,ℎ) 𝐾(𝑔,ℎ) 𝐿(𝑓) 𝑀(𝑓,𝑔,ℎ) 𝑁(𝑓,𝑔) 𝑂(𝑓) 𝑉(𝑓,𝑔) 𝑊(𝑔,ℎ) 𝑌(𝑓,𝑔) 0 (𝑓,𝑔)

**Proof of Theorem mapdrvallem3**
Step	Hyp	Ref	Expression
1		mapdrval.h	. . 3 ⊢ 𝐻 = (LHyp‘𝐾)
2		mapdrval.o	. . 3 ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)
3		mapdrval.m	. . 3 ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
4		mapdrval.u	. . 3 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
5		mapdrval.s	. . 3 ⊢ 𝑆 = (LSubSp‘𝑈)
6		mapdrval.f	. . 3 ⊢ 𝐹 = (LFnl‘𝑈)
7		mapdrval.l	. . 3 ⊢ 𝐿 = (LKer‘𝑈)
8		mapdrval.d	. . 3 ⊢ 𝐷 = (LDual‘𝑈)
9		mapdrval.t	. . 3 ⊢ 𝑇 = (LSubSp‘𝐷)
10		mapdrval.c	. . 3 ⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)}
11		mapdrval.k	. . 3 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
12		mapdrval.r	. . 3 ⊢ (𝜑 → 𝑅 ∈ 𝑇)
13		mapdrval.e	. . 3 ⊢ (𝜑 → 𝑅 ⊆ 𝐶)
14		mapdrval.q	. . 3 ⊢ 𝑄 = ∪ ℎ ∈ 𝑅 (𝑂‘(𝐿‘ℎ))
15		mapdrval.v	. . 3 ⊢ 𝑉 = (Base‘𝑈)
16		mapdrvallem2.a	. . 3 ⊢ 𝐴 = (LSAtoms‘𝑈)
17		mapdrvallem2.n	. . 3 ⊢ 𝑁 = (LSpan‘𝑈)
18		mapdrvallem2.z	. . 3 ⊢ 0 = (0_g‘𝑈)
19		mapdrvallem2.y	. . 3 ⊢ 𝑌 = (0_g‘𝐷)
20	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19	mapdrvallem2 37420	. 2 ⊢ (𝜑 → {𝑓 ∈ 𝐶 ∣ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑄} ⊆ 𝑅)
21		2fveq3 6407	. . . . . 6 ⊢ (ℎ = 𝑓 → (𝑂‘(𝐿‘ℎ)) = (𝑂‘(𝐿‘𝑓)))
22	21	ssiun2s 4749	. . . . 5 ⊢ (𝑓 ∈ 𝑅 → (𝑂‘(𝐿‘𝑓)) ⊆ ∪ ℎ ∈ 𝑅 (𝑂‘(𝐿‘ℎ)))
23	22	adantl 469	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑅) → (𝑂‘(𝐿‘𝑓)) ⊆ ∪ ℎ ∈ 𝑅 (𝑂‘(𝐿‘ℎ)))
24	23, 14	syl6sseqr 3843	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑅) → (𝑂‘(𝐿‘𝑓)) ⊆ 𝑄)
25	13, 24	ssrabdv 3872	. 2 ⊢ (𝜑 → 𝑅 ⊆ {𝑓 ∈ 𝐶 ∣ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑄})
26	20, 25	eqssd 3809	1 ⊢ (𝜑 → {𝑓 ∈ 𝐶 ∣ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑄} = 𝑅)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 = wceq 1637 ∈ wcel 2155 {crab 3096 ⊆ wss 3763 ∪ ciun 4705 ‘cfv 6095 Basecbs 16062 0_gc0g 16299 LSubSpclss 19130 LSpanclspn 19172 LSAtomsclsa 34748 LFnlclfn 34831 LKerclk 34859 LDualcld 34897 HLchlt 35124 LHypclh 35758 DVecHcdvh 36853 ocHcoch 37122 mapdcmpd 37399

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1877 ax-4 1894 ax-5 2001 ax-6 2067 ax-7 2103 ax-8 2157 ax-9 2164 ax-10 2184 ax-11 2200 ax-12 2213 ax-13 2419 ax-ext 2781 ax-rep 4957 ax-sep 4968 ax-nul 4977 ax-pow 5029 ax-pr 5090 ax-un 7173 ax-cnex 10271 ax-resscn 10272 ax-1cn 10273 ax-icn 10274 ax-addcl 10275 ax-addrcl 10276 ax-mulcl 10277 ax-mulrcl 10278 ax-mulcom 10279 ax-addass 10280 ax-mulass 10281 ax-distr 10282 ax-i2m1 10283 ax-1ne0 10284 ax-1rid 10285 ax-rnegex 10286 ax-rrecex 10287 ax-cnre 10288 ax-pre-lttri 10289 ax-pre-lttrn 10290 ax-pre-ltadd 10291 ax-pre-mulgt0 10292 ax-riotaBAD 34726

This theorem depends on definitions: df-bi 198 df-an 385 df-or 866 df-3or 1101 df-3an 1102 df-tru 1641 df-fal 1651 df-ex 1860 df-nf 1864 df-sb 2060 df-eu 2633 df-mo 2634 df-clab 2789 df-cleq 2795 df-clel 2798 df-nfc 2933 df-ne 2975 df-nel 3078 df-ral 3097 df-rex 3098 df-reu 3099 df-rmo 3100 df-rab 3101 df-v 3389 df-sbc 3628 df-csb 3723 df-dif 3766 df-un 3768 df-in 3770 df-ss 3777 df-pss 3779 df-nul 4111 df-if 4274 df-pw 4347 df-sn 4365 df-pr 4367 df-tp 4369 df-op 4371 df-uni 4624 df-int 4663 df-iun 4707 df-iin 4708 df-br 4838 df-opab 4900 df-mpt 4917 df-tr 4940 df-id 5213 df-eprel 5218 df-po 5226 df-so 5227 df-fr 5264 df-we 5266 df-xp 5311 df-rel 5312 df-cnv 5313 df-co 5314 df-dm 5315 df-rn 5316 df-res 5317 df-ima 5318 df-pred 5887 df-ord 5933 df-on 5934 df-lim 5935 df-suc 5936 df-iota 6058 df-fun 6097 df-fn 6098 df-f 6099 df-f1 6100 df-fo 6101 df-f1o 6102 df-fv 6103 df-riota 6829 df-ov 6871 df-oprab 6872 df-mpt2 6873 df-of 7121 df-om 7290 df-1st 7392 df-2nd 7393 df-tpos 7581 df-undef 7628 df-wrecs 7636 df-recs 7698 df-rdg 7736 df-1o 7790 df-oadd 7794 df-er 7973 df-map 8088 df-en 8187 df-dom 8188 df-sdom 8189 df-fin 8190 df-pnf 10355 df-mnf 10356 df-xr 10357 df-ltxr 10358 df-le 10359 df-sub 10547 df-neg 10548 df-nn 11300 df-2 11358 df-3 11359 df-4 11360 df-5 11361 df-6 11362 df-n0 11554 df-z 11638 df-uz 11899 df-fz 12544 df-struct 16064 df-ndx 16065 df-slot 16066 df-base 16068 df-sets 16069 df-ress 16070 df-plusg 16160 df-mulr 16161 df-sca 16163 df-vsca 16164 df-0g 16301 df-proset 17127 df-poset 17145 df-plt 17157 df-lub 17173 df-glb 17174 df-join 17175 df-meet 17176 df-p0 17238 df-p1 17239 df-lat 17245 df-clat 17307 df-mgm 17441 df-sgrp 17483 df-mnd 17494 df-submnd 17535 df-grp 17624 df-minusg 17625 df-sbg 17626 df-subg 17787 df-cntz 17945 df-lsm 18246 df-cmn 18390 df-abl 18391 df-mgp 18686 df-ur 18698 df-ring 18745 df-oppr 18819 df-dvdsr 18837 df-unit 18838 df-invr 18868 df-dvr 18879 df-drng 18947 df-lmod 19063 df-lss 19131 df-lsp 19173 df-lvec 19304 df-lsatoms 34750 df-lshyp 34751 df-lfl 34832 df-lkr 34860 df-ldual 34898 df-oposet 34950 df-ol 34952 df-oml 34953 df-covers 35040 df-ats 35041 df-atl 35072 df-cvlat 35096 df-hlat 35125 df-llines 35272 df-lplanes 35273 df-lvols 35274 df-lines 35275 df-psubsp 35277 df-pmap 35278 df-padd 35570 df-lhyp 35762 df-laut 35763 df-ldil 35878 df-ltrn 35879 df-trl 35934 df-tgrp 36518 df-tendo 36530 df-edring 36532 df-dveca 36778 df-disoa 36804 df-dvech 36854 df-dib 36914 df-dic 36948 df-dih 37004 df-doch 37123 df-djh 37170

This theorem is referenced by: mapdrval 37422

W3C validator