Theorem mapdunirnN 42157

Description: Union of the range of the map defined by df-mapd 42132. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)

Hypotheses

Ref	Expression
mapdrn.h	⊢ 𝐻 = (LHyp‘𝐾)
mapdrn.o	⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)
mapdrn.m	⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
mapdrn.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
mapdrn.f	⊢ 𝐹 = (LFnl‘𝑈)
mapdrn.l	⊢ 𝐿 = (LKer‘𝑈)
mapdunirn.c	⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)}
mapdunirn.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))

Assertion

Ref	Expression
mapdunirnN	⊢ (𝜑 → ∪ ran 𝑀 = 𝐶)

Distinct variable groups:   𝑔,𝐹   𝑔,𝐾   𝑔,𝐿   𝑔,𝑂   𝑈,𝑔   𝑔,𝑊

Allowed substitution hints:   𝜑(𝑔)   𝐶(𝑔)   𝐻(𝑔)   𝑀(𝑔)

Proof of Theorem mapdunirnN

Step	Hyp	Ref	Expression
1		mapdrn.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
2		mapdrn.o	. . . 4 ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)
3		mapdrn.m	. . . 4 ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
4		mapdrn.u	. . . 4 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
5		mapdrn.f	. . . 4 ⊢ 𝐹 = (LFnl‘𝑈)
6		mapdrn.l	. . . 4 ⊢ 𝐿 = (LKer‘𝑈)
7		eqid 2741	. . . 4 ⊢ (LDual‘𝑈) = (LDual‘𝑈)
8		eqid 2741	. . . 4 ⊢ (LSubSp‘(LDual‘𝑈)) = (LSubSp‘(LDual‘𝑈))
9		mapdunirn.c	. . . 4 ⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)}
10		mapdunirn.k	. . . 4 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
11	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	mapdrn 42156	. . 3 ⊢ (𝜑 → ran 𝑀 = ((LSubSp‘(LDual‘𝑈)) ∩ 𝒫 𝐶))
12	11	unieqd 4854	. 2 ⊢ (𝜑 → ∪ ran 𝑀 = ∪ ((LSubSp‘(LDual‘𝑈)) ∩ 𝒫 𝐶))
13		uniin 4865	. . . 4 ⊢ ∪ ((LSubSp‘(LDual‘𝑈)) ∩ 𝒫 𝐶) ⊆ (∪ (LSubSp‘(LDual‘𝑈)) ∩ ∪ 𝒫 𝐶)
14		eqid 2741	. . . . . . . 8 ⊢ (Base‘(LDual‘𝑈)) = (Base‘(LDual‘𝑈))
15	1, 4, 10	dvhlmod 41617	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ LMod)
16	7, 15	lduallmod 39660	. . . . . . . 8 ⊢ (𝜑 → (LDual‘𝑈) ∈ LMod)
17	14, 8, 16	lssuni 20933	. . . . . . 7 ⊢ (𝜑 → ∪ (LSubSp‘(LDual‘𝑈)) = (Base‘(LDual‘𝑈)))
18	5, 7, 14, 15	ldualvbase 39633	. . . . . . 7 ⊢ (𝜑 → (Base‘(LDual‘𝑈)) = 𝐹)
19	17, 18	eqtrd 2776	. . . . . 6 ⊢ (𝜑 → ∪ (LSubSp‘(LDual‘𝑈)) = 𝐹)
20		unipw 5392	. . . . . . 7 ⊢ ∪ 𝒫 𝐶 = 𝐶
21	20	a1i 11	. . . . . 6 ⊢ (𝜑 → ∪ 𝒫 𝐶 = 𝐶)
22	19, 21	ineq12d 4153	. . . . 5 ⊢ (𝜑 → (∪ (LSubSp‘(LDual‘𝑈)) ∩ ∪ 𝒫 𝐶) = (𝐹 ∩ 𝐶))
23		ssrab2 4014	. . . . . . . 8 ⊢ {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)} ⊆ 𝐹
24	9, 23	eqsstri 3963	. . . . . . 7 ⊢ 𝐶 ⊆ 𝐹
25		sseqin2 4155	. . . . . . 7 ⊢ (𝐶 ⊆ 𝐹 ↔ (𝐹 ∩ 𝐶) = 𝐶)
26	24, 25	mpbi 232	. . . . . 6 ⊢ (𝐹 ∩ 𝐶) = 𝐶
27	26	a1i 11	. . . . 5 ⊢ (𝜑 → (𝐹 ∩ 𝐶) = 𝐶)
28	22, 27	eqtrd 2776	. . . 4 ⊢ (𝜑 → (∪ (LSubSp‘(LDual‘𝑈)) ∩ ∪ 𝒫 𝐶) = 𝐶)
29	13, 28	sseqtrid 3959	. . 3 ⊢ (𝜑 → ∪ ((LSubSp‘(LDual‘𝑈)) ∩ 𝒫 𝐶) ⊆ 𝐶)
30	1, 4, 2, 5, 6, 7, 8, 9, 10	lclkr 42040	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ (LSubSp‘(LDual‘𝑈)))
31	5	fvexi 6845	. . . . . . . 8 ⊢ 𝐹 ∈ V
32	9, 31	rabex2 5272	. . . . . . 7 ⊢ 𝐶 ∈ V
33	32	pwid 4554	. . . . . 6 ⊢ 𝐶 ∈ 𝒫 𝐶
34	33	a1i 11	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ 𝒫 𝐶)
35	30, 34	elind 4132	. . . 4 ⊢ (𝜑 → 𝐶 ∈ ((LSubSp‘(LDual‘𝑈)) ∩ 𝒫 𝐶))
36		elssuni 4872	. . . 4 ⊢ (𝐶 ∈ ((LSubSp‘(LDual‘𝑈)) ∩ 𝒫 𝐶) → 𝐶 ⊆ ∪ ((LSubSp‘(LDual‘𝑈)) ∩ 𝒫 𝐶))
37	35, 36	syl 17	. . 3 ⊢ (𝜑 → 𝐶 ⊆ ∪ ((LSubSp‘(LDual‘𝑈)) ∩ 𝒫 𝐶))
38	29, 37	eqssd 3934	. 2 ⊢ (𝜑 → ∪ ((LSubSp‘(LDual‘𝑈)) ∩ 𝒫 𝐶) = 𝐶)
39	12, 38	eqtrd 2776	1 ⊢ (𝜑 → ∪ ran 𝑀 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1548   ∈ wcel 2121  {crab 3393   ∩ cin 3884   ⊆ wss 3885  𝒫 cpw 4532  ∪ cuni 4841  ran crn 5622  ‘cfv 6489  Basecbs 17174  LModclmod 20854  LSubSpclss 20925  LFnlclfn 39564  LKerclk 39592  LDualcld 39630  HLchlt 39857  LHypclh 40491  DVecHcdvh 41585  ocHcoch 41854  mapdcmpd 42131

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-rep 5202  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682  ax-cnex 11089  ax-resscn 11090  ax-1cn 11091  ax-icn 11092  ax-addcl 11093  ax-addrcl 11094  ax-mulcl 11095  ax-mulrcl 11096  ax-mulcom 11097  ax-addass 11098  ax-mulass 11099  ax-distr 11100  ax-i2m1 11101  ax-1ne0 11102  ax-1rid 11103  ax-rnegex 11104  ax-rrecex 11105  ax-cnre 11106  ax-pre-lttri 11107  ax-pre-lttrn 11108  ax-pre-ltadd 11109  ax-pre-mulgt0 11110  ax-riotaBAD 39460

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-rmo 3346  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4842  df-int 4881  df-iun 4926  df-iin 4927  df-br 5076  df-opab 5138  df-mpt 5157  df-tr 5183  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-of 7624  df-om 7811  df-1st 7935  df-2nd 7936  df-tpos 8170  df-undef 8217  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-2o 8400  df-er 8637  df-map 8769  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-pnf 11176  df-mnf 11177  df-xr 11178  df-ltxr 11179  df-le 11180  df-sub 11374  df-neg 11375  df-nn 12170  df-2 12239  df-3 12240  df-4 12241  df-5 12242  df-6 12243  df-n0 12433  df-z 12520  df-uz 12784  df-fz 13457  df-struct 17112  df-sets 17129  df-slot 17147  df-ndx 17159  df-base 17175  df-ress 17196  df-plusg 17228  df-mulr 17229  df-sca 17231  df-vsca 17232  df-0g 17399  df-mre 17543  df-mrc 17544  df-acs 17546  df-proset 18255  df-poset 18274  df-plt 18289  df-lub 18305  df-glb 18306  df-join 18307  df-meet 18308  df-p0 18384  df-p1 18385  df-lat 18393  df-clat 18460  df-mgm 18603  df-sgrp 18682  df-mnd 18698  df-submnd 18747  df-grp 18907  df-minusg 18908  df-sbg 18909  df-subg 19094  df-cntz 19287  df-oppg 19316  df-lsm 19606  df-cmn 19752  df-abl 19753  df-mgp 20117  df-rng 20129  df-ur 20158  df-ring 20211  df-oppr 20312  df-dvdsr 20332  df-unit 20333  df-invr 20363  df-dvr 20376  df-nzr 20489  df-rlreg 20670  df-domn 20671  df-drng 20707  df-lmod 20856  df-lss 20926  df-lsp 20966  df-lvec 21097  df-lsatoms 39483  df-lshyp 39484  df-lcv 39526  df-lfl 39565  df-lkr 39593  df-ldual 39631  df-oposet 39683  df-ol 39685  df-oml 39686  df-covers 39773  df-ats 39774  df-atl 39805  df-cvlat 39829  df-hlat 39858  df-llines 40005  df-lplanes 40006  df-lvols 40007  df-lines 40008  df-psubsp 40010  df-pmap 40011  df-padd 40303  df-lhyp 40495  df-laut 40496  df-ldil 40611  df-ltrn 40612  df-trl 40666  df-tgrp 41250  df-tendo 41262  df-edring 41264  df-dveca 41510  df-disoa 41536  df-dvech 41586  df-dib 41646  df-dic 41680  df-dih 41736  df-doch 41855  df-djh 41902  df-mapd 42132

This theorem is referenced by: (None)