This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )