cdlemn5

Description: Part of proof of Lemma N of Crawley p. 121 line 32. (Contributed by NM, 25-Feb-2014)

	Ref	Expression
Hypotheses	cdlemn5.b	\|- B = ( Base ` K )
	cdlemn5.l	\|- .<_ = ( le ` K )
	cdlemn5.j	\|- .\/ = ( join ` K )
	cdlemn5.a	\|- A = ( Atoms ` K )
	cdlemn5.h	\|- H = ( LHyp ` K )
	cdlemn5.u	\|- U = ( ( DVecH ` K ) ` W )
	cdlemn5.s	\|- .(+) = ( LSSum ` U )
	cdlemn5.i	\|- I = ( ( DIsoB ` K ) ` W )
	cdlemn5.J	\|- J = ( ( DIsoC ` K ) ` W )
Assertion	cdlemn5	\|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ R .<_ ( Q .\/ X ) ) -> ( J ` R ) C_ ( ( J ` Q ) .(+) ( I ` X ) ) )

Step	Hyp	Ref	Expression
1		cdlemn5.b	\|- B = ( Base ` K )
2		cdlemn5.l	\|- .<_ = ( le ` K )
3		cdlemn5.j	\|- .\/ = ( join ` K )
4		cdlemn5.a	\|- A = ( Atoms ` K )
5		cdlemn5.h	\|- H = ( LHyp ` K )
6		cdlemn5.u	\|- U = ( ( DVecH ` K ) ` W )
7		cdlemn5.s	\|- .(+) = ( LSSum ` U )
8		cdlemn5.i	\|- I = ( ( DIsoB ` K ) ` W )
9		cdlemn5.J	\|- J = ( ( DIsoC ` K ) ` W )
10		eqid	\|- ( ( oc ` K ) ` W ) = ( ( oc ` K ) ` W )
11		eqid	\|- ( h e. ( ( LTrn ` K ) ` W ) \|-> ( _I \|` B ) ) = ( h e. ( ( LTrn ` K ) ` W ) \|-> ( _I \|` B ) )
12		eqid	\|- ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
13		eqid	\|- ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
14		eqid	\|- ( LSpan ` U ) = ( LSpan ` U )
15		eqid	\|- ( iota_ h e. ( ( LTrn ` K ) ` W ) ( h ` ( ( oc ` K ) ` W ) ) = Q ) = ( iota_ h e. ( ( LTrn ` K ) ` W ) ( h ` ( ( oc ` K ) ` W ) ) = Q )
16		eqid	\|- ( iota_ h e. ( ( LTrn ` K ) ` W ) ( h ` ( ( oc ` K ) ` W ) ) = R ) = ( iota_ h e. ( ( LTrn ` K ) ` W ) ( h ` ( ( oc ` K ) ` W ) ) = R )
17		eqid	\|- ( iota_ h e. ( ( LTrn ` K ) ` W ) ( h ` Q ) = R ) = ( iota_ h e. ( ( LTrn ` K ) ` W ) ( h ` Q ) = R )
18	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	cdlemn5pre	\|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) /\ ( X e. B /\ X .<_ W ) ) /\ R .<_ ( Q .\/ X ) ) -> ( J ` R ) C_ ( ( J ` Q ) .(+) ( I ` X ) ) )

Metamath Proof Explorer