Description: Closure of partial isomorphism A for a lattice K . (Contributed by NM, 4-Dec-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dia1o.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | |
dia1o.i | ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) | ||
Assertion | diaclN | ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑋 ) ∈ ran 𝐼 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dia1o.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | |
2 | dia1o.i | ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) | |
3 | 1 2 | diaf11N | ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 ) |
4 | f1ofun | ⊢ ( 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 → Fun 𝐼 ) | |
5 | 3 4 | syl | ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → Fun 𝐼 ) |
6 | fvelrn | ⊢ ( ( Fun 𝐼 ∧ 𝑋 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑋 ) ∈ ran 𝐼 ) | |
7 | 5 6 | sylan | ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑋 ) ∈ ran 𝐼 ) |