# Metamath Proof Explorer

## Theorem dihprrn

Description: The span of a vector pair belongs to the range of isomorphism H i.e. is a closed subspace. (Contributed by NM, 29-Sep-2014)

Ref Expression
Hypotheses dihprrn.h
`|- H = ( LHyp ` K )`
dihprrn.u
`|- U = ( ( DVecH ` K ) ` W )`
dihprrn.v
`|- V = ( Base ` U )`
dihprrn.n
`|- N = ( LSpan ` U )`
dihprrn.i
`|- I = ( ( DIsoH ` K ) ` W )`
dihprrn.k
`|- ( ph -> ( K e. HL /\ W e. H ) )`
dihprrn.x
`|- ( ph -> X e. V )`
dihprrn.y
`|- ( ph -> Y e. V )`
Assertion dihprrn
`|- ( ph -> ( N ` { X , Y } ) e. ran I )`

### Proof

Step Hyp Ref Expression
1 dihprrn.h
` |-  H = ( LHyp ` K )`
2 dihprrn.u
` |-  U = ( ( DVecH ` K ) ` W )`
3 dihprrn.v
` |-  V = ( Base ` U )`
4 dihprrn.n
` |-  N = ( LSpan ` U )`
5 dihprrn.i
` |-  I = ( ( DIsoH ` K ) ` W )`
6 dihprrn.k
` |-  ( ph -> ( K e. HL /\ W e. H ) )`
7 dihprrn.x
` |-  ( ph -> X e. V )`
8 dihprrn.y
` |-  ( ph -> Y e. V )`
9 prcom
` |-  { X , Y } = { Y , X }`
10 preq2
` |-  ( X = ( 0g ` U ) -> { Y , X } = { Y , ( 0g ` U ) } )`
11 9 10 syl5eq
` |-  ( X = ( 0g ` U ) -> { X , Y } = { Y , ( 0g ` U ) } )`
12 11 fveq2d
` |-  ( X = ( 0g ` U ) -> ( N ` { X , Y } ) = ( N ` { Y , ( 0g ` U ) } ) )`
13 eqid
` |-  ( 0g ` U ) = ( 0g ` U )`
14 1 2 6 dvhlmod
` |-  ( ph -> U e. LMod )`
15 3 13 4 14 8 lsppr0
` |-  ( ph -> ( N ` { Y , ( 0g ` U ) } ) = ( N ` { Y } ) )`
16 12 15 sylan9eqr
` |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( N ` { X , Y } ) = ( N ` { Y } ) )`
17 1 2 3 4 5 dihlsprn
` |-  ( ( ( K e. HL /\ W e. H ) /\ Y e. V ) -> ( N ` { Y } ) e. ran I )`
18 6 8 17 syl2anc
` |-  ( ph -> ( N ` { Y } ) e. ran I )`
` |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( N ` { Y } ) e. ran I )`
20 16 19 eqeltrd
` |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( N ` { X , Y } ) e. ran I )`
21 preq2
` |-  ( Y = ( 0g ` U ) -> { X , Y } = { X , ( 0g ` U ) } )`
22 21 fveq2d
` |-  ( Y = ( 0g ` U ) -> ( N ` { X , Y } ) = ( N ` { X , ( 0g ` U ) } ) )`
23 3 13 4 14 7 lsppr0
` |-  ( ph -> ( N ` { X , ( 0g ` U ) } ) = ( N ` { X } ) )`
24 22 23 sylan9eqr
` |-  ( ( ph /\ Y = ( 0g ` U ) ) -> ( N ` { X , Y } ) = ( N ` { X } ) )`
25 1 2 3 4 5 dihlsprn
` |-  ( ( ( K e. HL /\ W e. H ) /\ X e. V ) -> ( N ` { X } ) e. ran I )`
26 6 7 25 syl2anc
` |-  ( ph -> ( N ` { X } ) e. ran I )`
` |-  ( ( ph /\ Y = ( 0g ` U ) ) -> ( N ` { X } ) e. ran I )`
28 24 27 eqeltrd
` |-  ( ( ph /\ Y = ( 0g ` U ) ) -> ( N ` { X , Y } ) e. ran I )`
` |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> ( K e. HL /\ W e. H ) )`
` |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> X e. V )`
` |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> Y e. V )`
` |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> X =/= ( 0g ` U ) )`
` |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> Y =/= ( 0g ` U ) )`
` |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> ( N ` { X , Y } ) e. ran I )`
` |-  ( ph -> ( N ` { X , Y } ) e. ran I )`