dihord11b

Description: Part of proof after Lemma N of Crawley p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014)

	Ref	Expression
Hypotheses	dihjust.b	\|- B = ( Base ` K )
	dihjust.l	\|- .<_ = ( le ` K )
	dihjust.j	\|- .\/ = ( join ` K )
	dihjust.m	\|- ./\ = ( meet ` K )
	dihjust.a	\|- A = ( Atoms ` K )
	dihjust.h	\|- H = ( LHyp ` K )
	dihjust.i	\|- I = ( ( DIsoB ` K ) ` W )
	dihjust.J	\|- J = ( ( DIsoC ` K ) ` W )
	dihjust.u	\|- U = ( ( DVecH ` K ) ` W )
	dihjust.s	\|- .(+) = ( LSSum ` U )
	dihord2c.t	\|- T = ( ( LTrn ` K ) ` W )
	dihord2c.r	\|- R = ( ( trL ` K ) ` W )
	dihord2c.o	\|- O = ( h e. T \|-> ( _I \|` B ) )
	dihord2.p	\|- P = ( ( oc ` K ) ` W )
	dihord2.e	\|- E = ( ( TEndo ` K ) ` W )
	dihord2.d	\|- .+ = ( +g ` U )
	dihord2.g	\|- G = ( iota_ h e. T ( h ` P ) = N )
Assertion	dihord11b	\|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) ) -> <. f , O >. e. ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dihjust.b	\|- B = ( Base ` K )
2		dihjust.l	\|- .<_ = ( le ` K )
3		dihjust.j	\|- .\/ = ( join ` K )
4		dihjust.m	\|- ./\ = ( meet ` K )
5		dihjust.a	\|- A = ( Atoms ` K )
6		dihjust.h	\|- H = ( LHyp ` K )
7		dihjust.i	\|- I = ( ( DIsoB ` K ) ` W )
8		dihjust.J	\|- J = ( ( DIsoC ` K ) ` W )
9		dihjust.u	\|- U = ( ( DVecH ` K ) ` W )
10		dihjust.s	\|- .(+) = ( LSSum ` U )
11		dihord2c.t	\|- T = ( ( LTrn ` K ) ` W )
12		dihord2c.r	\|- R = ( ( trL ` K ) ` W )
13		dihord2c.o	\|- O = ( h e. T \|-> ( _I \|` B ) )
14		dihord2.p	\|- P = ( ( oc ` K ) ` W )
15		dihord2.e	\|- E = ( ( TEndo ` K ) ` W )
16		dihord2.d	\|- .+ = ( +g ` U )
17		dihord2.g	\|- G = ( iota_ h e. T ( h ` P ) = N )
18	1 2 3 4 5 6 7 8 9 10	dihord2b	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) ) -> ( I ` ( X ./\ W ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) )
19	18	adantr	\|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) ) -> ( I ` ( X ./\ W ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) )
20		simpr	\|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) ) -> ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) )
21		eqidd	\|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) ) -> O = O )
22		simpl11	\|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) ) -> ( K e. HL /\ W e. H ) )
23		simp11l	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) ) -> K e. HL )
24	23	adantr	\|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) ) -> K e. HL )
25	24	hllatd	\|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) ) -> K e. Lat )
26		simpl2l	\|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) ) -> X e. B )
27		simp11r	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) ) -> W e. H )
28	27	adantr	\|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) ) -> W e. H )
29	1 6	lhpbase	\|- ( W e. H -> W e. B )
30	28 29	syl	\|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) ) -> W e. B )
31	1 4	latmcl	\|- ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ./\ W ) e. B )
32	25 26 30 31	syl3anc	\|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) ) -> ( X ./\ W ) e. B )
33	1 2 4	latmle2	\|- ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ./\ W ) .<_ W )
34	25 26 30 33	syl3anc	\|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) ) -> ( X ./\ W ) .<_ W )
35	1 2 6 11 12 13 7	dibopelval3	\|- ( ( ( K e. HL /\ W e. H ) /\ ( ( X ./\ W ) e. B /\ ( X ./\ W ) .<_ W ) ) -> ( <. f , O >. e. ( I ` ( X ./\ W ) ) <-> ( ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ O = O ) ) )
36	22 32 34 35	syl12anc	\|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) ) -> ( <. f , O >. e. ( I ` ( X ./\ W ) ) <-> ( ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ O = O ) ) )
37	20 21 36	mpbir2and	\|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) ) -> <. f , O >. e. ( I ` ( X ./\ W ) ) )
38	19 37	sseldd	\|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) ) -> <. f , O >. e. ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) )

Metamath Proof Explorer

Theorem dihord11b

Proof