Theorem 4atexlemqtb

Description: Lemma for 4atexlem7 . (Contributed by NM, 24-Nov-2012)

	Ref	Expression
Hypotheses	4thatlem.ph	|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )
	4thatlempqb.j	|- .\/ = ( join ` K )
	4thatlempqb.a	|- A = ( Atoms ` K )
Assertion	4atexlemqtb	|- ( ph -> ( Q .\/ T ) e. ( Base ` K ) )

Proof

Step	Hyp	Ref	Expression
1		4thatlem.ph	|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )
2		4thatlempqb.j	|- .\/ = ( join ` K )
3		4thatlempqb.a	|- A = ( Atoms ` K )
4	1	4atexlemk	|- ( ph -> K e. HL )
5	1	4atexlemq	|- ( ph -> Q e. A )
6	1	4atexlemt	|- ( ph -> T e. A )
7		eqid	|- ( Base ` K ) = ( Base ` K )
8	7 2 3	hlatjcl	|- ( ( K e. HL /\ Q e. A /\ T e. A ) -> ( Q .\/ T ) e. ( Base ` K ) )
9	4 5 6 8	syl3anc	|- ( ph -> ( Q .\/ T ) e. ( Base ` K ) )