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 ⊢ H = LHyp ⁡ K
dia1.t ⊢ T = LTrn ⁡ K ⁡ W
dia1.i ⊢ I = DIsoA ⁡ K ⁡ W
Assertion dia1elN ⊢ K ∈ HL ∧ W ∈ H → T ∈ ran ⁡ I

Proof

Step Hyp Ref Expression
1 dia1.h ⊢ H = LHyp ⁡ K
2 dia1.t ⊢ T = LTrn ⁡ K ⁡ W
3 dia1.i ⊢ I = DIsoA ⁡ K ⁡ W
4 1 2 3 dia1N ⊢ K ∈ HL ∧ W ∈ H → I ⁡ W = T
5 1 3 diaf11N ⊢ K ∈ HL ∧ W ∈ H → I : dom ⁡ I ⟶ 1-1 onto ran ⁡ I
6 f1ofun ⊢ I : dom ⁡ I ⟶ 1-1 onto ran ⁡ I → Fun ⁡ I
7 5 6 syl ⊢ K ∈ HL ∧ W ∈ H → Fun ⁡ I
8 1 3 dia1eldmN ⊢ K ∈ HL ∧ W ∈ H → W ∈ dom ⁡ I
9 fvelrn ⊢ Fun ⁡ I ∧ W ∈ dom ⁡ I → I ⁡ W ∈ ran ⁡ I
10 7 8 9 syl2anc ⊢ K ∈ HL ∧ W ∈ H → I ⁡ W ∈ ran ⁡ I
11 4 10 eqeltrrd ⊢ K ∈ HL ∧ W ∈ H → T ∈ ran ⁡ I