Theorem djaclN

Description: Closure of subspace join for DVecA partial vector space. (Contributed by NM, 5-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	djacl.h	|- H = ( LHyp ` K )
	djacl.t	|- T = ( ( LTrn ` K ) ` W )
	djacl.i	|- I = ( ( DIsoA ` K ) ` W )
	djacl.j	|- J = ( ( vA ` K ) ` W )
Assertion	djaclN	|- ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> ( X J Y ) e. ran I )

Proof

Step	Hyp	Ref	Expression
1		djacl.h	|- H = ( LHyp ` K )
2		djacl.t	|- T = ( ( LTrn ` K ) ` W )
3		djacl.i	|- I = ( ( DIsoA ` K ) ` W )
4		djacl.j	|- J = ( ( vA ` K ) ` W )
5		eqid	|- ( ( ocA ` K ) ` W ) = ( ( ocA ` K ) ` W )
6	1 2 3 5 4	djavalN	|- ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> ( X J Y ) = ( ( ( ocA ` K ) ` W ) ` ( ( ( ( ocA ` K ) ` W ) ` X ) i^i ( ( ( ocA ` K ) ` W ) ` Y ) ) ) )
7		inss1	|- ( ( ( ( ocA ` K ) ` W ) ` X ) i^i ( ( ( ocA ` K ) ` W ) ` Y ) ) C_ ( ( ( ocA ` K ) ` W ) ` X )
8	1 2 3 5	docaclN	|- ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( ( ( ocA ` K ) ` W ) ` X ) e. ran I )
9	8	adantrr	|- ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> ( ( ( ocA ` K ) ` W ) ` X ) e. ran I )
10	1 2 3	diaelrnN	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( ( ocA ` K ) ` W ) ` X ) e. ran I ) -> ( ( ( ocA ` K ) ` W ) ` X ) C_ T )
11	9 10	syldan	|- ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> ( ( ( ocA ` K ) ` W ) ` X ) C_ T )
12	7 11	sstrid	|- ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> ( ( ( ( ocA ` K ) ` W ) ` X ) i^i ( ( ( ocA ` K ) ` W ) ` Y ) ) C_ T )
13	1 2 3 5	docaclN	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( ( ( ocA ` K ) ` W ) ` X ) i^i ( ( ( ocA ` K ) ` W ) ` Y ) ) C_ T ) -> ( ( ( ocA ` K ) ` W ) ` ( ( ( ( ocA ` K ) ` W ) ` X ) i^i ( ( ( ocA ` K ) ` W ) ` Y ) ) ) e. ran I )
14	12 13	syldan	|- ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> ( ( ( ocA ` K ) ` W ) ` ( ( ( ( ocA ` K ) ` W ) ` X ) i^i ( ( ( ocA ` K ) ` W ) ` Y ) ) ) e. ran I )
15	6 14	eqeltrd	|- ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> ( X J Y ) e. ran I )