Theorem cdlemksel

Description: Part of proof of Lemma K of Crawley p. 118. Conditions for the sigma(p) function to be a translation. TODO: combine cdlemki ? (Contributed by NM, 26-Jun-2013)

	Ref	Expression
Hypotheses	cdlemk.b	|- B = ( Base ` K )
	cdlemk.l	|- .<_ = ( le ` K )
	cdlemk.j	|- .\/ = ( join ` K )
	cdlemk.a	|- A = ( Atoms ` K )
	cdlemk.h	|- H = ( LHyp ` K )
	cdlemk.t	|- T = ( ( LTrn ` K ) ` W )
	cdlemk.r	|- R = ( ( trL ` K ) ` W )
	cdlemk.m	|- ./\ = ( meet ` K )
	cdlemk.s	|- S = ( f e. T |-> ( iota_ i e. T ( i ` P ) = ( ( P .\/ ( R ` f ) ) ./\ ( ( N ` P ) .\/ ( R ` ( f o. `' F ) ) ) ) ) )
Assertion	cdlemksel	|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` F ) ) ) -> ( S ` G ) e. T )

Proof

Step	Hyp	Ref	Expression
1		cdlemk.b	|- B = ( Base ` K )
2		cdlemk.l	|- .<_ = ( le ` K )
3		cdlemk.j	|- .\/ = ( join ` K )
4		cdlemk.a	|- A = ( Atoms ` K )
5		cdlemk.h	|- H = ( LHyp ` K )
6		cdlemk.t	|- T = ( ( LTrn ` K ) ` W )
7		cdlemk.r	|- R = ( ( trL ` K ) ` W )
8		cdlemk.m	|- ./\ = ( meet ` K )
9		cdlemk.s	|- S = ( f e. T |-> ( iota_ i e. T ( i ` P ) = ( ( P .\/ ( R ` f ) ) ./\ ( ( N ` P ) .\/ ( R ` ( f o. `' F ) ) ) ) ) )
10		simp13	|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` F ) ) ) -> G e. T )
11	1 2 3 4 5 6 7 8 9	cdlemksv	|- ( G e. T -> ( S ` G ) = ( iota_ i e. T ( i ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( N ` P ) .\/ ( R ` ( G o. `' F ) ) ) ) ) )
12	10 11	syl	|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` F ) ) ) -> ( S ` G ) = ( iota_ i e. T ( i ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( N ` P ) .\/ ( R ` ( G o. `' F ) ) ) ) ) )
13		eqid	|- ( iota_ i e. T ( i ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( N ` P ) .\/ ( R ` ( G o. `' F ) ) ) ) ) = ( iota_ i e. T ( i ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( N ` P ) .\/ ( R ` ( G o. `' F ) ) ) ) )
14	1 2 3 4 5 6 7 8 13	cdlemki	|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` F ) ) ) -> ( iota_ i e. T ( i ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( N ` P ) .\/ ( R ` ( G o. `' F ) ) ) ) ) e. T )
15	12 14	eqeltrd	|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` F ) ) ) -> ( S ` G ) e. T )