Theorem pmap11

Description: The projective map of a Hilbert lattice is one-to-one. Part of Theorem 15.5 of MaedaMaeda p. 62. (Contributed by NM, 22-Oct-2011)

	Ref	Expression
Hypotheses	pmap11.b	|- B = ( Base ` K )
	pmap11.m	|- M = ( pmap ` K )
Assertion	pmap11	|- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( M ` X ) = ( M ` Y ) <-> X = Y ) )

Proof

Step	Hyp	Ref	Expression
1		pmap11.b	|- B = ( Base ` K )
2		pmap11.m	|- M = ( pmap ` K )
3		eqss	|- ( ( M ` X ) = ( M ` Y ) <-> ( ( M ` X ) C_ ( M ` Y ) /\ ( M ` Y ) C_ ( M ` X ) ) )
4		hllat	|- ( K e. HL -> K e. Lat )
5		eqid	|- ( le ` K ) = ( le ` K )
6	1 5	latasymb	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( X ( le ` K ) Y /\ Y ( le ` K ) X ) <-> X = Y ) )
7	4 6	syl3an1	|- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( X ( le ` K ) Y /\ Y ( le ` K ) X ) <-> X = Y ) )
8	1 5 2	pmaple	|- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X ( le ` K ) Y <-> ( M ` X ) C_ ( M ` Y ) ) )
9	1 5 2	pmaple	|- ( ( K e. HL /\ Y e. B /\ X e. B ) -> ( Y ( le ` K ) X <-> ( M ` Y ) C_ ( M ` X ) ) )
10	9	3com23	|- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( Y ( le ` K ) X <-> ( M ` Y ) C_ ( M ` X ) ) )
11	8 10	anbi12d	|- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( X ( le ` K ) Y /\ Y ( le ` K ) X ) <-> ( ( M ` X ) C_ ( M ` Y ) /\ ( M ` Y ) C_ ( M ` X ) ) ) )
12	7 11	bitr3d	|- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X = Y <-> ( ( M ` X ) C_ ( M ` Y ) /\ ( M ` Y ) C_ ( M ` X ) ) ) )
13	3 12	bitr4id	|- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( M ` X ) = ( M ` Y ) <-> X = Y ) )