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 eqtrid 
 |-  ( 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 )
19 18 adantr 
 |-  ( ( 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 )
27 26 adantr 
 |-  ( ( ph /\ Y = ( 0g ` U ) ) -> ( N ` { X } ) e. ran I )
28 24 27 eqeltrd 
 |-  ( ( ph /\ Y = ( 0g ` U ) ) -> ( N ` { X , Y } ) e. ran I )
29 6 adantr 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> ( K e. HL /\ W e. H ) )
30 7 adantr 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> X e. V )
31 8 adantr 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> Y e. V )
32 simprl 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> X =/= ( 0g ` U ) )
33 simprr 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> Y =/= ( 0g ` U ) )
34 1 2 3 4 5 29 30 31 13 32 33 dihprrnlem2 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> ( N ` { X , Y } ) e. ran I )
35 20 28 34 pm2.61da2ne 
 |-  ( ph -> ( N ` { X , Y } ) e. ran I )