# Metamath Proof Explorer

## Theorem mapdcv

Description: Covering property of the converse of the map defined by df-mapd . (Contributed by NM, 14-Mar-2015)

Ref Expression
Hypotheses mapdcv.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
mapdcv.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
mapdcv.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
mapdcv.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
mapdcv.c ${⊢}{C}={⋖}_{L}\left({U}\right)$
mapdcv.d ${⊢}{D}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
mapdcv.e ${⊢}{E}={⋖}_{L}\left({D}\right)$
mapdcv.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
mapdcv.x ${⊢}{\phi }\to {X}\in {S}$
mapdcv.y ${⊢}{\phi }\to {Y}\in {S}$
Assertion mapdcv ${⊢}{\phi }\to \left({X}{C}{Y}↔{M}\left({X}\right){E}{M}\left({Y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 mapdcv.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 mapdcv.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
3 mapdcv.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
4 mapdcv.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
5 mapdcv.c ${⊢}{C}={⋖}_{L}\left({U}\right)$
6 mapdcv.d ${⊢}{D}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
7 mapdcv.e ${⊢}{E}={⋖}_{L}\left({D}\right)$
8 mapdcv.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
9 mapdcv.x ${⊢}{\phi }\to {X}\in {S}$
10 mapdcv.y ${⊢}{\phi }\to {Y}\in {S}$
11 1 2 3 4 8 9 10 mapdsord ${⊢}{\phi }\to \left({M}\left({X}\right)\subset {M}\left({Y}\right)↔{X}\subset {Y}\right)$
12 eqid ${⊢}\mathrm{LSubSp}\left({D}\right)=\mathrm{LSubSp}\left({D}\right)$
13 8 adantr ${⊢}\left({\phi }\wedge {v}\in {S}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
14 simpr ${⊢}\left({\phi }\wedge {v}\in {S}\right)\to {v}\in {S}$
15 1 2 3 4 6 12 13 14 mapdcl2 ${⊢}\left({\phi }\wedge {v}\in {S}\right)\to {M}\left({v}\right)\in \mathrm{LSubSp}\left({D}\right)$
16 8 adantr ${⊢}\left({\phi }\wedge {f}\in \mathrm{LSubSp}\left({D}\right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
17 1 2 6 12 8 mapdrn2 ${⊢}{\phi }\to \mathrm{ran}{M}=\mathrm{LSubSp}\left({D}\right)$
18 17 eleq2d ${⊢}{\phi }\to \left({f}\in \mathrm{ran}{M}↔{f}\in \mathrm{LSubSp}\left({D}\right)\right)$
19 18 biimpar ${⊢}\left({\phi }\wedge {f}\in \mathrm{LSubSp}\left({D}\right)\right)\to {f}\in \mathrm{ran}{M}$
20 1 2 3 4 16 19 mapdcnvcl ${⊢}\left({\phi }\wedge {f}\in \mathrm{LSubSp}\left({D}\right)\right)\to {{M}}^{-1}\left({f}\right)\in {S}$
21 1 2 16 19 mapdcnvid2 ${⊢}\left({\phi }\wedge {f}\in \mathrm{LSubSp}\left({D}\right)\right)\to {M}\left({{M}}^{-1}\left({f}\right)\right)={f}$
22 21 eqcomd ${⊢}\left({\phi }\wedge {f}\in \mathrm{LSubSp}\left({D}\right)\right)\to {f}={M}\left({{M}}^{-1}\left({f}\right)\right)$
23 fveq2 ${⊢}{v}={{M}}^{-1}\left({f}\right)\to {M}\left({v}\right)={M}\left({{M}}^{-1}\left({f}\right)\right)$
24 23 rspceeqv ${⊢}\left({{M}}^{-1}\left({f}\right)\in {S}\wedge {f}={M}\left({{M}}^{-1}\left({f}\right)\right)\right)\to \exists {v}\in {S}\phantom{\rule{.4em}{0ex}}{f}={M}\left({v}\right)$
25 20 22 24 syl2anc ${⊢}\left({\phi }\wedge {f}\in \mathrm{LSubSp}\left({D}\right)\right)\to \exists {v}\in {S}\phantom{\rule{.4em}{0ex}}{f}={M}\left({v}\right)$
26 psseq2 ${⊢}{f}={M}\left({v}\right)\to \left({M}\left({X}\right)\subset {f}↔{M}\left({X}\right)\subset {M}\left({v}\right)\right)$
27 psseq1 ${⊢}{f}={M}\left({v}\right)\to \left({f}\subset {M}\left({Y}\right)↔{M}\left({v}\right)\subset {M}\left({Y}\right)\right)$
28 26 27 anbi12d ${⊢}{f}={M}\left({v}\right)\to \left(\left({M}\left({X}\right)\subset {f}\wedge {f}\subset {M}\left({Y}\right)\right)↔\left({M}\left({X}\right)\subset {M}\left({v}\right)\wedge {M}\left({v}\right)\subset {M}\left({Y}\right)\right)\right)$
29 28 adantl ${⊢}\left({\phi }\wedge {f}={M}\left({v}\right)\right)\to \left(\left({M}\left({X}\right)\subset {f}\wedge {f}\subset {M}\left({Y}\right)\right)↔\left({M}\left({X}\right)\subset {M}\left({v}\right)\wedge {M}\left({v}\right)\subset {M}\left({Y}\right)\right)\right)$
30 15 25 29 rexxfrd ${⊢}{\phi }\to \left(\exists {f}\in \mathrm{LSubSp}\left({D}\right)\phantom{\rule{.4em}{0ex}}\left({M}\left({X}\right)\subset {f}\wedge {f}\subset {M}\left({Y}\right)\right)↔\exists {v}\in {S}\phantom{\rule{.4em}{0ex}}\left({M}\left({X}\right)\subset {M}\left({v}\right)\wedge {M}\left({v}\right)\subset {M}\left({Y}\right)\right)\right)$
31 9 adantr ${⊢}\left({\phi }\wedge {v}\in {S}\right)\to {X}\in {S}$
32 1 2 3 4 13 31 14 mapdsord ${⊢}\left({\phi }\wedge {v}\in {S}\right)\to \left({M}\left({X}\right)\subset {M}\left({v}\right)↔{X}\subset {v}\right)$
33 10 adantr ${⊢}\left({\phi }\wedge {v}\in {S}\right)\to {Y}\in {S}$
34 1 2 3 4 13 14 33 mapdsord ${⊢}\left({\phi }\wedge {v}\in {S}\right)\to \left({M}\left({v}\right)\subset {M}\left({Y}\right)↔{v}\subset {Y}\right)$
35 32 34 anbi12d ${⊢}\left({\phi }\wedge {v}\in {S}\right)\to \left(\left({M}\left({X}\right)\subset {M}\left({v}\right)\wedge {M}\left({v}\right)\subset {M}\left({Y}\right)\right)↔\left({X}\subset {v}\wedge {v}\subset {Y}\right)\right)$
36 35 rexbidva ${⊢}{\phi }\to \left(\exists {v}\in {S}\phantom{\rule{.4em}{0ex}}\left({M}\left({X}\right)\subset {M}\left({v}\right)\wedge {M}\left({v}\right)\subset {M}\left({Y}\right)\right)↔\exists {v}\in {S}\phantom{\rule{.4em}{0ex}}\left({X}\subset {v}\wedge {v}\subset {Y}\right)\right)$
37 30 36 bitrd ${⊢}{\phi }\to \left(\exists {f}\in \mathrm{LSubSp}\left({D}\right)\phantom{\rule{.4em}{0ex}}\left({M}\left({X}\right)\subset {f}\wedge {f}\subset {M}\left({Y}\right)\right)↔\exists {v}\in {S}\phantom{\rule{.4em}{0ex}}\left({X}\subset {v}\wedge {v}\subset {Y}\right)\right)$
38 37 notbid ${⊢}{\phi }\to \left(¬\exists {f}\in \mathrm{LSubSp}\left({D}\right)\phantom{\rule{.4em}{0ex}}\left({M}\left({X}\right)\subset {f}\wedge {f}\subset {M}\left({Y}\right)\right)↔¬\exists {v}\in {S}\phantom{\rule{.4em}{0ex}}\left({X}\subset {v}\wedge {v}\subset {Y}\right)\right)$
39 11 38 anbi12d ${⊢}{\phi }\to \left(\left({M}\left({X}\right)\subset {M}\left({Y}\right)\wedge ¬\exists {f}\in \mathrm{LSubSp}\left({D}\right)\phantom{\rule{.4em}{0ex}}\left({M}\left({X}\right)\subset {f}\wedge {f}\subset {M}\left({Y}\right)\right)\right)↔\left({X}\subset {Y}\wedge ¬\exists {v}\in {S}\phantom{\rule{.4em}{0ex}}\left({X}\subset {v}\wedge {v}\subset {Y}\right)\right)\right)$
40 1 6 8 lcdlmod ${⊢}{\phi }\to {D}\in \mathrm{LMod}$
41 1 2 3 4 6 12 8 9 mapdcl2 ${⊢}{\phi }\to {M}\left({X}\right)\in \mathrm{LSubSp}\left({D}\right)$
42 1 2 3 4 6 12 8 10 mapdcl2 ${⊢}{\phi }\to {M}\left({Y}\right)\in \mathrm{LSubSp}\left({D}\right)$
43 12 7 40 41 42 lcvbr ${⊢}{\phi }\to \left({M}\left({X}\right){E}{M}\left({Y}\right)↔\left({M}\left({X}\right)\subset {M}\left({Y}\right)\wedge ¬\exists {f}\in \mathrm{LSubSp}\left({D}\right)\phantom{\rule{.4em}{0ex}}\left({M}\left({X}\right)\subset {f}\wedge {f}\subset {M}\left({Y}\right)\right)\right)\right)$
44 1 3 8 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
45 4 5 44 9 10 lcvbr ${⊢}{\phi }\to \left({X}{C}{Y}↔\left({X}\subset {Y}\wedge ¬\exists {v}\in {S}\phantom{\rule{.4em}{0ex}}\left({X}\subset {v}\wedge {v}\subset {Y}\right)\right)\right)$
46 39 43 45 3bitr4rd ${⊢}{\phi }\to \left({X}{C}{Y}↔{M}\left({X}\right){E}{M}\left({Y}\right)\right)$