Theorem dia1elN

Description: The largest subspace in the range of partial isomorphism A. (Contributed by NM, 5-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dia1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dia1.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	dia1.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
Assertion	dia1elN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑇 ∈ ran 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		dia1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dia1.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3		dia1.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
4	1 2 3	dia1N	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ 𝑊 ) = 𝑇 )
5	1 3	diaf11N	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 )
6		f1ofun	⊢ ( 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 → Fun 𝐼 )
7	5 6	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → Fun 𝐼 )
8	1 3	dia1eldmN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ∈ dom 𝐼 )
9		fvelrn	⊢ ( ( Fun 𝐼 ∧ 𝑊 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑊 ) ∈ ran 𝐼 )
10	7 8 9	syl2anc	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ 𝑊 ) ∈ ran 𝐼 )
11	4 10	eqeltrrd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑇 ∈ ran 𝐼 )