Theorem mapd11

Description: The map defined by df-mapd is one-to-one. Property (c) of Baer p. 40. (Contributed by NM, 12-Mar-2015)

	Ref	Expression
Hypotheses	mapdord.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	mapdord.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	mapdord.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
	mapdord.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	mapdord.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	mapdord.x	$$⊢\phi \to X\in S$$
	mapdord.y	$$⊢\phi \to Y\in S$$
Assertion	mapd11	$$⊢\phi \to \left(M\left(X\right)=M\left(Y\right)\leftrightarrow X=Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		mapdord.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		mapdord.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		mapdord.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
4		mapdord.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
5		mapdord.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
6		mapdord.x	$$⊢\phi \to X\in S$$
7		mapdord.y	$$⊢\phi \to Y\in S$$
8	1 2 3 4 5 6 7	mapdord	$$⊢\phi \to \left(M\left(X\right)\subseteq M\left(Y\right)\leftrightarrow X\subseteq Y\right)$$
9	1 2 3 4 5 7 6	mapdord	$$⊢\phi \to \left(M\left(Y\right)\subseteq M\left(X\right)\leftrightarrow Y\subseteq X\right)$$
10	8 9	anbi12d	$$⊢\phi \to \left(\left(M\left(X\right)\subseteq M\left(Y\right)\wedge M\left(Y\right)\subseteq M\left(X\right)\right)\leftrightarrow \left(X\subseteq Y\wedge Y\subseteq X\right)\right)$$
11		eqss	$$⊢M\left(X\right)=M\left(Y\right)\leftrightarrow \left(M\left(X\right)\subseteq M\left(Y\right)\wedge M\left(Y\right)\subseteq M\left(X\right)\right)$$
12		eqss	$$⊢X=Y\leftrightarrow \left(X\subseteq Y\wedge Y\subseteq X\right)$$
13	10 11 12	3bitr4g	$$⊢\phi \to \left(M\left(X\right)=M\left(Y\right)\leftrightarrow X=Y\right)$$