dalem35

Description: Lemma for dath . Analogue of dalem24 for I . (Contributed by NM, 3-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 ) ) ) )
	dalem34.m	\|- ./\ = ( meet ` K )
	dalem34.o	\|- O = ( LPlanes ` K )
	dalem34.y	\|- Y = ( ( P .\/ Q ) .\/ R )
	dalem34.z	\|- Z = ( ( S .\/ T ) .\/ U )
	dalem34.i	\|- I = ( ( c .\/ R ) ./\ ( d .\/ U ) )
Assertion	dalem35	\|- ( ( ph /\ Y = Z /\ ps ) -> -. I .<_ Y )

Proof

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		dalem34.m	\|- ./\ = ( meet ` K )
7		dalem34.o	\|- O = ( LPlanes ` K )
8		dalem34.y	\|- Y = ( ( P .\/ Q ) .\/ R )
9		dalem34.z	\|- Z = ( ( S .\/ T ) .\/ U )
10		dalem34.i	\|- I = ( ( c .\/ R ) ./\ ( d .\/ U ) )
11	1 2 3 4 8 9	dalemrot	\|- ( ph -> ( ( ( K e. HL /\ C e. ( Base ` K ) ) /\ ( Q e. A /\ R e. A /\ P e. A ) /\ ( T e. A /\ U e. A /\ S e. A ) ) /\ ( ( ( Q .\/ R ) .\/ P ) e. O /\ ( ( T .\/ U ) .\/ S ) e. O ) /\ ( ( -. C .<_ ( Q .\/ R ) /\ -. C .<_ ( R .\/ P ) /\ -. C .<_ ( P .\/ Q ) ) /\ ( -. C .<_ ( T .\/ U ) /\ -. C .<_ ( U .\/ S ) /\ -. C .<_ ( S .\/ T ) ) /\ ( C .<_ ( Q .\/ T ) /\ C .<_ ( R .\/ U ) /\ C .<_ ( P .\/ S ) ) ) ) )
12	11	3ad2ant1	\|- ( ( ph /\ Y = Z /\ ps ) -> ( ( ( K e. HL /\ C e. ( Base ` K ) ) /\ ( Q e. A /\ R e. A /\ P e. A ) /\ ( T e. A /\ U e. A /\ S e. A ) ) /\ ( ( ( Q .\/ R ) .\/ P ) e. O /\ ( ( T .\/ U ) .\/ S ) e. O ) /\ ( ( -. C .<_ ( Q .\/ R ) /\ -. C .<_ ( R .\/ P ) /\ -. C .<_ ( P .\/ Q ) ) /\ ( -. C .<_ ( T .\/ U ) /\ -. C .<_ ( U .\/ S ) /\ -. C .<_ ( S .\/ T ) ) /\ ( C .<_ ( Q .\/ T ) /\ C .<_ ( R .\/ U ) /\ C .<_ ( P .\/ S ) ) ) ) )
13	1 2 3 4 8 9	dalemrotyz	\|- ( ( ph /\ Y = Z ) -> ( ( Q .\/ R ) .\/ P ) = ( ( T .\/ U ) .\/ S ) )
14	13	3adant3	\|- ( ( ph /\ Y = Z /\ ps ) -> ( ( Q .\/ R ) .\/ P ) = ( ( T .\/ U ) .\/ S ) )
15	1 2 3 4 5 8	dalemrotps	\|- ( ( ph /\ ps ) -> ( ( c e. A /\ d e. A ) /\ -. c .<_ ( ( Q .\/ R ) .\/ P ) /\ ( d =/= c /\ -. d .<_ ( ( Q .\/ R ) .\/ P ) /\ C .<_ ( c .\/ d ) ) ) )
16	15	3adant2	\|- ( ( ph /\ Y = Z /\ ps ) -> ( ( c e. A /\ d e. A ) /\ -. c .<_ ( ( Q .\/ R ) .\/ P ) /\ ( d =/= c /\ -. d .<_ ( ( Q .\/ R ) .\/ P ) /\ C .<_ ( c .\/ d ) ) ) )
17		biid	\|- ( ( ( ( K e. HL /\ C e. ( Base ` K ) ) /\ ( Q e. A /\ R e. A /\ P e. A ) /\ ( T e. A /\ U e. A /\ S e. A ) ) /\ ( ( ( Q .\/ R ) .\/ P ) e. O /\ ( ( T .\/ U ) .\/ S ) e. O ) /\ ( ( -. C .<_ ( Q .\/ R ) /\ -. C .<_ ( R .\/ P ) /\ -. C .<_ ( P .\/ Q ) ) /\ ( -. C .<_ ( T .\/ U ) /\ -. C .<_ ( U .\/ S ) /\ -. C .<_ ( S .\/ T ) ) /\ ( C .<_ ( Q .\/ T ) /\ C .<_ ( R .\/ U ) /\ C .<_ ( P .\/ S ) ) ) ) <-> ( ( ( K e. HL /\ C e. ( Base ` K ) ) /\ ( Q e. A /\ R e. A /\ P e. A ) /\ ( T e. A /\ U e. A /\ S e. A ) ) /\ ( ( ( Q .\/ R ) .\/ P ) e. O /\ ( ( T .\/ U ) .\/ S ) e. O ) /\ ( ( -. C .<_ ( Q .\/ R ) /\ -. C .<_ ( R .\/ P ) /\ -. C .<_ ( P .\/ Q ) ) /\ ( -. C .<_ ( T .\/ U ) /\ -. C .<_ ( U .\/ S ) /\ -. C .<_ ( S .\/ T ) ) /\ ( C .<_ ( Q .\/ T ) /\ C .<_ ( R .\/ U ) /\ C .<_ ( P .\/ S ) ) ) ) )
18		biid	\|- ( ( ( c e. A /\ d e. A ) /\ -. c .<_ ( ( Q .\/ R ) .\/ P ) /\ ( d =/= c /\ -. d .<_ ( ( Q .\/ R ) .\/ P ) /\ C .<_ ( c .\/ d ) ) ) <-> ( ( c e. A /\ d e. A ) /\ -. c .<_ ( ( Q .\/ R ) .\/ P ) /\ ( d =/= c /\ -. d .<_ ( ( Q .\/ R ) .\/ P ) /\ C .<_ ( c .\/ d ) ) ) )
19		eqid	\|- ( ( Q .\/ R ) .\/ P ) = ( ( Q .\/ R ) .\/ P )
20		eqid	\|- ( ( T .\/ U ) .\/ S ) = ( ( T .\/ U ) .\/ S )
21	17 2 3 4 18 6 7 19 20 10	dalem30	\|- ( ( ( ( ( K e. HL /\ C e. ( Base ` K ) ) /\ ( Q e. A /\ R e. A /\ P e. A ) /\ ( T e. A /\ U e. A /\ S e. A ) ) /\ ( ( ( Q .\/ R ) .\/ P ) e. O /\ ( ( T .\/ U ) .\/ S ) e. O ) /\ ( ( -. C .<_ ( Q .\/ R ) /\ -. C .<_ ( R .\/ P ) /\ -. C .<_ ( P .\/ Q ) ) /\ ( -. C .<_ ( T .\/ U ) /\ -. C .<_ ( U .\/ S ) /\ -. C .<_ ( S .\/ T ) ) /\ ( C .<_ ( Q .\/ T ) /\ C .<_ ( R .\/ U ) /\ C .<_ ( P .\/ S ) ) ) ) /\ ( ( Q .\/ R ) .\/ P ) = ( ( T .\/ U ) .\/ S ) /\ ( ( c e. A /\ d e. A ) /\ -. c .<_ ( ( Q .\/ R ) .\/ P ) /\ ( d =/= c /\ -. d .<_ ( ( Q .\/ R ) .\/ P ) /\ C .<_ ( c .\/ d ) ) ) ) -> -. I .<_ ( ( Q .\/ R ) .\/ P ) )
22	12 14 16 21	syl3anc	\|- ( ( ph /\ Y = Z /\ ps ) -> -. I .<_ ( ( Q .\/ R ) .\/ P ) )
23	1 3 4	dalemqrprot	\|- ( ph -> ( ( Q .\/ R ) .\/ P ) = ( ( P .\/ Q ) .\/ R ) )
24	8 23	eqtr4id	\|- ( ph -> Y = ( ( Q .\/ R ) .\/ P ) )
25	24	breq2d	\|- ( ph -> ( I .<_ Y <-> I .<_ ( ( Q .\/ R ) .\/ P ) ) )
26	25	3ad2ant1	\|- ( ( ph /\ Y = Z /\ ps ) -> ( I .<_ Y <-> I .<_ ( ( Q .\/ R ) .\/ P ) ) )
27	22 26	mtbird	\|- ( ( ph /\ Y = Z /\ ps ) -> -. I .<_ Y )

Metamath Proof Explorer

Theorem dalem35

Proof