cdlemkuv2

Description: Part of proof of Lemma K of Crawley p. 118. Line 16 on p. 119 for i = 1, where sigma_1 (p) is U , f_1 is D , and k_1 is O . (Contributed by NM, 2-Jul-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cdlemk1.b	\|- B = ( Base ` K )
2		cdlemk1.l	\|- .<_ = ( le ` K )
3		cdlemk1.j	\|- .\/ = ( join ` K )
4		cdlemk1.m	\|- ./\ = ( meet ` K )
5		cdlemk1.a	\|- A = ( Atoms ` K )
6		cdlemk1.h	\|- H = ( LHyp ` K )
7		cdlemk1.t	\|- T = ( ( LTrn ` K ) ` W )
8		cdlemk1.r	\|- R = ( ( trL ` K ) ` W )
9		cdlemk1.s	\|- S = ( f e. T \|-> ( iota_ i e. T ( i ` P ) = ( ( P .\/ ( R ` f ) ) ./\ ( ( N ` P ) .\/ ( R ` ( f o. `' F ) ) ) ) ) )
10		cdlemk1.o	\|- O = ( S ` D )
11		cdlemk1.u	\|- U = ( e e. T \|-> ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( O ` P ) .\/ ( R ` ( e o. `' D ) ) ) ) ) )
12		simp13	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) /\ G e. T ) /\ ( F e. T /\ D e. T /\ N e. T ) /\ ( ( ( R ` D ) =/= ( R ` F ) /\ ( R ` D ) =/= ( R ` G ) ) /\ ( F =/= ( _I \|` B ) /\ G =/= ( _I \|` B ) /\ D =/= ( _I \|` B ) ) /\ ( P e. A /\ -. P .<_ W ) ) ) -> G e. T )
13	1 2 3 5 6 7 8 4 11	cdlemksv	\|- ( G e. T -> ( U ` G ) = ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( O ` P ) .\/ ( R ` ( G o. `' D ) ) ) ) ) )
14	12 13	syl	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) /\ G e. T ) /\ ( F e. T /\ D e. T /\ N e. T ) /\ ( ( ( R ` D ) =/= ( R ` F ) /\ ( R ` D ) =/= ( R ` G ) ) /\ ( F =/= ( _I \|` B ) /\ G =/= ( _I \|` B ) /\ D =/= ( _I \|` B ) ) /\ ( P e. A /\ -. P .<_ W ) ) ) -> ( U ` G ) = ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( O ` P ) .\/ ( R ` ( G o. `' D ) ) ) ) ) )
15	14	eqcomd	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) /\ G e. T ) /\ ( F e. T /\ D e. T /\ N e. T ) /\ ( ( ( R ` D ) =/= ( R ` F ) /\ ( R ` D ) =/= ( R ` G ) ) /\ ( F =/= ( _I \|` B ) /\ G =/= ( _I \|` B ) /\ D =/= ( _I \|` B ) ) /\ ( P e. A /\ -. P .<_ W ) ) ) -> ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( O ` P ) .\/ ( R ` ( G o. `' D ) ) ) ) ) = ( U ` G ) )
16	1 2 3 4 5 6 7 8 9 10 11	cdlemkuel	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) /\ G e. T ) /\ ( F e. T /\ D e. T /\ N e. T ) /\ ( ( ( R ` D ) =/= ( R ` F ) /\ ( R ` D ) =/= ( R ` G ) ) /\ ( F =/= ( _I \|` B ) /\ G =/= ( _I \|` B ) /\ D =/= ( _I \|` B ) ) /\ ( P e. A /\ -. P .<_ W ) ) ) -> ( U ` G ) e. T )
17		simp11l	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) /\ G e. T ) /\ ( F e. T /\ D e. T /\ N e. T ) /\ ( ( ( R ` D ) =/= ( R ` F ) /\ ( R ` D ) =/= ( R ` G ) ) /\ ( F =/= ( _I \|` B ) /\ G =/= ( _I \|` B ) /\ D =/= ( _I \|` B ) ) /\ ( P e. A /\ -. P .<_ W ) ) ) -> K e. HL )
18		simp11r	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) /\ G e. T ) /\ ( F e. T /\ D e. T /\ N e. T ) /\ ( ( ( R ` D ) =/= ( R ` F ) /\ ( R ` D ) =/= ( R ` G ) ) /\ ( F =/= ( _I \|` B ) /\ G =/= ( _I \|` B ) /\ D =/= ( _I \|` B ) ) /\ ( P e. A /\ -. P .<_ W ) ) ) -> W e. H )
19		simp33	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) /\ G e. T ) /\ ( F e. T /\ D e. T /\ N e. T ) /\ ( ( ( R ` D ) =/= ( R ` F ) /\ ( R ` D ) =/= ( R ` G ) ) /\ ( F =/= ( _I \|` B ) /\ G =/= ( _I \|` B ) /\ D =/= ( _I \|` B ) ) /\ ( P e. A /\ -. P .<_ W ) ) ) -> ( P e. A /\ -. P .<_ W ) )
20	1 2 3 4 5 6 7 8 9 10	cdlemk16a	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) /\ G e. T ) /\ ( F e. T /\ D e. T /\ N e. T ) /\ ( ( ( R ` D ) =/= ( R ` F ) /\ ( R ` D ) =/= ( R ` G ) ) /\ ( F =/= ( _I \|` B ) /\ G =/= ( _I \|` B ) /\ D =/= ( _I \|` B ) ) /\ ( P e. A /\ -. P .<_ W ) ) ) -> ( ( ( P .\/ ( R ` G ) ) ./\ ( ( O ` P ) .\/ ( R ` ( G o. `' D ) ) ) ) e. A /\ -. ( ( P .\/ ( R ` G ) ) ./\ ( ( O ` P ) .\/ ( R ` ( G o. `' D ) ) ) ) .<_ W ) )
21	2 5 6 7	cdleme	\|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( ( ( P .\/ ( R ` G ) ) ./\ ( ( O ` P ) .\/ ( R ` ( G o. `' D ) ) ) ) e. A /\ -. ( ( P .\/ ( R ` G ) ) ./\ ( ( O ` P ) .\/ ( R ` ( G o. `' D ) ) ) ) .<_ W ) ) -> E! j e. T ( j ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( O ` P ) .\/ ( R ` ( G o. `' D ) ) ) ) )
22	17 18 19 20 21	syl211anc	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) /\ G e. T ) /\ ( F e. T /\ D e. T /\ N e. T ) /\ ( ( ( R ` D ) =/= ( R ` F ) /\ ( R ` D ) =/= ( R ` G ) ) /\ ( F =/= ( _I \|` B ) /\ G =/= ( _I \|` B ) /\ D =/= ( _I \|` B ) ) /\ ( P e. A /\ -. P .<_ W ) ) ) -> E! j e. T ( j ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( O ` P ) .\/ ( R ` ( G o. `' D ) ) ) ) )
23		nfcv	\|- F/_ j T
24		nfriota1	\|- F/_ j ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( O ` P ) .\/ ( R ` ( e o. `' D ) ) ) ) )
25	23 24	nfmpt	\|- F/_ j ( e e. T \|-> ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( O ` P ) .\/ ( R ` ( e o. `' D ) ) ) ) ) )
26	11 25	nfcxfr	\|- F/_ j U
27		nfcv	\|- F/_ j G
28	26 27	nffv	\|- F/_ j ( U ` G )
29		nfcv	\|- F/_ j P
30	28 29	nffv	\|- F/_ j ( ( U ` G ) ` P )
31	30	nfeq1	\|- F/ j ( ( U ` G ) ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( O ` P ) .\/ ( R ` ( G o. `' D ) ) ) )
32		fveq1	\|- ( j = ( U ` G ) -> ( j ` P ) = ( ( U ` G ) ` P ) )
33	32	eqeq1d	\|- ( j = ( U ` G ) -> ( ( j ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( O ` P ) .\/ ( R ` ( G o. `' D ) ) ) ) <-> ( ( U ` G ) ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( O ` P ) .\/ ( R ` ( G o. `' D ) ) ) ) ) )
34	28 31 33	riota2f	\|- ( ( ( U ` G ) e. T /\ E! j e. T ( j ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( O ` P ) .\/ ( R ` ( G o. `' D ) ) ) ) ) -> ( ( ( U ` G ) ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( O ` P ) .\/ ( R ` ( G o. `' D ) ) ) ) <-> ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( O ` P ) .\/ ( R ` ( G o. `' D ) ) ) ) ) = ( U ` G ) ) )
35	16 22 34	syl2anc	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) /\ G e. T ) /\ ( F e. T /\ D e. T /\ N e. T ) /\ ( ( ( R ` D ) =/= ( R ` F ) /\ ( R ` D ) =/= ( R ` G ) ) /\ ( F =/= ( _I \|` B ) /\ G =/= ( _I \|` B ) /\ D =/= ( _I \|` B ) ) /\ ( P e. A /\ -. P .<_ W ) ) ) -> ( ( ( U ` G ) ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( O ` P ) .\/ ( R ` ( G o. `' D ) ) ) ) <-> ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( O ` P ) .\/ ( R ` ( G o. `' D ) ) ) ) ) = ( U ` G ) ) )
36	15 35	mpbird	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) /\ G e. T ) /\ ( F e. T /\ D e. T /\ N e. T ) /\ ( ( ( R ` D ) =/= ( R ` F ) /\ ( R ` D ) =/= ( R ` G ) ) /\ ( F =/= ( _I \|` B ) /\ G =/= ( _I \|` B ) /\ D =/= ( _I \|` B ) ) /\ ( P e. A /\ -. P .<_ W ) ) ) -> ( ( U ` G ) ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( O ` P ) .\/ ( R ` ( G o. `' D ) ) ) ) )

Metamath Proof Explorer

Theorem cdlemkuv2

Proof