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=LHyp⁡K
dvadia.u ⊢U=DVecA⁡K⁡W
dvadia.i ⊢I=DIsoA⁡K⁡W
dvadia.n ⊢⊥˙=ocA⁡K⁡W
dvadia.s ⊢S=LSubSp⁡U
Assertion diaf1oN ⊢K∈HL∧W∈H→I:dom⁡I⟶1-1 ontox∈S|⊥˙⁡⊥˙⁡x=x

Proof

Step Hyp Ref Expression
1 dvadia.h ⊢H=LHyp⁡K
2 dvadia.u ⊢U=DVecA⁡K⁡W
3 dvadia.i ⊢I=DIsoA⁡K⁡W
4 dvadia.n ⊢⊥˙=ocA⁡K⁡W
5 dvadia.s ⊢S=LSubSp⁡U
6 1 3 diaf11N ⊢K∈HL∧W∈H→I:dom⁡I⟶1-1 ontoran⁡I
7 f1of1 ⊢I:dom⁡I⟶1-1 ontoran⁡I→I:dom⁡I⟶1-1ran⁡I
8 6 7 syl ⊢K∈HL∧W∈H→I:dom⁡I⟶1-1ran⁡I
9 1 2 3 4 5 diarnN ⊢K∈HL∧W∈H→ran⁡I=x∈S|⊥˙⁡⊥˙⁡x=x
10 f1eq3 ⊢ran⁡I=x∈S|⊥˙⁡⊥˙⁡x=x→I:dom⁡I⟶1-1ran⁡I↔I:dom⁡I⟶1-1x∈S|⊥˙⁡⊥˙⁡x=x
11 9 10 syl ⊢K∈HL∧W∈H→I:dom⁡I⟶1-1ran⁡I↔I:dom⁡I⟶1-1x∈S|⊥˙⁡⊥˙⁡x=x
12 8 11 mpbid ⊢K∈HL∧W∈H→I:dom⁡I⟶1-1x∈S|⊥˙⁡⊥˙⁡x=x
13 dff1o5 ⊢I:dom⁡I⟶1-1 ontox∈S|⊥˙⁡⊥˙⁡x=x↔I:dom⁡I⟶1-1x∈S|⊥˙⁡⊥˙⁡x=x∧ran⁡I=x∈S|⊥˙⁡⊥˙⁡x=x
14 12 9 13 sylanbrc ⊢K∈HL∧W∈H→I:dom⁡I⟶1-1 ontox∈S|⊥˙⁡⊥˙⁡x=x