Theorem cdleml6

Description: Part of proof of Lemma L of Crawley p. 120. TODO: fix comment. (Contributed by NM, 11-Aug-2013)

	Ref	Expression
Hypotheses	cdleml6.b	|- B = ( Base ` K )
	cdleml6.j	|- .\/ = ( join ` K )
	cdleml6.m	|- ./\ = ( meet ` K )
	cdleml6.h	|- H = ( LHyp ` K )
	cdleml6.t	|- T = ( ( LTrn ` K ) ` W )
	cdleml6.r	|- R = ( ( trL ` K ) ` W )
	cdleml6.p	|- Q = ( ( oc ` K ) ` W )
	cdleml6.z	|- Z = ( ( Q .\/ ( R ` b ) ) ./\ ( ( h ` Q ) .\/ ( R ` ( b o. `' ( s ` h ) ) ) ) )
	cdleml6.y	|- Y = ( ( Q .\/ ( R ` g ) ) ./\ ( Z .\/ ( R ` ( g o. `' b ) ) ) )
	cdleml6.x	|- X = ( iota_ z e. T A. b e. T ( ( b =/= ( _I |` B ) /\ ( R ` b ) =/= ( R ` ( s ` h ) ) /\ ( R ` b ) =/= ( R ` g ) ) -> ( z ` Q ) = Y ) )
	cdleml6.u	|- U = ( g e. T |-> if ( ( s ` h ) = h , g , X ) )
	cdleml6.e	|- E = ( ( TEndo ` K ) ` W )
	cdleml6.o	|- .0. = ( f e. T |-> ( _I |` B ) )
Assertion	cdleml6	|- ( ( ( K e. HL /\ W e. H ) /\ h e. T /\ ( s e. E /\ s =/= .0. ) ) -> ( U e. E /\ ( U ` ( s ` h ) ) = h ) )

Proof

Step	Hyp	Ref	Expression
1		cdleml6.b	|- B = ( Base ` K )
2		cdleml6.j	|- .\/ = ( join ` K )
3		cdleml6.m	|- ./\ = ( meet ` K )
4		cdleml6.h	|- H = ( LHyp ` K )
5		cdleml6.t	|- T = ( ( LTrn ` K ) ` W )
6		cdleml6.r	|- R = ( ( trL ` K ) ` W )
7		cdleml6.p	|- Q = ( ( oc ` K ) ` W )
8		cdleml6.z	|- Z = ( ( Q .\/ ( R ` b ) ) ./\ ( ( h ` Q ) .\/ ( R ` ( b o. `' ( s ` h ) ) ) ) )
9		cdleml6.y	|- Y = ( ( Q .\/ ( R ` g ) ) ./\ ( Z .\/ ( R ` ( g o. `' b ) ) ) )
10		cdleml6.x	|- X = ( iota_ z e. T A. b e. T ( ( b =/= ( _I |` B ) /\ ( R ` b ) =/= ( R ` ( s ` h ) ) /\ ( R ` b ) =/= ( R ` g ) ) -> ( z ` Q ) = Y ) )
11		cdleml6.u	|- U = ( g e. T |-> if ( ( s ` h ) = h , g , X ) )
12		cdleml6.e	|- E = ( ( TEndo ` K ) ` W )
13		cdleml6.o	|- .0. = ( f e. T |-> ( _I |` B ) )
14		simp1	|- ( ( ( K e. HL /\ W e. H ) /\ h e. T /\ ( s e. E /\ s =/= .0. ) ) -> ( K e. HL /\ W e. H ) )
15		simp3l	|- ( ( ( K e. HL /\ W e. H ) /\ h e. T /\ ( s e. E /\ s =/= .0. ) ) -> s e. E )
16		simp2	|- ( ( ( K e. HL /\ W e. H ) /\ h e. T /\ ( s e. E /\ s =/= .0. ) ) -> h e. T )
17	4 5 12	tendocl	|- ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ h e. T ) -> ( s ` h ) e. T )
18	14 15 16 17	syl3anc	|- ( ( ( K e. HL /\ W e. H ) /\ h e. T /\ ( s e. E /\ s =/= .0. ) ) -> ( s ` h ) e. T )
19	1 4 5 6 12 13	tendotr	|- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ s =/= .0. ) /\ h e. T ) -> ( R ` ( s ` h ) ) = ( R ` h ) )
20	19	3com23	|- ( ( ( K e. HL /\ W e. H ) /\ h e. T /\ ( s e. E /\ s =/= .0. ) ) -> ( R ` ( s ` h ) ) = ( R ` h ) )
21		eqid	|- ( oc ` K ) = ( oc ` K )
22		eqid	|- ( Atoms ` K ) = ( Atoms ` K )
23	1 2 3 21 22 4 5 6 7 8 9 10 11 12	cdlemk56w	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( s ` h ) e. T /\ h e. T ) /\ ( R ` ( s ` h ) ) = ( R ` h ) ) -> ( U e. E /\ ( U ` ( s ` h ) ) = h ) )
24	14 18 16 20 23	syl121anc	|- ( ( ( K e. HL /\ W e. H ) /\ h e. T /\ ( s e. E /\ s =/= .0. ) ) -> ( U e. E /\ ( U ` ( s ` h ) ) = h ) )