Step |
Hyp |
Ref |
Expression |
1 |
|
cdlemg6.l |
|- .<_ = ( le ` K ) |
2 |
|
cdlemg6.a |
|- A = ( Atoms ` K ) |
3 |
|
cdlemg6.h |
|- H = ( LHyp ` K ) |
4 |
|
cdlemg6.t |
|- T = ( ( LTrn ` K ) ` W ) |
5 |
|
simpl1 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ ( F ` ( G ` P ) ) = P ) ) /\ Q .<_ ( P ( join ` K ) ( ( ( trL ` K ) ` W ) ` G ) ) ) -> ( K e. HL /\ W e. H ) ) |
6 |
|
simpl2l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ ( F ` ( G ` P ) ) = P ) ) /\ Q .<_ ( P ( join ` K ) ( ( ( trL ` K ) ` W ) ` G ) ) ) -> ( P e. A /\ -. P .<_ W ) ) |
7 |
|
simpl2r |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ ( F ` ( G ` P ) ) = P ) ) /\ Q .<_ ( P ( join ` K ) ( ( ( trL ` K ) ` W ) ` G ) ) ) -> ( Q e. A /\ -. Q .<_ W ) ) |
8 |
|
simpl31 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ ( F ` ( G ` P ) ) = P ) ) /\ Q .<_ ( P ( join ` K ) ( ( ( trL ` K ) ` W ) ` G ) ) ) -> F e. T ) |
9 |
|
simpl32 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ ( F ` ( G ` P ) ) = P ) ) /\ Q .<_ ( P ( join ` K ) ( ( ( trL ` K ) ` W ) ` G ) ) ) -> G e. T ) |
10 |
|
simpr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ ( F ` ( G ` P ) ) = P ) ) /\ Q .<_ ( P ( join ` K ) ( ( ( trL ` K ) ` W ) ` G ) ) ) -> Q .<_ ( P ( join ` K ) ( ( ( trL ` K ) ` W ) ` G ) ) ) |
11 |
|
simpl33 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ ( F ` ( G ` P ) ) = P ) ) /\ Q .<_ ( P ( join ` K ) ( ( ( trL ` K ) ` W ) ` G ) ) ) -> ( F ` ( G ` P ) ) = P ) |
12 |
|
eqid |
|- ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W ) |
13 |
|
eqid |
|- ( join ` K ) = ( join ` K ) |
14 |
|
eqid |
|- ( ( ( trL ` K ) ` W ) ` G ) = ( ( ( trL ` K ) ` W ) ` G ) |
15 |
1 2 3 4 12 13 14
|
cdlemg6e |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ F e. T ) /\ ( G e. T /\ Q .<_ ( P ( join ` K ) ( ( ( trL ` K ) ` W ) ` G ) ) /\ ( F ` ( G ` P ) ) = P ) ) -> ( F ` ( G ` Q ) ) = Q ) |
16 |
5 6 7 8 9 10 11 15
|
syl133anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ ( F ` ( G ` P ) ) = P ) ) /\ Q .<_ ( P ( join ` K ) ( ( ( trL ` K ) ` W ) ` G ) ) ) -> ( F ` ( G ` Q ) ) = Q ) |
17 |
|
simpl1 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ ( F ` ( G ` P ) ) = P ) ) /\ -. Q .<_ ( P ( join ` K ) ( ( ( trL ` K ) ` W ) ` G ) ) ) -> ( K e. HL /\ W e. H ) ) |
18 |
|
simpl2l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ ( F ` ( G ` P ) ) = P ) ) /\ -. Q .<_ ( P ( join ` K ) ( ( ( trL ` K ) ` W ) ` G ) ) ) -> ( P e. A /\ -. P .<_ W ) ) |
19 |
|
simpl2r |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ ( F ` ( G ` P ) ) = P ) ) /\ -. Q .<_ ( P ( join ` K ) ( ( ( trL ` K ) ` W ) ` G ) ) ) -> ( Q e. A /\ -. Q .<_ W ) ) |
20 |
|
simpl31 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ ( F ` ( G ` P ) ) = P ) ) /\ -. Q .<_ ( P ( join ` K ) ( ( ( trL ` K ) ` W ) ` G ) ) ) -> F e. T ) |
21 |
|
simpl32 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ ( F ` ( G ` P ) ) = P ) ) /\ -. Q .<_ ( P ( join ` K ) ( ( ( trL ` K ) ` W ) ` G ) ) ) -> G e. T ) |
22 |
|
simpr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ ( F ` ( G ` P ) ) = P ) ) /\ -. Q .<_ ( P ( join ` K ) ( ( ( trL ` K ) ` W ) ` G ) ) ) -> -. Q .<_ ( P ( join ` K ) ( ( ( trL ` K ) ` W ) ` G ) ) ) |
23 |
|
simpl33 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ ( F ` ( G ` P ) ) = P ) ) /\ -. Q .<_ ( P ( join ` K ) ( ( ( trL ` K ) ` W ) ` G ) ) ) -> ( F ` ( G ` P ) ) = P ) |
24 |
1 2 3 4 12 13 14
|
cdlemg4 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ F e. T ) /\ ( G e. T /\ -. Q .<_ ( P ( join ` K ) ( ( ( trL ` K ) ` W ) ` G ) ) /\ ( F ` ( G ` P ) ) = P ) ) -> ( F ` ( G ` Q ) ) = Q ) |
25 |
17 18 19 20 21 22 23 24
|
syl133anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ ( F ` ( G ` P ) ) = P ) ) /\ -. Q .<_ ( P ( join ` K ) ( ( ( trL ` K ) ` W ) ` G ) ) ) -> ( F ` ( G ` Q ) ) = Q ) |
26 |
16 25
|
pm2.61dan |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ ( F ` ( G ` P ) ) = P ) ) -> ( F ` ( G ` Q ) ) = Q ) |