cdleme20bN

Description: Part of proof of Lemma E in Crawley p. 113, last paragraph on p. 114, second line. D , F , Y , G represent s_2, f(s), t_2, f(t). We show v \/ s_2 = v \/ t_2. (Contributed by NM, 15-Nov-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdleme19.l	\|- .<_ = ( le ` K )
	cdleme19.j	\|- .\/ = ( join ` K )
	cdleme19.m	\|- ./\ = ( meet ` K )
	cdleme19.a	\|- A = ( Atoms ` K )
	cdleme19.h	\|- H = ( LHyp ` K )
	cdleme19.u	\|- U = ( ( P .\/ Q ) ./\ W )
	cdleme19.f	\|- F = ( ( S .\/ U ) ./\ ( Q .\/ ( ( P .\/ S ) ./\ W ) ) )
	cdleme19.g	\|- G = ( ( T .\/ U ) ./\ ( Q .\/ ( ( P .\/ T ) ./\ W ) ) )
	cdleme19.d	\|- D = ( ( R .\/ S ) ./\ W )
	cdleme19.y	\|- Y = ( ( R .\/ T ) ./\ W )
	cdleme20.v	\|- V = ( ( S .\/ T ) ./\ W )
Assertion	cdleme20bN	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> ( V .\/ D ) = ( V .\/ Y ) )

Proof

Step	Hyp	Ref	Expression
1		cdleme19.l	\|- .<_ = ( le ` K )
2		cdleme19.j	\|- .\/ = ( join ` K )
3		cdleme19.m	\|- ./\ = ( meet ` K )
4		cdleme19.a	\|- A = ( Atoms ` K )
5		cdleme19.h	\|- H = ( LHyp ` K )
6		cdleme19.u	\|- U = ( ( P .\/ Q ) ./\ W )
7		cdleme19.f	\|- F = ( ( S .\/ U ) ./\ ( Q .\/ ( ( P .\/ S ) ./\ W ) ) )
8		cdleme19.g	\|- G = ( ( T .\/ U ) ./\ ( Q .\/ ( ( P .\/ T ) ./\ W ) ) )
9		cdleme19.d	\|- D = ( ( R .\/ S ) ./\ W )
10		cdleme19.y	\|- Y = ( ( R .\/ T ) ./\ W )
11		cdleme20.v	\|- V = ( ( S .\/ T ) ./\ W )
12		simp1l	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> K e. HL )
13	12	hllatd	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> K e. Lat )
14		simp22l	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> S e. A )
15		eqid	\|- ( Base ` K ) = ( Base ` K )
16	15 4	atbase	\|- ( S e. A -> S e. ( Base ` K ) )
17	14 16	syl	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> S e. ( Base ` K ) )
18		simp21	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> R e. A )
19	15 4	atbase	\|- ( R e. A -> R e. ( Base ` K ) )
20	18 19	syl	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> R e. ( Base ` K ) )
21		simp23l	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> T e. A )
22	15 4	atbase	\|- ( T e. A -> T e. ( Base ` K ) )
23	21 22	syl	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> T e. ( Base ` K ) )
24	15 2	latj31	\|- ( ( K e. Lat /\ ( S e. ( Base ` K ) /\ R e. ( Base ` K ) /\ T e. ( Base ` K ) ) ) -> ( ( S .\/ R ) .\/ T ) = ( ( T .\/ R ) .\/ S ) )
25	13 17 20 23 24	syl13anc	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> ( ( S .\/ R ) .\/ T ) = ( ( T .\/ R ) .\/ S ) )
26	25	oveq1d	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> ( ( ( S .\/ R ) .\/ T ) ./\ W ) = ( ( ( T .\/ R ) .\/ S ) ./\ W ) )
27		simp1r	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> W e. H )
28		simp22r	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> -. S .<_ W )
29		simp31	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> -. S .<_ ( P .\/ Q ) )
30		simp33	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> R .<_ ( P .\/ Q ) )
31	1 2 3 4 5 6 7 8 9 10 11	cdleme20aN	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. S .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> ( V .\/ D ) = ( ( ( S .\/ R ) .\/ T ) ./\ W ) )
32	12 27 18 14 28 21 29 30 31	syl233anc	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> ( V .\/ D ) = ( ( ( S .\/ R ) .\/ T ) ./\ W ) )
33	2 4	hlatjcom	\|- ( ( K e. HL /\ S e. A /\ T e. A ) -> ( S .\/ T ) = ( T .\/ S ) )
34	12 14 21 33	syl3anc	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> ( S .\/ T ) = ( T .\/ S ) )
35	34	oveq1d	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> ( ( S .\/ T ) ./\ W ) = ( ( T .\/ S ) ./\ W ) )
36	11 35	syl5eq	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> V = ( ( T .\/ S ) ./\ W ) )
37	36	oveq1d	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> ( V .\/ Y ) = ( ( ( T .\/ S ) ./\ W ) .\/ Y ) )
38		simp23r	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> -. T .<_ W )
39		simp32	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> -. T .<_ ( P .\/ Q ) )
40		eqid	\|- ( ( T .\/ S ) ./\ W ) = ( ( T .\/ S ) ./\ W )
41	1 2 3 4 5 6 8 7 10 9 40	cdleme20aN	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ T e. A /\ -. T .<_ W ) /\ ( S e. A /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> ( ( ( T .\/ S ) ./\ W ) .\/ Y ) = ( ( ( T .\/ R ) .\/ S ) ./\ W ) )
42	12 27 18 21 38 14 39 30 41	syl233anc	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> ( ( ( T .\/ S ) ./\ W ) .\/ Y ) = ( ( ( T .\/ R ) .\/ S ) ./\ W ) )
43	37 42	eqtrd	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> ( V .\/ Y ) = ( ( ( T .\/ R ) .\/ S ) ./\ W ) )
44	26 32 43	3eqtr4d	\|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> ( V .\/ D ) = ( V .\/ Y ) )

Metamath Proof Explorer

Theorem cdleme20bN

Proof