Theorem mapdsord

Description: Strong ordering property of themap defined by df-mapd . (Contributed by NM, 13-Mar-2015)

	Ref	Expression
Hypotheses	mapdcnvcl.h	|- H = ( LHyp ` K )
	mapdcnvcl.m	|- M = ( ( mapd ` K ) ` W )
	mapdcnvcl.u	|- U = ( ( DVecH ` K ) ` W )
	mapdcnvcl.s	|- S = ( LSubSp ` U )
	mapdcnvcl.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	mapdcl.x	|- ( ph -> X e. S )
	mapdsord.x	|- ( ph -> Y e. S )
Assertion	mapdsord	|- ( ph -> ( ( M ` X ) C. ( M ` Y ) <-> X C. Y ) )

Proof

Step	Hyp	Ref	Expression
1		mapdcnvcl.h	|- H = ( LHyp ` K )
2		mapdcnvcl.m	|- M = ( ( mapd ` K ) ` W )
3		mapdcnvcl.u	|- U = ( ( DVecH ` K ) ` W )
4		mapdcnvcl.s	|- S = ( LSubSp ` U )
5		mapdcnvcl.k	|- ( ph -> ( K e. HL /\ W e. H ) )
6		mapdcl.x	|- ( ph -> X e. S )
7		mapdsord.x	|- ( ph -> Y e. S )
8	1 3 4 2 5 6 7	mapdord	|- ( ph -> ( ( M ` X ) C_ ( M ` Y ) <-> X C_ Y ) )
9	1 3 4 2 5 6 7	mapd11	|- ( ph -> ( ( M ` X ) = ( M ` Y ) <-> X = Y ) )
10	9	necon3bid	|- ( ph -> ( ( M ` X ) =/= ( M ` Y ) <-> X =/= Y ) )
11	8 10	anbi12d	|- ( ph -> ( ( ( M ` X ) C_ ( M ` Y ) /\ ( M ` X ) =/= ( M ` Y ) ) <-> ( X C_ Y /\ X =/= Y ) ) )
12		df-pss	|- ( ( M ` X ) C. ( M ` Y ) <-> ( ( M ` X ) C_ ( M ` Y ) /\ ( M ` X ) =/= ( M ` Y ) ) )
13		df-pss	|- ( X C. Y <-> ( X C_ Y /\ X =/= Y ) )
14	11 12 13	3bitr4g	|- ( ph -> ( ( M ` X ) C. ( M ` Y ) <-> X C. Y ) )