dalem53

Description: Lemma for dath . The auxiliary axis of perspectivity B is a line (analogous to the actual axis of perspectivity X in dalem15 . (Contributed by NM, 8-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 ) ) ) )
	dalem53.m	\|- ./\ = ( meet ` K )
	dalem53.n	\|- N = ( LLines ` K )
	dalem53.o	\|- O = ( LPlanes ` K )
	dalem53.y	\|- Y = ( ( P .\/ Q ) .\/ R )
	dalem53.z	\|- Z = ( ( S .\/ T ) .\/ U )
	dalem53.g	\|- G = ( ( c .\/ P ) ./\ ( d .\/ S ) )
	dalem53.h	\|- H = ( ( c .\/ Q ) ./\ ( d .\/ T ) )
	dalem53.i	\|- I = ( ( c .\/ R ) ./\ ( d .\/ U ) )
	dalem53.b1	\|- B = ( ( ( G .\/ H ) .\/ I ) ./\ Y )
Assertion	dalem53	\|- ( ( ph /\ Y = Z /\ ps ) -> B e. N )

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		dalem53.m	\|- ./\ = ( meet ` K )
7		dalem53.n	\|- N = ( LLines ` K )
8		dalem53.o	\|- O = ( LPlanes ` K )
9		dalem53.y	\|- Y = ( ( P .\/ Q ) .\/ R )
10		dalem53.z	\|- Z = ( ( S .\/ T ) .\/ U )
11		dalem53.g	\|- G = ( ( c .\/ P ) ./\ ( d .\/ S ) )
12		dalem53.h	\|- H = ( ( c .\/ Q ) ./\ ( d .\/ T ) )
13		dalem53.i	\|- I = ( ( c .\/ R ) ./\ ( d .\/ U ) )
14		dalem53.b1	\|- B = ( ( ( G .\/ H ) .\/ I ) ./\ Y )
15	1 2 3 4 5 6 8 9 10 11 12 13	dalem51	\|- ( ( ph /\ Y = Z /\ ps ) -> ( ( ( ( K e. HL /\ c e. A ) /\ ( G e. A /\ H e. A /\ I e. A ) /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( ( ( G .\/ H ) .\/ I ) e. O /\ Y e. O ) /\ ( ( -. c .<_ ( G .\/ H ) /\ -. c .<_ ( H .\/ I ) /\ -. c .<_ ( I .\/ G ) ) /\ ( -. c .<_ ( P .\/ Q ) /\ -. c .<_ ( Q .\/ R ) /\ -. c .<_ ( R .\/ P ) ) /\ ( c .<_ ( G .\/ P ) /\ c .<_ ( H .\/ Q ) /\ c .<_ ( I .\/ R ) ) ) ) /\ ( ( G .\/ H ) .\/ I ) =/= Y ) )
16		eqid	\|- ( Base ` K ) = ( Base ` K )
17	16 4	atbase	\|- ( c e. A -> c e. ( Base ` K ) )
18	17	anim2i	\|- ( ( K e. HL /\ c e. A ) -> ( K e. HL /\ c e. ( Base ` K ) ) )
19	18	3anim1i	\|- ( ( ( K e. HL /\ c e. A ) /\ ( G e. A /\ H e. A /\ I e. A ) /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( K e. HL /\ c e. ( Base ` K ) ) /\ ( G e. A /\ H e. A /\ I e. A ) /\ ( P e. A /\ Q e. A /\ R e. A ) ) )
20		biid	\|- ( ( ( ( K e. HL /\ c e. ( Base ` K ) ) /\ ( G e. A /\ H e. A /\ I e. A ) /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( ( ( G .\/ H ) .\/ I ) e. O /\ Y e. O ) /\ ( ( -. c .<_ ( G .\/ H ) /\ -. c .<_ ( H .\/ I ) /\ -. c .<_ ( I .\/ G ) ) /\ ( -. c .<_ ( P .\/ Q ) /\ -. c .<_ ( Q .\/ R ) /\ -. c .<_ ( R .\/ P ) ) /\ ( c .<_ ( G .\/ P ) /\ c .<_ ( H .\/ Q ) /\ c .<_ ( I .\/ R ) ) ) ) <-> ( ( ( K e. HL /\ c e. ( Base ` K ) ) /\ ( G e. A /\ H e. A /\ I e. A ) /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( ( ( G .\/ H ) .\/ I ) e. O /\ Y e. O ) /\ ( ( -. c .<_ ( G .\/ H ) /\ -. c .<_ ( H .\/ I ) /\ -. c .<_ ( I .\/ G ) ) /\ ( -. c .<_ ( P .\/ Q ) /\ -. c .<_ ( Q .\/ R ) /\ -. c .<_ ( R .\/ P ) ) /\ ( c .<_ ( G .\/ P ) /\ c .<_ ( H .\/ Q ) /\ c .<_ ( I .\/ R ) ) ) ) )
21		eqid	\|- ( ( G .\/ H ) .\/ I ) = ( ( G .\/ H ) .\/ I )
22	20 2 3 4 6 7 8 21 9 14	dalem15	\|- ( ( ( ( ( K e. HL /\ c e. ( Base ` K ) ) /\ ( G e. A /\ H e. A /\ I e. A ) /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( ( ( G .\/ H ) .\/ I ) e. O /\ Y e. O ) /\ ( ( -. c .<_ ( G .\/ H ) /\ -. c .<_ ( H .\/ I ) /\ -. c .<_ ( I .\/ G ) ) /\ ( -. c .<_ ( P .\/ Q ) /\ -. c .<_ ( Q .\/ R ) /\ -. c .<_ ( R .\/ P ) ) /\ ( c .<_ ( G .\/ P ) /\ c .<_ ( H .\/ Q ) /\ c .<_ ( I .\/ R ) ) ) ) /\ ( ( G .\/ H ) .\/ I ) =/= Y ) -> B e. N )
23	19 22	syl3anl1	\|- ( ( ( ( ( K e. HL /\ c e. A ) /\ ( G e. A /\ H e. A /\ I e. A ) /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( ( ( G .\/ H ) .\/ I ) e. O /\ Y e. O ) /\ ( ( -. c .<_ ( G .\/ H ) /\ -. c .<_ ( H .\/ I ) /\ -. c .<_ ( I .\/ G ) ) /\ ( -. c .<_ ( P .\/ Q ) /\ -. c .<_ ( Q .\/ R ) /\ -. c .<_ ( R .\/ P ) ) /\ ( c .<_ ( G .\/ P ) /\ c .<_ ( H .\/ Q ) /\ c .<_ ( I .\/ R ) ) ) ) /\ ( ( G .\/ H ) .\/ I ) =/= Y ) -> B e. N )
24	15 23	syl	\|- ( ( ph /\ Y = Z /\ ps ) -> B e. N )

Metamath Proof Explorer

Theorem dalem53

Proof