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 )

Metamath Proof Explorer

Theorem dihprrn

Proof