Metamath Proof Explorer

Theorem diaf1oN

Description: The partial isomorphism A for a lattice K is a one-to-one, onto function. Part of Lemma M of Crawley p. 121 line 12, with closed subspaces rather than subspaces. See diadm for the domain. (Contributed by NM, 17-Jan-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dvadia.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dvadia.u ${⊢}{U}=\mathrm{DVecA}\left({K}\right)\left({W}\right)$
dvadia.i ${⊢}{I}=\mathrm{DIsoA}\left({K}\right)\left({W}\right)$
dvadia.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
Assertion diaf1oN

Proof

Step Hyp Ref Expression
1 dvadia.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dvadia.u ${⊢}{U}=\mathrm{DVecA}\left({K}\right)\left({W}\right)$
3 dvadia.i ${⊢}{I}=\mathrm{DIsoA}\left({K}\right)\left({W}\right)$
5 dvadia.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
6 1 3 diaf11N ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {I}:\mathrm{dom}{I}\underset{1-1 onto}{⟶}\mathrm{ran}{I}$
7 f1of1 ${⊢}{I}:\mathrm{dom}{I}\underset{1-1 onto}{⟶}\mathrm{ran}{I}\to {I}:\mathrm{dom}{I}\underset{1-1}{⟶}\mathrm{ran}{I}$
8 6 7 syl ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {I}:\mathrm{dom}{I}\underset{1-1}{⟶}\mathrm{ran}{I}$