This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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