dalemcjden

Description: Lemma for dath . Show that the dummy atoms form a line. (Contributed by NM, 15-Aug-2012)

	Ref	Expression
Hypotheses	dalem.ph	\|- ( ph <-> ( ( ( K e. HL /\ C e. ( Base ` K ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) /\ ( Y e. O /\ Z e. O ) /\ ( ( -. C .<_ ( P .\/ Q ) /\ -. C .<_ ( Q .\/ R ) /\ -. C .<_ ( R .\/ P ) ) /\ ( -. C .<_ ( S .\/ T ) /\ -. C .<_ ( T .\/ U ) /\ -. C .<_ ( U .\/ S ) ) /\ ( C .<_ ( P .\/ S ) /\ C .<_ ( Q .\/ T ) /\ C .<_ ( R .\/ U ) ) ) ) )
	dalem.l	\|- .<_ = ( le ` K )
	dalem.j	\|- .\/ = ( join ` K )
	dalem.a	\|- A = ( Atoms ` K )
	dalem.ps	\|- ( ps <-> ( ( c e. A /\ d e. A ) /\ -. c .<_ Y /\ ( d =/= c /\ -. d .<_ Y /\ C .<_ ( c .\/ d ) ) ) )
Assertion	dalemcjden	\|- ( ( ph /\ ps ) -> ( c .\/ d ) e. ( LLines ` K ) )

Step	Hyp	Ref	Expression
1		dalem.ph	\|- ( ph <-> ( ( ( K e. HL /\ C e. ( Base ` K ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) /\ ( Y e. O /\ Z e. O ) /\ ( ( -. C .<_ ( P .\/ Q ) /\ -. C .<_ ( Q .\/ R ) /\ -. C .<_ ( R .\/ P ) ) /\ ( -. C .<_ ( S .\/ T ) /\ -. C .<_ ( T .\/ U ) /\ -. C .<_ ( U .\/ S ) ) /\ ( C .<_ ( P .\/ S ) /\ C .<_ ( Q .\/ T ) /\ C .<_ ( R .\/ U ) ) ) ) )
2		dalem.l	\|- .<_ = ( le ` K )
3		dalem.j	\|- .\/ = ( join ` K )
4		dalem.a	\|- A = ( Atoms ` K )
5		dalem.ps	\|- ( ps <-> ( ( c e. A /\ d e. A ) /\ -. c .<_ Y /\ ( d =/= c /\ -. d .<_ Y /\ C .<_ ( c .\/ d ) ) ) )
6	1	dalemkehl	\|- ( ph -> K e. HL )
7	6	adantr	\|- ( ( ph /\ ps ) -> K e. HL )
8	5	dalemccea	\|- ( ps -> c e. A )
9	8	adantl	\|- ( ( ph /\ ps ) -> c e. A )
10	5	dalemddea	\|- ( ps -> d e. A )
11	10	adantl	\|- ( ( ph /\ ps ) -> d e. A )
12	5	dalemccnedd	\|- ( ps -> c =/= d )
13	12	adantl	\|- ( ( ph /\ ps ) -> c =/= d )
14		eqid	\|- ( LLines ` K ) = ( LLines ` K )
15	3 4 14	llni2	\|- ( ( ( K e. HL /\ c e. A /\ d e. A ) /\ c =/= d ) -> ( c .\/ d ) e. ( LLines ` K ) )
16	7 9 11 13 15	syl31anc	\|- ( ( ph /\ ps ) -> ( c .\/ d ) e. ( LLines ` K ) )

Metamath Proof Explorer