Theorem cdlemd5

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 30-May-2012)

	Ref	Expression
Hypotheses	cdlemd4.l	|- .<_ = ( le ` K )
	cdlemd4.j	|- .\/ = ( join ` K )
	cdlemd4.a	|- A = ( Atoms ` K )
	cdlemd4.h	|- H = ( LHyp ` K )
	cdlemd4.t	|- T = ( ( LTrn ` K ) ` W )
Assertion	cdlemd5	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ P =/= Q ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( F ` R ) = ( G ` R ) )

Proof

Step	Hyp	Ref	Expression
1		cdlemd4.l	|- .<_ = ( le ` K )
2		cdlemd4.j	|- .\/ = ( join ` K )
3		cdlemd4.a	|- A = ( Atoms ` K )
4		cdlemd4.h	|- H = ( LHyp ` K )
5		cdlemd4.t	|- T = ( ( LTrn ` K ) ` W )
6		fveq2	|- ( R = P -> ( F ` R ) = ( F ` P ) )
7		fveq2	|- ( R = P -> ( G ` R ) = ( G ` P ) )
8	6 7	eqeq12d	|- ( R = P -> ( ( F ` R ) = ( G ` R ) <-> ( F ` P ) = ( G ` P ) ) )
9		simpll1	|- ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ P =/= Q ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ R .<_ ( P .\/ Q ) ) /\ R =/= P ) -> ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) )
10		simpl21	|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ P =/= Q ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ R .<_ ( P .\/ Q ) ) -> ( P e. A /\ -. P .<_ W ) )
11	10	adantr	|- ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ P =/= Q ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ R .<_ ( P .\/ Q ) ) /\ R =/= P ) -> ( P e. A /\ -. P .<_ W ) )
12		simpl22	|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ P =/= Q ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ R .<_ ( P .\/ Q ) ) -> ( Q e. A /\ -. Q .<_ W ) )
13	12	adantr	|- ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ P =/= Q ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ R .<_ ( P .\/ Q ) ) /\ R =/= P ) -> ( Q e. A /\ -. Q .<_ W ) )
14		simp23	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ P =/= Q ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> P =/= Q )
15	14	ad2antrr	|- ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ P =/= Q ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ R .<_ ( P .\/ Q ) ) /\ R =/= P ) -> P =/= Q )
16		simplr	|- ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ P =/= Q ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ R .<_ ( P .\/ Q ) ) /\ R =/= P ) -> R .<_ ( P .\/ Q ) )
17		simpr	|- ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ P =/= Q ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ R .<_ ( P .\/ Q ) ) /\ R =/= P ) -> R =/= P )
18	15 16 17	3jca	|- ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ P =/= Q ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ R .<_ ( P .\/ Q ) ) /\ R =/= P ) -> ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) )
19		simpll3	|- ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ P =/= Q ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ R .<_ ( P .\/ Q ) ) /\ R =/= P ) -> ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) )
20	1 2 3 4 5	cdlemd4	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( F ` R ) = ( G ` R ) )
21	9 11 13 18 19 20	syl131anc	|- ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ P =/= Q ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ R .<_ ( P .\/ Q ) ) /\ R =/= P ) -> ( F ` R ) = ( G ` R ) )
22		simpl3l	|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ P =/= Q ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ R .<_ ( P .\/ Q ) ) -> ( F ` P ) = ( G ` P ) )
23	8 21 22	pm2.61ne	|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ P =/= Q ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ R .<_ ( P .\/ Q ) ) -> ( F ` R ) = ( G ` R ) )
24		simpl1	|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ P =/= Q ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ -. R .<_ ( P .\/ Q ) ) -> ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) )
25		simpl21	|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ P =/= Q ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ -. R .<_ ( P .\/ Q ) ) -> ( P e. A /\ -. P .<_ W ) )
26		simpl22	|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ P =/= Q ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ -. R .<_ ( P .\/ Q ) ) -> ( Q e. A /\ -. Q .<_ W ) )
27		simpl23	|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ P =/= Q ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ -. R .<_ ( P .\/ Q ) ) -> P =/= Q )
28		simpr	|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ P =/= Q ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ -. R .<_ ( P .\/ Q ) ) -> -. R .<_ ( P .\/ Q ) )
29	27 28	jca	|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ P =/= Q ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ -. R .<_ ( P .\/ Q ) ) -> ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) )
30		simpl3	|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ P =/= Q ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ -. R .<_ ( P .\/ Q ) ) -> ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) )
31	1 2 3 4 5	cdlemd2	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( F ` R ) = ( G ` R ) )
32	24 25 26 29 30 31	syl131anc	|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ P =/= Q ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ -. R .<_ ( P .\/ Q ) ) -> ( F ` R ) = ( G ` R ) )
33	23 32	pm2.61dan	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ P =/= Q ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( F ` R ) = ( G ` R ) )