Theorem cdlemg36

Description: Use cdlemg35 to eliminate v from cdlemg34 . TODO: Fix comment. (Contributed by NM, 31-May-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cdlemg35.l	|- .<_ = ( le ` K )
2		cdlemg35.j	|- .\/ = ( join ` K )
3		cdlemg35.m	|- ./\ = ( meet ` K )
4		cdlemg35.a	|- A = ( Atoms ` K )
5		cdlemg35.h	|- H = ( LHyp ` K )
6		cdlemg35.t	|- T = ( ( LTrn ` K ) ` W )
7		cdlemg35.r	|- R = ( ( trL ` K ) ` W )
8		simp11	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) /\ ( R ` F ) =/= ( R ` G ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> ( K e. HL /\ W e. H ) )
9		simp12	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) /\ ( R ` F ) =/= ( R ` G ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> ( P e. A /\ -. P .<_ W ) )
10		simp21	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) /\ ( R ` F ) =/= ( R ` G ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> F e. T )
11		simp22	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) /\ ( R ` F ) =/= ( R ` G ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> G e. T )
12		simp31l	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) /\ ( R ` F ) =/= ( R ` G ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> ( F ` P ) =/= P )
13		simp31r	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) /\ ( R ` F ) =/= ( R ` G ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> ( G ` P ) =/= P )
14		simp32	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) /\ ( R ` F ) =/= ( R ` G ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> ( R ` F ) =/= ( R ` G ) )
15	1 2 3 4 5 6 7	cdlemg35	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) -> E. v e. A ( v .<_ W /\ ( v =/= ( R ` F ) /\ v =/= ( R ` G ) ) ) )
16	8 9 10 11 12 13 14 15	syl133anc	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) /\ ( R ` F ) =/= ( R ` G ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> E. v e. A ( v .<_ W /\ ( v =/= ( R ` F ) /\ v =/= ( R ` G ) ) ) )
17		simp11	|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) /\ ( R ` F ) =/= ( R ` G ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ v e. A /\ ( v .<_ W /\ ( v =/= ( R ` F ) /\ v =/= ( R ` G ) ) ) ) -> ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) )
18		simp2	|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) /\ ( R ` F ) =/= ( R ` G ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ v e. A /\ ( v .<_ W /\ ( v =/= ( R ` F ) /\ v =/= ( R ` G ) ) ) ) -> v e. A )
19		simp3l	|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) /\ ( R ` F ) =/= ( R ` G ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ v e. A /\ ( v .<_ W /\ ( v =/= ( R ` F ) /\ v =/= ( R ` G ) ) ) ) -> v .<_ W )
20	18 19	jca	|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) /\ ( R ` F ) =/= ( R ` G ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ v e. A /\ ( v .<_ W /\ ( v =/= ( R ` F ) /\ v =/= ( R ` G ) ) ) ) -> ( v e. A /\ v .<_ W ) )
21		simp121	|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) /\ ( R ` F ) =/= ( R ` G ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ v e. A /\ ( v .<_ W /\ ( v =/= ( R ` F ) /\ v =/= ( R ` G ) ) ) ) -> F e. T )
22		simp122	|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) /\ ( R ` F ) =/= ( R ` G ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ v e. A /\ ( v .<_ W /\ ( v =/= ( R ` F ) /\ v =/= ( R ` G ) ) ) ) -> G e. T )
23	21 22	jca	|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) /\ ( R ` F ) =/= ( R ` G ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ v e. A /\ ( v .<_ W /\ ( v =/= ( R ` F ) /\ v =/= ( R ` G ) ) ) ) -> ( F e. T /\ G e. T ) )
24		simp123	|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) /\ ( R ` F ) =/= ( R ` G ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ v e. A /\ ( v .<_ W /\ ( v =/= ( R ` F ) /\ v =/= ( R ` G ) ) ) ) -> P =/= Q )
25		simp3rl	|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) /\ ( R ` F ) =/= ( R ` G ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ v e. A /\ ( v .<_ W /\ ( v =/= ( R ` F ) /\ v =/= ( R ` G ) ) ) ) -> v =/= ( R ` F ) )
26		simp3rr	|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) /\ ( R ` F ) =/= ( R ` G ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ v e. A /\ ( v .<_ W /\ ( v =/= ( R ` F ) /\ v =/= ( R ` G ) ) ) ) -> v =/= ( R ` G ) )
27		simp133	|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) /\ ( R ` F ) =/= ( R ` G ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ v e. A /\ ( v .<_ W /\ ( v =/= ( R ` F ) /\ v =/= ( R ` G ) ) ) ) -> E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) )
28		eqid	|- ( ( P .\/ v ) ./\ ( Q .\/ ( R ` F ) ) ) = ( ( P .\/ v ) ./\ ( Q .\/ ( R ` F ) ) )
29		eqid	|- ( ( P .\/ v ) ./\ ( Q .\/ ( R ` G ) ) ) = ( ( P .\/ v ) ./\ ( Q .\/ ( R ` G ) ) )
30	1 2 3 4 5 6 7 28 29	cdlemg34	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ ( F e. T /\ G e. T ) /\ P =/= Q ) /\ ( v =/= ( R ` F ) /\ v =/= ( R ` G ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> ( ( P .\/ ( F ` ( G ` P ) ) ) ./\ W ) = ( ( Q .\/ ( F ` ( G ` Q ) ) ) ./\ W ) )
31	17 20 23 24 25 26 27 30	syl133anc	|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) /\ ( R ` F ) =/= ( R ` G ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ v e. A /\ ( v .<_ W /\ ( v =/= ( R ` F ) /\ v =/= ( R ` G ) ) ) ) -> ( ( P .\/ ( F ` ( G ` P ) ) ) ./\ W ) = ( ( Q .\/ ( F ` ( G ` Q ) ) ) ./\ W ) )
32	31	rexlimdv3a	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) /\ ( R ` F ) =/= ( R ` G ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> ( E. v e. A ( v .<_ W /\ ( v =/= ( R ` F ) /\ v =/= ( R ` G ) ) ) -> ( ( P .\/ ( F ` ( G ` P ) ) ) ./\ W ) = ( ( Q .\/ ( F ` ( G ` Q ) ) ) ./\ W ) ) )
33	16 32	mpd	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) /\ ( R ` F ) =/= ( R ` G ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> ( ( P .\/ ( F ` ( G ` P ) ) ) ./\ W ) = ( ( Q .\/ ( F ` ( G ` Q ) ) ) ./\ W ) )