Theorem dihf11

Description: The isomorphism H for a lattice K is a one-to-one function. Part of proof after Lemma N of Crawley p. 122 line 6. (Contributed by NM, 7-Mar-2014)

	Ref	Expression
Hypotheses	dihf11.b	|- B = ( Base ` K )
	dihf11.h	|- H = ( LHyp ` K )
	dihf11.i	|- I = ( ( DIsoH ` K ) ` W )
	dihf11.u	|- U = ( ( DVecH ` K ) ` W )
	dihf11.s	|- S = ( LSubSp ` U )
Assertion	dihf11	|- ( ( K e. HL /\ W e. H ) -> I : B -1-1-> S )

Proof

Step	Hyp	Ref	Expression
1		dihf11.b	|- B = ( Base ` K )
2		dihf11.h	|- H = ( LHyp ` K )
3		dihf11.i	|- I = ( ( DIsoH ` K ) ` W )
4		dihf11.u	|- U = ( ( DVecH ` K ) ` W )
5		dihf11.s	|- S = ( LSubSp ` U )
6	1 2 3 4 5	dihf11lem	|- ( ( K e. HL /\ W e. H ) -> I : B --> S )
7	1 2 3	dih11	|- ( ( ( K e. HL /\ W e. H ) /\ x e. B /\ y e. B ) -> ( ( I ` x ) = ( I ` y ) <-> x = y ) )
8	7	biimpd	|- ( ( ( K e. HL /\ W e. H ) /\ x e. B /\ y e. B ) -> ( ( I ` x ) = ( I ` y ) -> x = y ) )
9	8	3expb	|- ( ( ( K e. HL /\ W e. H ) /\ ( x e. B /\ y e. B ) ) -> ( ( I ` x ) = ( I ` y ) -> x = y ) )
10	9	ralrimivva	|- ( ( K e. HL /\ W e. H ) -> A. x e. B A. y e. B ( ( I ` x ) = ( I ` y ) -> x = y ) )
11		dff13	|- ( I : B -1-1-> S <-> ( I : B --> S /\ A. x e. B A. y e. B ( ( I ` x ) = ( I ` y ) -> x = y ) ) )
12	6 10 11	sylanbrc	|- ( ( K e. HL /\ W e. H ) -> I : B -1-1-> S )