Theorem djhval2

Description: Value of subspace join for DVecH vector space. (Contributed by NM, 6-Aug-2014)

	Ref	Expression
Hypotheses	djhval.h	|- H = ( LHyp ` K )
	djhval.u	|- U = ( ( DVecH ` K ) ` W )
	djhval.v	|- V = ( Base ` U )
	djhval.o	|- ._|_ = ( ( ocH ` K ) ` W )
	djhval.j	|- .\/ = ( ( joinH ` K ) ` W )
Assertion	djhval2	|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( X .\/ Y ) = ( ._|_ ` ( ._|_ ` ( X u. Y ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		djhval.h	|- H = ( LHyp ` K )
2		djhval.u	|- U = ( ( DVecH ` K ) ` W )
3		djhval.v	|- V = ( Base ` U )
4		djhval.o	|- ._|_ = ( ( ocH ` K ) ` W )
5		djhval.j	|- .\/ = ( ( joinH ` K ) ` W )
6	1 2 3 4 5	djhval	|- ( ( ( K e. HL /\ W e. H ) /\ ( X C_ V /\ Y C_ V ) ) -> ( X .\/ Y ) = ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) )
7	6	3impb	|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( X .\/ Y ) = ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) )
8	1 2 3 4	dochdmj1	|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( ._|_ ` ( X u. Y ) ) = ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) )
9	8	fveq2d	|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( ._|_ ` ( ._|_ ` ( X u. Y ) ) ) = ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) )
10	7 9	eqtr4d	|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( X .\/ Y ) = ( ._|_ ` ( ._|_ ` ( X u. Y ) ) ) )