Metamath Proof Explorer


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 HL W H X T Y T X J Y 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 HL W H X T Y T X J Y = ocA K W ocA K W X ocA K W Y
7 inss1 ocA K W X ocA K W Y ocA K W X
8 1 2 3 5 docaclN K HL W H X T ocA K W X ran I
9 8 adantrr K HL W H X T Y T ocA K W X ran I
10 1 2 3 diaelrnN K HL W H ocA K W X ran I ocA K W X T
11 9 10 syldan K HL W H X T Y T ocA K W X T
12 7 11 sstrid K HL W H X T Y T ocA K W X ocA K W Y T
13 1 2 3 5 docaclN K HL W H ocA K W X ocA K W Y T ocA K W ocA K W X ocA K W Y ran I
14 12 13 syldan K HL W H X T Y T ocA K W ocA K W X ocA K W Y ran I
15 6 14 eqeltrd K HL W H X T Y T X J Y ran I