Theorem mapdunirnN

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

	Ref	Expression
Hypotheses	mapdrn.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	mapdrn.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
	mapdrn.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	mapdrn.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	mapdrn.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	mapdrn.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	mapdunirn.c	$$⊢C=\left\{g\in F|O\left(O\left(L\left(g\right)\right)\right)=L\left(g\right)\right\}$$
	mapdunirn.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
Assertion	mapdunirnN	$$⊢\phi \to \bigcup \mathrm{ran}M=C$$

Proof

Step	Hyp	Ref	Expression
1		mapdrn.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		mapdrn.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		mapdrn.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
4		mapdrn.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		mapdrn.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
6		mapdrn.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
7		mapdunirn.c	$$⊢C=\left\{g\in F|O\left(O\left(L\left(g\right)\right)\right)=L\left(g\right)\right\}$$
8		mapdunirn.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		eqid	$$⊢\mathrm{LDual}\left(U\right)=\mathrm{LDual}\left(U\right)$$
10		eqid	$$⊢\mathrm{LSubSp}\left(\mathrm{LDual}\left(U\right)\right)=\mathrm{LSubSp}\left(\mathrm{LDual}\left(U\right)\right)$$
11	1 2 3 4 5 6 9 10 7 8	mapdrn	$$⊢\phi \to \mathrm{ran}M=\mathrm{LSubSp}\left(\mathrm{LDual}\left(U\right)\right)\cap 𝒫C$$
12	11	unieqd	$$⊢\phi \to \bigcup \mathrm{ran}M=\bigcup \left(\mathrm{LSubSp}\left(\mathrm{LDual}\left(U\right)\right)\cap 𝒫C\right)$$
13		uniin	$$⊢\bigcup \left(\mathrm{LSubSp}\left(\mathrm{LDual}\left(U\right)\right)\cap 𝒫C\right)\subseteq \bigcup \mathrm{LSubSp}\left(\mathrm{LDual}\left(U\right)\right)\cap \bigcup 𝒫C$$
14		eqid	$$⊢{\mathrm{Base}}_{\mathrm{LDual}\left(U\right)}={\mathrm{Base}}_{\mathrm{LDual}\left(U\right)}$$
15	1 4 8	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
16	9 15	lduallmod	$$⊢\phi \to \mathrm{LDual}\left(U\right)\in \mathrm{LMod}$$
17	14 10 16	lssuni	$$⊢\phi \to \bigcup \mathrm{LSubSp}\left(\mathrm{LDual}\left(U\right)\right)={\mathrm{Base}}_{\mathrm{LDual}\left(U\right)}$$
18	5 9 14 15	ldualvbase	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{LDual}\left(U\right)}=F$$
19	17 18	eqtrd	$$⊢\phi \to \bigcup \mathrm{LSubSp}\left(\mathrm{LDual}\left(U\right)\right)=F$$
20		unipw	$$⊢\bigcup 𝒫C=C$$
21	20	a1i	$$⊢\phi \to \bigcup 𝒫C=C$$
22	19 21	ineq12d	$$⊢\phi \to \bigcup \mathrm{LSubSp}\left(\mathrm{LDual}\left(U\right)\right)\cap \bigcup 𝒫C=F\cap C$$
23		ssrab2	$$⊢\left\{g\in F|O\left(O\left(L\left(g\right)\right)\right)=L\left(g\right)\right\}\subseteq F$$
24	7 23	eqsstri	$$⊢C\subseteq F$$
25		sseqin2	$$⊢C\subseteq F\leftrightarrow F\cap C=C$$
26	24 25	mpbi	$$⊢F\cap C=C$$
27	26	a1i	$$⊢\phi \to F\cap C=C$$
28	22 27	eqtrd	$$⊢\phi \to \bigcup \mathrm{LSubSp}\left(\mathrm{LDual}\left(U\right)\right)\cap \bigcup 𝒫C=C$$
29	13 28	sseqtrid	$$⊢\phi \to \bigcup \left(\mathrm{LSubSp}\left(\mathrm{LDual}\left(U\right)\right)\cap 𝒫C\right)\subseteq C$$
30	1 4 2 5 6 9 10 7 8	lclkr	$$⊢\phi \to C\in \mathrm{LSubSp}\left(\mathrm{LDual}\left(U\right)\right)$$
31	5	fvexi	$$⊢F\in \mathrm{V}$$
32	7 31	rabex2	$$⊢C\in \mathrm{V}$$
33	32	pwid	$$⊢C\in 𝒫C$$
34	33	a1i	$$⊢\phi \to C\in 𝒫C$$
35	30 34	elind	$$⊢\phi \to C\in \left(\mathrm{LSubSp}\left(\mathrm{LDual}\left(U\right)\right)\cap 𝒫C\right)$$
36		elssuni	$$⊢C\in \left(\mathrm{LSubSp}\left(\mathrm{LDual}\left(U\right)\right)\cap 𝒫C\right)\to C\subseteq \bigcup \left(\mathrm{LSubSp}\left(\mathrm{LDual}\left(U\right)\right)\cap 𝒫C\right)$$
37	35 36	syl	$$⊢\phi \to C\subseteq \bigcup \left(\mathrm{LSubSp}\left(\mathrm{LDual}\left(U\right)\right)\cap 𝒫C\right)$$
38	29 37	eqssd	$$⊢\phi \to \bigcup \left(\mathrm{LSubSp}\left(\mathrm{LDual}\left(U\right)\right)\cap 𝒫C\right)=C$$
39	12 38	eqtrd	$$⊢\phi \to \bigcup \mathrm{ran}M=C$$