dihord11c

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	dihord11c	\|- ( ( ( ( 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 ) ) ) -> E. y e. ( J ` N ) E. z e. ( I ` ( Y ./\ W ) ) <. f , O >. = ( y .+ z ) )

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		simp1	\|- ( ( ( ( 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 ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) )
19		simp2	\|- ( ( ( ( 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 /\ Y e. B ) )
20		simp31	\|- ( ( ( ( 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 ) ) ) -> ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) )
21		simp32	\|- ( ( ( ( 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 )
22		simp33	\|- ( ( ( ( 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 ) ) ) -> ( R ` f ) .<_ ( X ./\ W ) )
23	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	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 ) ) ) )
24	18 19 20 21 22 23	syl32anc	\|- ( ( ( ( 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 ) ) ) )
25		simp11	\|- ( ( ( ( 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 ) )
26	6 9 25	dvhlmod	\|- ( ( ( ( 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 ) ) ) -> U e. LMod )
27		eqid	\|- ( LSubSp ` U ) = ( LSubSp ` U )
28	27	lsssssubg	\|- ( U e. LMod -> ( LSubSp ` U ) C_ ( SubGrp ` U ) )
29	26 28	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 ) ) ) -> ( LSubSp ` U ) C_ ( SubGrp ` U ) )
30		simp13	\|- ( ( ( ( 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 ) ) ) -> ( N e. A /\ -. N .<_ W ) )
31	2 5 6 9 8 27	diclss	\|- ( ( ( K e. HL /\ W e. H ) /\ ( N e. A /\ -. N .<_ W ) ) -> ( J ` N ) e. ( LSubSp ` U ) )
32	25 30 31	syl2anc	\|- ( ( ( ( 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 ) ) ) -> ( J ` N ) e. ( LSubSp ` U ) )
33	29 32	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 ) ) ) -> ( J ` N ) e. ( SubGrp ` U ) )
34		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 ) ) ) /\ f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) ) -> K e. HL )
35	34	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 )
36		simp2r	\|- ( ( ( ( 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 ) ) ) -> Y e. B )
37		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 ) ) ) /\ f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) ) -> W e. H )
38	1 6	lhpbase	\|- ( W e. H -> W e. B )
39	37 38	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 )
40	1 4	latmcl	\|- ( ( K e. Lat /\ Y e. B /\ W e. B ) -> ( Y ./\ W ) e. B )
41	35 36 39 40	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 ) ) ) -> ( Y ./\ W ) e. B )
42	1 2 4	latmle2	\|- ( ( K e. Lat /\ Y e. B /\ W e. B ) -> ( Y ./\ W ) .<_ W )
43	35 36 39 42	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 ) ) ) -> ( Y ./\ W ) .<_ W )
44	1 2 6 9 7 27	diblss	\|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Y ./\ W ) e. B /\ ( Y ./\ W ) .<_ W ) ) -> ( I ` ( Y ./\ W ) ) e. ( LSubSp ` U ) )
45	25 41 43 44	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 ) ) ) -> ( I ` ( Y ./\ W ) ) e. ( LSubSp ` U ) )
46	29 45	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 ) ) ) -> ( I ` ( Y ./\ W ) ) e. ( SubGrp ` U ) )
47	16 10	lsmelval	\|- ( ( ( J ` N ) e. ( SubGrp ` U ) /\ ( I ` ( Y ./\ W ) ) e. ( SubGrp ` U ) ) -> ( <. f , O >. e. ( ( J ` N ) .(+) ( I ` ( Y ./\ W ) ) ) <-> E. y e. ( J ` N ) E. z e. ( I ` ( Y ./\ W ) ) <. f , O >. = ( y .+ z ) ) )
48	33 46 47	syl2anc	\|- ( ( ( ( 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 ) ) ) <-> E. y e. ( J ` N ) E. z e. ( I ` ( Y ./\ W ) ) <. f , O >. = ( y .+ z ) ) )
49	24 48	mpbid	\|- ( ( ( ( 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 ) ) ) -> E. y e. ( J ` N ) E. z e. ( I ` ( Y ./\ W ) ) <. f , O >. = ( y .+ z ) )

Metamath Proof Explorer

Theorem dihord11c

Proof