Metamath Proof Explorer


Theorem cdlemg4g

Description: TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013)

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

Proof

Step Hyp Ref Expression
1 cdlemg4.l
 |-  .<_ = ( le ` K )
2 cdlemg4.a
 |-  A = ( Atoms ` K )
3 cdlemg4.h
 |-  H = ( LHyp ` K )
4 cdlemg4.t
 |-  T = ( ( LTrn ` K ) ` W )
5 cdlemg4.r
 |-  R = ( ( trL ` K ) ` W )
6 cdlemg4.j
 |-  .\/ = ( join ` K )
7 cdlemg4b.v
 |-  V = ( R ` G )
8 cdlemg4.m
 |-  ./\ = ( meet ` K )
9 1 2 3 4 5 6 7 8 cdlemg4f
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ F e. T ) /\ ( G e. T /\ -. Q .<_ ( P .\/ V ) /\ ( F ` ( G ` P ) ) = P ) ) -> ( F ` ( G ` Q ) ) = ( ( Q .\/ V ) ./\ ( P .\/ ( ( P .\/ Q ) ./\ W ) ) ) )
10 simp1l
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ F e. T ) /\ ( G e. T /\ -. Q .<_ ( P .\/ V ) /\ ( F ` ( G ` P ) ) = P ) ) -> K e. HL )
11 simp1r
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ F e. T ) /\ ( G e. T /\ -. Q .<_ ( P .\/ V ) /\ ( F ` ( G ` P ) ) = P ) ) -> W e. H )
12 simp21
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ F e. T ) /\ ( G e. T /\ -. Q .<_ ( P .\/ V ) /\ ( F ` ( G ` P ) ) = P ) ) -> ( P e. A /\ -. P .<_ W ) )
13 simp22l
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ F e. T ) /\ ( G e. T /\ -. Q .<_ ( P .\/ V ) /\ ( F ` ( G ` P ) ) = P ) ) -> Q e. A )
14 eqid
 |-  ( ( P .\/ Q ) ./\ W ) = ( ( P .\/ Q ) ./\ W )
15 1 6 8 2 3 14 cdleme0cp
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A ) ) -> ( P .\/ ( ( P .\/ Q ) ./\ W ) ) = ( P .\/ Q ) )
16 10 11 12 13 15 syl22anc
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ F e. T ) /\ ( G e. T /\ -. Q .<_ ( P .\/ V ) /\ ( F ` ( G ` P ) ) = P ) ) -> ( P .\/ ( ( P .\/ Q ) ./\ W ) ) = ( P .\/ Q ) )
17 16 oveq2d
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ F e. T ) /\ ( G e. T /\ -. Q .<_ ( P .\/ V ) /\ ( F ` ( G ` P ) ) = P ) ) -> ( ( Q .\/ V ) ./\ ( P .\/ ( ( P .\/ Q ) ./\ W ) ) ) = ( ( Q .\/ V ) ./\ ( P .\/ Q ) ) )
18 9 17 eqtrd
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ F e. T ) /\ ( G e. T /\ -. Q .<_ ( P .\/ V ) /\ ( F ` ( G ` P ) ) = P ) ) -> ( F ` ( G ` Q ) ) = ( ( Q .\/ V ) ./\ ( P .\/ Q ) ) )