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 HL W 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 HL W H I : B S
7 1 2 3 dih11 K HL W H x B y B I x = I y x = y
8 7 biimpd K HL W H x B y B I x = I y x = y
9 8 3expb K HL W H x B y B I x = I y x = y
10 9 ralrimivva K HL W H x B y B I x = I y x = y
11 dff13 I : B 1-1 S I : B S x B y B I x = I y x = y
12 6 10 11 sylanbrc K HL W H I : B 1-1 S