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 = LHyp (K)$
	mapdat.m	$⊢ M = mapd (K) (W)$
	mapdat.u	$⊢ U = DVecH (K) (W)$
	mapdat.a	$⊢ A = LSAtoms (U)$
	mapdat.c	$⊢ C = LCDual (K) (W)$
	mapdat.b	$⊢ B = LSAtoms (C)$
	mapdat.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdcnvat.q	$⊢ φ \to Q \in B$
Assertion	mapdcnvatN	$⊢ φ \to M^{-1} (Q) \in A$

Proof

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

Metamath Proof Explorer

Theorem mapdcnvatN

Proof