cdlemk22-3

Description: Part of proof of Lemma K of Crawley p. 118. Lines 26-27, p. 119 for i=1 and j=2. (Contributed by NM, 7-Jul-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cdlemk3.b	\|- B = ( Base ` K )
2		cdlemk3.l	\|- .<_ = ( le ` K )
3		cdlemk3.j	\|- .\/ = ( join ` K )
4		cdlemk3.m	\|- ./\ = ( meet ` K )
5		cdlemk3.a	\|- A = ( Atoms ` K )
6		cdlemk3.h	\|- H = ( LHyp ` K )
7		cdlemk3.t	\|- T = ( ( LTrn ` K ) ` W )
8		cdlemk3.r	\|- R = ( ( trL ` K ) ` W )
9		cdlemk3.s	\|- S = ( f e. T \|-> ( iota_ i e. T ( i ` P ) = ( ( P .\/ ( R ` f ) ) ./\ ( ( N ` P ) .\/ ( R ` ( f o. `' F ) ) ) ) ) )
10		cdlemk3.u1	\|- Y = ( d e. T , e e. T \|-> ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( ( S ` d ) ` P ) .\/ ( R ` ( e o. `' d ) ) ) ) ) )
11		eqid	\|- ( S ` C ) = ( S ` C )
12		eqid	\|- ( e e. T \|-> ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( ( S ` C ) ` P ) .\/ ( R ` ( e o. `' C ) ) ) ) ) ) = ( e e. T \|-> ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( ( S ` C ) ` P ) .\/ ( R ` ( e o. `' C ) ) ) ) ) )
13		eqid	\|- ( S ` D ) = ( S ` D )
14		eqid	\|- ( e e. T \|-> ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( ( S ` D ) ` P ) .\/ ( R ` ( e o. `' D ) ) ) ) ) ) = ( e e. T \|-> ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( ( S ` D ) ` P ) .\/ ( R ` ( e o. `' D ) ) ) ) ) )
15	1 2 3 4 5 6 7 8 9 11 12 13 14	cdlemk22	\|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ D e. T ) /\ ( ( N e. T /\ G e. T /\ C e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I \|` B ) /\ D =/= ( _I \|` B ) /\ G =/= ( _I \|` B ) ) /\ ( C =/= ( _I \|` B ) /\ ( R ` G ) =/= ( R ` C ) /\ ( R ` C ) =/= ( R ` F ) ) /\ ( ( R ` D ) =/= ( R ` F ) /\ ( R ` G ) =/= ( R ` D ) /\ ( R ` C ) =/= ( R ` D ) ) ) ) -> ( ( ( e e. T \|-> ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( ( S ` D ) ` P ) .\/ ( R ` ( e o. `' D ) ) ) ) ) ) ` G ) ` P ) = ( ( ( e e. T \|-> ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( ( S ` C ) ` P ) .\/ ( R ` ( e o. `' C ) ) ) ) ) ) ` G ) ` P ) )
16		simp13	\|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ D e. T ) /\ ( ( N e. T /\ G e. T /\ C e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I \|` B ) /\ D =/= ( _I \|` B ) /\ G =/= ( _I \|` B ) ) /\ ( C =/= ( _I \|` B ) /\ ( R ` G ) =/= ( R ` C ) /\ ( R ` C ) =/= ( R ` F ) ) /\ ( ( R ` D ) =/= ( R ` F ) /\ ( R ` G ) =/= ( R ` D ) /\ ( R ` C ) =/= ( R ` D ) ) ) ) -> D e. T )
17		simp212	\|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ D e. T ) /\ ( ( N e. T /\ G e. T /\ C e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I \|` B ) /\ D =/= ( _I \|` B ) /\ G =/= ( _I \|` B ) ) /\ ( C =/= ( _I \|` B ) /\ ( R ` G ) =/= ( R ` C ) /\ ( R ` C ) =/= ( R ` F ) ) /\ ( ( R ` D ) =/= ( R ` F ) /\ ( R ` G ) =/= ( R ` D ) /\ ( R ` C ) =/= ( R ` D ) ) ) ) -> G e. T )
18	1 2 3 4 5 6 7 8 9 10 13 14	cdlemkuu	\|- ( ( D e. T /\ G e. T ) -> ( D Y G ) = ( ( e e. T \|-> ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( ( S ` D ) ` P ) .\/ ( R ` ( e o. `' D ) ) ) ) ) ) ` G ) )
19	16 17 18	syl2anc	\|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ D e. T ) /\ ( ( N e. T /\ G e. T /\ C e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I \|` B ) /\ D =/= ( _I \|` B ) /\ G =/= ( _I \|` B ) ) /\ ( C =/= ( _I \|` B ) /\ ( R ` G ) =/= ( R ` C ) /\ ( R ` C ) =/= ( R ` F ) ) /\ ( ( R ` D ) =/= ( R ` F ) /\ ( R ` G ) =/= ( R ` D ) /\ ( R ` C ) =/= ( R ` D ) ) ) ) -> ( D Y G ) = ( ( e e. T \|-> ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( ( S ` D ) ` P ) .\/ ( R ` ( e o. `' D ) ) ) ) ) ) ` G ) )
20	19	fveq1d	\|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ D e. T ) /\ ( ( N e. T /\ G e. T /\ C e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I \|` B ) /\ D =/= ( _I \|` B ) /\ G =/= ( _I \|` B ) ) /\ ( C =/= ( _I \|` B ) /\ ( R ` G ) =/= ( R ` C ) /\ ( R ` C ) =/= ( R ` F ) ) /\ ( ( R ` D ) =/= ( R ` F ) /\ ( R ` G ) =/= ( R ` D ) /\ ( R ` C ) =/= ( R ` D ) ) ) ) -> ( ( D Y G ) ` P ) = ( ( ( e e. T \|-> ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( ( S ` D ) ` P ) .\/ ( R ` ( e o. `' D ) ) ) ) ) ) ` G ) ` P ) )
21		simp213	\|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ D e. T ) /\ ( ( N e. T /\ G e. T /\ C e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I \|` B ) /\ D =/= ( _I \|` B ) /\ G =/= ( _I \|` B ) ) /\ ( C =/= ( _I \|` B ) /\ ( R ` G ) =/= ( R ` C ) /\ ( R ` C ) =/= ( R ` F ) ) /\ ( ( R ` D ) =/= ( R ` F ) /\ ( R ` G ) =/= ( R ` D ) /\ ( R ` C ) =/= ( R ` D ) ) ) ) -> C e. T )
22	1 2 3 4 5 6 7 8 9 10 11 12	cdlemkuu	\|- ( ( C e. T /\ G e. T ) -> ( C Y G ) = ( ( e e. T \|-> ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( ( S ` C ) ` P ) .\/ ( R ` ( e o. `' C ) ) ) ) ) ) ` G ) )
23	21 17 22	syl2anc	\|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ D e. T ) /\ ( ( N e. T /\ G e. T /\ C e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I \|` B ) /\ D =/= ( _I \|` B ) /\ G =/= ( _I \|` B ) ) /\ ( C =/= ( _I \|` B ) /\ ( R ` G ) =/= ( R ` C ) /\ ( R ` C ) =/= ( R ` F ) ) /\ ( ( R ` D ) =/= ( R ` F ) /\ ( R ` G ) =/= ( R ` D ) /\ ( R ` C ) =/= ( R ` D ) ) ) ) -> ( C Y G ) = ( ( e e. T \|-> ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( ( S ` C ) ` P ) .\/ ( R ` ( e o. `' C ) ) ) ) ) ) ` G ) )
24	23	fveq1d	\|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ D e. T ) /\ ( ( N e. T /\ G e. T /\ C e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I \|` B ) /\ D =/= ( _I \|` B ) /\ G =/= ( _I \|` B ) ) /\ ( C =/= ( _I \|` B ) /\ ( R ` G ) =/= ( R ` C ) /\ ( R ` C ) =/= ( R ` F ) ) /\ ( ( R ` D ) =/= ( R ` F ) /\ ( R ` G ) =/= ( R ` D ) /\ ( R ` C ) =/= ( R ` D ) ) ) ) -> ( ( C Y G ) ` P ) = ( ( ( e e. T \|-> ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( ( S ` C ) ` P ) .\/ ( R ` ( e o. `' C ) ) ) ) ) ) ` G ) ` P ) )
25	15 20 24	3eqtr4d	\|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ D e. T ) /\ ( ( N e. T /\ G e. T /\ C e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I \|` B ) /\ D =/= ( _I \|` B ) /\ G =/= ( _I \|` B ) ) /\ ( C =/= ( _I \|` B ) /\ ( R ` G ) =/= ( R ` C ) /\ ( R ` C ) =/= ( R ` F ) ) /\ ( ( R ` D ) =/= ( R ` F ) /\ ( R ` G ) =/= ( R ` D ) /\ ( R ` C ) =/= ( R ` D ) ) ) ) -> ( ( D Y G ) ` P ) = ( ( C Y G ) ` P ) )

Metamath Proof Explorer

Theorem cdlemk22-3

Proof