dihord10

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	dihord10	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ ( ( s e. E /\ g e. T ) /\ ( R ` g ) .<_ ( Y ./\ W ) /\ <. f , O >. = ( <. ( s ` G ) , s >. .+ <. g , O >. ) ) ) -> ( R ` f ) .<_ ( 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		simp11	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ ( ( s e. E /\ g e. T ) /\ ( R ` g ) .<_ ( Y ./\ W ) /\ <. f , O >. = ( <. ( s ` G ) , s >. .+ <. g , O >. ) ) ) -> ( K e. HL /\ W e. H ) )
19		simp12	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ ( ( s e. E /\ g e. T ) /\ ( R ` g ) .<_ ( Y ./\ W ) /\ <. f , O >. = ( <. ( s ` G ) , s >. .+ <. g , O >. ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
20		simp13	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ ( ( s e. E /\ g e. T ) /\ ( R ` g ) .<_ ( Y ./\ W ) /\ <. f , O >. = ( <. ( s ` G ) , s >. .+ <. g , O >. ) ) ) -> ( N e. A /\ -. N .<_ W ) )
21		simp31l	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ ( ( s e. E /\ g e. T ) /\ ( R ` g ) .<_ ( Y ./\ W ) /\ <. f , O >. = ( <. ( s ` G ) , s >. .+ <. g , O >. ) ) ) -> s e. E )
22		simp31r	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ ( ( s e. E /\ g e. T ) /\ ( R ` g ) .<_ ( Y ./\ W ) /\ <. f , O >. = ( <. ( s ` G ) , s >. .+ <. g , O >. ) ) ) -> g e. T )
23		simp33	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ ( ( s e. E /\ g e. T ) /\ ( R ` g ) .<_ ( Y ./\ W ) /\ <. f , O >. = ( <. ( s ` G ) , s >. .+ <. g , O >. ) ) ) -> <. f , O >. = ( <. ( s ` G ) , s >. .+ <. g , O >. ) )
24	1 2 5 6 14 13 11 15 9 16 17	dihordlem7b	\|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( s e. E /\ g e. T /\ <. f , O >. = ( <. ( s ` G ) , s >. .+ <. g , O >. ) ) ) -> ( f = g /\ O = s ) )
25	24	simpld	\|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( s e. E /\ g e. T /\ <. f , O >. = ( <. ( s ` G ) , s >. .+ <. g , O >. ) ) ) -> f = g )
26	18 19 20 21 22 23 25	syl123anc	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ ( ( s e. E /\ g e. T ) /\ ( R ` g ) .<_ ( Y ./\ W ) /\ <. f , O >. = ( <. ( s ` G ) , s >. .+ <. g , O >. ) ) ) -> f = g )
27	26	fveq2d	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ ( ( s e. E /\ g e. T ) /\ ( R ` g ) .<_ ( Y ./\ W ) /\ <. f , O >. = ( <. ( s ` G ) , s >. .+ <. g , O >. ) ) ) -> ( R ` f ) = ( R ` g ) )
28		simp32	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ ( ( s e. E /\ g e. T ) /\ ( R ` g ) .<_ ( Y ./\ W ) /\ <. f , O >. = ( <. ( s ` G ) , s >. .+ <. g , O >. ) ) ) -> ( R ` g ) .<_ ( Y ./\ W ) )
29	27 28	eqbrtrd	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ ( ( s e. E /\ g e. T ) /\ ( R ` g ) .<_ ( Y ./\ W ) /\ <. f , O >. = ( <. ( s ` G ) , s >. .+ <. g , O >. ) ) ) -> ( R ` f ) .<_ ( Y ./\ W ) )

Metamath Proof Explorer

Theorem dihord10

Proof