cdleme26f

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph, 6th and 7th lines on p. 115. F , N represent f(t), f_t(s) respectively. If t <_ t \/ v, then f_t(s) <_ f(t) \/ v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013)

	Ref	Expression
Hypotheses	cdleme26.b	\|- B = ( Base ` K )
	cdleme26.l	\|- .<_ = ( le ` K )
	cdleme26.j	\|- .\/ = ( join ` K )
	cdleme26.m	\|- ./\ = ( meet ` K )
	cdleme26.a	\|- A = ( Atoms ` K )
	cdleme26.h	\|- H = ( LHyp ` K )
	cdleme26f.u	\|- U = ( ( P .\/ Q ) ./\ W )
	cdleme26f.f	\|- F = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) )
	cdleme26f.n	\|- N = ( ( P .\/ Q ) ./\ ( F .\/ ( ( S .\/ t ) ./\ W ) ) )
	cdleme26f.i	\|- I = ( iota_ u e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> u = N ) )
Assertion	cdleme26f	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( -. t .<_ ( P .\/ Q ) /\ ( S =/= t /\ S .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> I .<_ ( F .\/ V ) )

Proof

Step	Hyp	Ref	Expression
1		cdleme26.b	\|- B = ( Base ` K )
2		cdleme26.l	\|- .<_ = ( le ` K )
3		cdleme26.j	\|- .\/ = ( join ` K )
4		cdleme26.m	\|- ./\ = ( meet ` K )
5		cdleme26.a	\|- A = ( Atoms ` K )
6		cdleme26.h	\|- H = ( LHyp ` K )
7		cdleme26f.u	\|- U = ( ( P .\/ Q ) ./\ W )
8		cdleme26f.f	\|- F = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) )
9		cdleme26f.n	\|- N = ( ( P .\/ Q ) ./\ ( F .\/ ( ( S .\/ t ) ./\ W ) ) )
10		cdleme26f.i	\|- I = ( iota_ u e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> u = N ) )
11		simp11	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( -. t .<_ ( P .\/ Q ) /\ ( S =/= t /\ S .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> ( K e. HL /\ W e. H ) )
12		simp21	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( -. t .<_ ( P .\/ Q ) /\ ( S =/= t /\ S .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> ( P e. A /\ -. P .<_ W ) )
13		simp22	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( -. t .<_ ( P .\/ Q ) /\ ( S =/= t /\ S .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
14		simp23l	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( -. t .<_ ( P .\/ Q ) /\ ( S =/= t /\ S .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> S e. A )
15		simp23r	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( -. t .<_ ( P .\/ Q ) /\ ( S =/= t /\ S .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> -. S .<_ W )
16		simp12l	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( -. t .<_ ( P .\/ Q ) /\ ( S =/= t /\ S .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> P =/= Q )
17		simp12r	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( -. t .<_ ( P .\/ Q ) /\ ( S =/= t /\ S .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> S .<_ ( P .\/ Q ) )
18	1 2 3 4 5 6 7 8 9 10	cdleme25cl	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ -. S .<_ W ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) -> I e. B )
19	11 12 13 14 15 16 17 18	syl322anc	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( -. t .<_ ( P .\/ Q ) /\ ( S =/= t /\ S .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> I e. B )
20		simp13l	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( -. t .<_ ( P .\/ Q ) /\ ( S =/= t /\ S .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> t e. A )
21		simp13r	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( -. t .<_ ( P .\/ Q ) /\ ( S =/= t /\ S .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> -. t .<_ W )
22		simp31	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( -. t .<_ ( P .\/ Q ) /\ ( S =/= t /\ S .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> -. t .<_ ( P .\/ Q ) )
23	1	fvexi	\|- B e. _V
24	23 10	riotasv	\|- ( ( I e. B /\ t e. A /\ ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) ) -> I = N )
25	19 20 21 22 24	syl112anc	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( -. t .<_ ( P .\/ Q ) /\ ( S =/= t /\ S .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> I = N )
26		simp23	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( -. t .<_ ( P .\/ Q ) /\ ( S =/= t /\ S .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> ( S e. A /\ -. S .<_ W ) )
27		simp33	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( -. t .<_ ( P .\/ Q ) /\ ( S =/= t /\ S .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> ( V e. A /\ V .<_ W ) )
28		simp32	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( -. t .<_ ( P .\/ Q ) /\ ( S =/= t /\ S .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> ( S =/= t /\ S .<_ ( t .\/ V ) ) )
29	2 3 4 5 6 7 8 9	cdleme22f	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ t e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= t /\ S .<_ ( t .\/ V ) ) ) -> N .<_ ( F .\/ V ) )
30	11 12 13 26 20 27 28 29	syl331anc	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( -. t .<_ ( P .\/ Q ) /\ ( S =/= t /\ S .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> N .<_ ( F .\/ V ) )
31	25 30	eqbrtrd	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( -. t .<_ ( P .\/ Q ) /\ ( S =/= t /\ S .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> I .<_ ( F .\/ V ) )

Metamath Proof Explorer

Theorem cdleme26f

Proof