# 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}={\mathrm{Base}}_{{K}}$
dihf11.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dihf11.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
dihf11.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dihf11.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
Assertion dihf11 ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {I}:{B}\underset{1-1}{⟶}{S}$

### Proof

Step Hyp Ref Expression
1 dihf11.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 dihf11.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
3 dihf11.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
4 dihf11.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
5 dihf11.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
6 1 2 3 4 5 dihf11lem ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {I}:{B}⟶{S}$
7 1 2 3 dih11 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {x}\in {B}\wedge {y}\in {B}\right)\to \left({I}\left({x}\right)={I}\left({y}\right)↔{x}={y}\right)$
8 7 biimpd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {x}\in {B}\wedge {y}\in {B}\right)\to \left({I}\left({x}\right)={I}\left({y}\right)\to {x}={y}\right)$
9 8 3expb ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \left({I}\left({x}\right)={I}\left({y}\right)\to {x}={y}\right)$
10 9 ralrimivva ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({I}\left({x}\right)={I}\left({y}\right)\to {x}={y}\right)$
11 dff13 ${⊢}{I}:{B}\underset{1-1}{⟶}{S}↔\left({I}:{B}⟶{S}\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({I}\left({x}\right)={I}\left({y}\right)\to {x}={y}\right)\right)$
12 6 10 11 sylanbrc ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {I}:{B}\underset{1-1}{⟶}{S}$