Theorem diaclN

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 𝐼 )

Proof

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 𝐼 )