Theorem mapdcnvatN

Description: Atoms are preserved by the map defined by df-mapd . (Contributed by NM, 29-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mapdat.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	mapdat.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	mapdat.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	mapdat.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
	mapdat.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	mapdat.b	$$⊢B=\mathrm{LSAtoms}\left(C\right)$$
	mapdat.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	mapdcnvat.q	$$⊢\phi \to Q\in B$$
Assertion	mapdcnvatN	$$⊢\phi \to M^{-1}\left(Q\right)\in A$$

Proof

Step	Hyp	Ref	Expression
1		mapdat.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		mapdat.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
3		mapdat.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		mapdat.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
5		mapdat.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
6		mapdat.b	$$⊢B=\mathrm{LSAtoms}\left(C\right)$$
7		mapdat.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
8		mapdcnvat.q	$$⊢\phi \to Q\in B$$
9		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
10	1 3 7	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
11		eqid	$$⊢0_U=0_U$$
12	11 9	lsssn0	$$⊢U\in \mathrm{LMod}\to \left\{0_U\right\}\in \mathrm{LSubSp}\left(U\right)$$
13	10 12	syl	$$⊢\phi \to \left\{0_U\right\}\in \mathrm{LSubSp}\left(U\right)$$
14	1 2 3 9 7 13	mapdcnvid1N	$$⊢\phi \to M^{-1}\left(M\left(\left\{0_U\right\}\right)\right)=\left\{0_U\right\}$$
15		eqid	$$⊢0_C=0_C$$
16	1 2 3 11 5 15 7	mapd0	$$⊢\phi \to M\left(\left\{0_U\right\}\right)=\left\{0_C\right\}$$
17	16	fveq2d	$$⊢\phi \to M^{-1}\left(M\left(\left\{0_U\right\}\right)\right)=M^{-1}\left(\left\{0_C\right\}\right)$$
18	14 17	eqtr3d	$$⊢\phi \to \left\{0_U\right\}=M^{-1}\left(\left\{0_C\right\}\right)$$
19		eqid	$$⊢{⋖}_L\left(C\right)={⋖}_L\left(C\right)$$
20	1 5 7	lcdlvec	$$⊢\phi \to C\in \mathrm{LVec}$$
21	15 6 19 20 8	lsatcv0	$$⊢\phi \to \left\{0_C\right\}{⋖}_L\left(C\right)Q$$
22	1 5 7	lcdlmod	$$⊢\phi \to C\in \mathrm{LMod}$$
23		eqid	$$⊢\mathrm{LSubSp}\left(C\right)=\mathrm{LSubSp}\left(C\right)$$
24	15 23	lsssn0	$$⊢C\in \mathrm{LMod}\to \left\{0_C\right\}\in \mathrm{LSubSp}\left(C\right)$$
25	22 24	syl	$$⊢\phi \to \left\{0_C\right\}\in \mathrm{LSubSp}\left(C\right)$$
26	1 2 5 23 7	mapdrn2	$$⊢\phi \to \mathrm{ran}M=\mathrm{LSubSp}\left(C\right)$$
27	25 26	eleqtrrd	$$⊢\phi \to \left\{0_C\right\}\in \mathrm{ran}M$$
28	1 2 7 27	mapdcnvid2	$$⊢\phi \to M\left(M^{-1}\left(\left\{0_C\right\}\right)\right)=\left\{0_C\right\}$$
29	23 6 22 8	lsatlssel	$$⊢\phi \to Q\in \mathrm{LSubSp}\left(C\right)$$
30	29 26	eleqtrrd	$$⊢\phi \to Q\in \mathrm{ran}M$$
31	1 2 7 30	mapdcnvid2	$$⊢\phi \to M\left(M^{-1}\left(Q\right)\right)=Q$$
32	21 28 31	3brtr4d	$$⊢\phi \to M\left(M^{-1}\left(\left\{0_C\right\}\right)\right){⋖}_L\left(C\right)M\left(M^{-1}\left(Q\right)\right)$$
33		eqid	$$⊢{⋖}_L\left(U\right)={⋖}_L\left(U\right)$$
34	1 2 3 9 7 27	mapdcnvcl	$$⊢\phi \to M^{-1}\left(\left\{0_C\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
35	1 2 3 9 7 30	mapdcnvcl	$$⊢\phi \to M^{-1}\left(Q\right)\in \mathrm{LSubSp}\left(U\right)$$
36	1 2 3 9 33 5 19 7 34 35	mapdcv	$$⊢\phi \to \left(M^{-1}\left(\left\{0_C\right\}\right){⋖}_L\left(U\right)M^{-1}\left(Q\right)\leftrightarrow M\left(M^{-1}\left(\left\{0_C\right\}\right)\right){⋖}_L\left(C\right)M\left(M^{-1}\left(Q\right)\right)\right)$$
37	32 36	mpbird	$$⊢\phi \to M^{-1}\left(\left\{0_C\right\}\right){⋖}_L\left(U\right)M^{-1}\left(Q\right)$$
38	18 37	eqbrtrd	$$⊢\phi \to \left\{0_U\right\}{⋖}_L\left(U\right)M^{-1}\left(Q\right)$$
39	1 3 7	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
40	11 9 4 33 39 35	lsat0cv	$$⊢\phi \to \left(M^{-1}\left(Q\right)\in A\leftrightarrow \left\{0_U\right\}{⋖}_L\left(U\right)M^{-1}\left(Q\right)\right)$$
41	38 40	mpbird	$$⊢\phi \to M^{-1}\left(Q\right)\in A$$