Theorem lcfrlem18

Description: Lemma for lcfr . (Contributed by NM, 24-Feb-2015)

	Ref	Expression
Hypotheses	lcfrlem17.h	|- H = ( LHyp ` K )
	lcfrlem17.o	|- ._|_ = ( ( ocH ` K ) ` W )
	lcfrlem17.u	|- U = ( ( DVecH ` K ) ` W )
	lcfrlem17.v	|- V = ( Base ` U )
	lcfrlem17.p	|- .+ = ( +g ` U )
	lcfrlem17.z	|- .0. = ( 0g ` U )
	lcfrlem17.n	|- N = ( LSpan ` U )
	lcfrlem17.a	|- A = ( LSAtoms ` U )
	lcfrlem17.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	lcfrlem17.x	|- ( ph -> X e. ( V \ { .0. } ) )
	lcfrlem17.y	|- ( ph -> Y e. ( V \ { .0. } ) )
	lcfrlem17.ne	|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
Assertion	lcfrlem18	|- ( ph -> ( ._|_ ` { X , Y } ) = ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) )

Proof

Step	Hyp	Ref	Expression
1		lcfrlem17.h	|- H = ( LHyp ` K )
2		lcfrlem17.o	|- ._|_ = ( ( ocH ` K ) ` W )
3		lcfrlem17.u	|- U = ( ( DVecH ` K ) ` W )
4		lcfrlem17.v	|- V = ( Base ` U )
5		lcfrlem17.p	|- .+ = ( +g ` U )
6		lcfrlem17.z	|- .0. = ( 0g ` U )
7		lcfrlem17.n	|- N = ( LSpan ` U )
8		lcfrlem17.a	|- A = ( LSAtoms ` U )
9		lcfrlem17.k	|- ( ph -> ( K e. HL /\ W e. H ) )
10		lcfrlem17.x	|- ( ph -> X e. ( V \ { .0. } ) )
11		lcfrlem17.y	|- ( ph -> Y e. ( V \ { .0. } ) )
12		lcfrlem17.ne	|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
13		df-pr	|- { X , Y } = ( { X } u. { Y } )
14	13	fveq2i	|- ( ._|_ ` { X , Y } ) = ( ._|_ ` ( { X } u. { Y } ) )
15	10	eldifad	|- ( ph -> X e. V )
16	15	snssd	|- ( ph -> { X } C_ V )
17	11	eldifad	|- ( ph -> Y e. V )
18	17	snssd	|- ( ph -> { Y } C_ V )
19	1 3 4 2	dochdmj1	|- ( ( ( K e. HL /\ W e. H ) /\ { X } C_ V /\ { Y } C_ V ) -> ( ._|_ ` ( { X } u. { Y } ) ) = ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) )
20	9 16 18 19	syl3anc	|- ( ph -> ( ._|_ ` ( { X } u. { Y } ) ) = ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) )
21	14 20	syl5eq	|- ( ph -> ( ._|_ ` { X , Y } ) = ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) )