Step |
Hyp |
Ref |
Expression |
1 |
|
cdlemk5.b |
|- B = ( Base ` K ) |
2 |
|
cdlemk5.l |
|- .<_ = ( le ` K ) |
3 |
|
cdlemk5.j |
|- .\/ = ( join ` K ) |
4 |
|
cdlemk5.m |
|- ./\ = ( meet ` K ) |
5 |
|
cdlemk5.a |
|- A = ( Atoms ` K ) |
6 |
|
cdlemk5.h |
|- H = ( LHyp ` K ) |
7 |
|
cdlemk5.t |
|- T = ( ( LTrn ` K ) ` W ) |
8 |
|
cdlemk5.r |
|- R = ( ( trL ` K ) ` W ) |
9 |
|
cdlemk5.z |
|- Z = ( ( P .\/ ( R ` b ) ) ./\ ( ( N ` P ) .\/ ( R ` ( b o. `' F ) ) ) ) |
10 |
|
cdlemk5.y |
|- Y = ( ( P .\/ ( R ` g ) ) ./\ ( Z .\/ ( R ` ( g o. `' b ) ) ) ) |
11 |
|
cdlemk5.x |
|- X = ( iota_ z e. T A. b e. T ( ( b =/= ( _I |` B ) /\ ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` g ) ) -> ( z ` P ) = Y ) ) |
12 |
|
simp11l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> K e. HL ) |
13 |
|
simp11 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( K e. HL /\ W e. H ) ) |
14 |
|
simp12 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( F e. T /\ F =/= ( _I |` B ) ) ) |
15 |
|
simp13 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( G e. T /\ G =/= ( _I |` B ) ) ) |
16 |
|
simp21 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> N e. T ) |
17 |
|
simp22 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( P e. A /\ -. P .<_ W ) ) |
18 |
|
simp23 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( R ` F ) = ( R ` N ) ) |
19 |
1 2 3 4 5 6 7 8 9 10 11
|
cdlemk35s |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) /\ N e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) ) -> [_ G / g ]_ X e. T ) |
20 |
13 14 15 16 17 18 19
|
syl132anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> [_ G / g ]_ X e. T ) |
21 |
2 5 6 7
|
ltrnel |
|- ( ( ( K e. HL /\ W e. H ) /\ [_ G / g ]_ X e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( [_ G / g ]_ X ` P ) e. A /\ -. ( [_ G / g ]_ X ` P ) .<_ W ) ) |
22 |
13 20 17 21
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( ( [_ G / g ]_ X ` P ) e. A /\ -. ( [_ G / g ]_ X ` P ) .<_ W ) ) |
23 |
22
|
simpld |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( [_ G / g ]_ X ` P ) e. A ) |
24 |
|
simp31 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> I e. T ) |
25 |
|
simp32 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> I =/= ( _I |` B ) ) |
26 |
1 5 6 7 8
|
trlnidat |
|- ( ( ( K e. HL /\ W e. H ) /\ I e. T /\ I =/= ( _I |` B ) ) -> ( R ` I ) e. A ) |
27 |
13 24 25 26
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( R ` I ) e. A ) |
28 |
24 25
|
jca |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( I e. T /\ I =/= ( _I |` B ) ) ) |
29 |
1 2 3 4 5 6 7 8 9 10 11
|
cdlemk35s |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( F e. T /\ F =/= ( _I |` B ) ) /\ ( I e. T /\ I =/= ( _I |` B ) ) /\ N e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) ) -> [_ I / g ]_ X e. T ) |
30 |
13 14 28 16 17 18 29
|
syl132anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> [_ I / g ]_ X e. T ) |
31 |
|
simp22l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> P e. A ) |
32 |
2 5 6 7
|
ltrnat |
|- ( ( ( K e. HL /\ W e. H ) /\ [_ I / g ]_ X e. T /\ P e. A ) -> ( [_ I / g ]_ X ` P ) e. A ) |
33 |
13 30 31 32
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( [_ I / g ]_ X ` P ) e. A ) |
34 |
|
simp13l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> G e. T ) |
35 |
|
simp13r |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> G =/= ( _I |` B ) ) |
36 |
1 5 6 7 8
|
trlnidat |
|- ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ G =/= ( _I |` B ) ) -> ( R ` G ) e. A ) |
37 |
13 34 35 36
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( R ` G ) e. A ) |
38 |
6 7
|
ltrnco |
|- ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ I e. T ) -> ( G o. I ) e. T ) |
39 |
13 34 24 38
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( G o. I ) e. T ) |
40 |
34 24
|
jca |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( G e. T /\ I e. T ) ) |
41 |
|
simp33 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( R ` G ) =/= ( R ` I ) ) |
42 |
1 6 7 8
|
trlconid |
|- ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ I e. T ) /\ ( R ` G ) =/= ( R ` I ) ) -> ( G o. I ) =/= ( _I |` B ) ) |
43 |
13 40 41 42
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( G o. I ) =/= ( _I |` B ) ) |
44 |
39 43
|
jca |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( ( G o. I ) e. T /\ ( G o. I ) =/= ( _I |` B ) ) ) |
45 |
1 2 3 4 5 6 7 8 9 10 11
|
cdlemk35s |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( F e. T /\ F =/= ( _I |` B ) ) /\ ( ( G o. I ) e. T /\ ( G o. I ) =/= ( _I |` B ) ) /\ N e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) ) -> [_ ( G o. I ) / g ]_ X e. T ) |
46 |
13 14 44 16 17 18 45
|
syl132anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> [_ ( G o. I ) / g ]_ X e. T ) |
47 |
2 5 6 7
|
ltrnat |
|- ( ( ( K e. HL /\ W e. H ) /\ [_ ( G o. I ) / g ]_ X e. T /\ P e. A ) -> ( [_ ( G o. I ) / g ]_ X ` P ) e. A ) |
48 |
13 46 31 47
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( [_ ( G o. I ) / g ]_ X ` P ) e. A ) |
49 |
24 25 43
|
3jca |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( I e. T /\ I =/= ( _I |` B ) /\ ( G o. I ) =/= ( _I |` B ) ) ) |
50 |
1 2 3 4 5 6 7 8 9 10 11
|
cdlemk46 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( G o. I ) =/= ( _I |` B ) ) ) -> ( [_ ( G o. I ) / g ]_ X ` P ) .<_ ( ( [_ G / g ]_ X ` P ) .\/ ( R ` I ) ) ) |
51 |
49 50
|
syld3an3 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( [_ ( G o. I ) / g ]_ X ` P ) .<_ ( ( [_ G / g ]_ X ` P ) .\/ ( R ` I ) ) ) |
52 |
1 2 3 4 5 6 7 8 9 10 11
|
cdlemk45 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( G o. I ) =/= ( _I |` B ) ) ) -> ( [_ ( G o. I ) / g ]_ X ` P ) .<_ ( ( [_ I / g ]_ X ` P ) .\/ ( R ` G ) ) ) |
53 |
49 52
|
syld3an3 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( [_ ( G o. I ) / g ]_ X ` P ) .<_ ( ( [_ I / g ]_ X ` P ) .\/ ( R ` G ) ) ) |
54 |
2 6 7 8
|
trlle |
|- ( ( ( K e. HL /\ W e. H ) /\ I e. T ) -> ( R ` I ) .<_ W ) |
55 |
13 24 54
|
syl2anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( R ` I ) .<_ W ) |
56 |
27 55
|
jca |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( ( R ` I ) e. A /\ ( R ` I ) .<_ W ) ) |
57 |
2 6 7 8
|
trlle |
|- ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> ( R ` G ) .<_ W ) |
58 |
13 34 57
|
syl2anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( R ` G ) .<_ W ) |
59 |
37 58
|
jca |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( ( R ` G ) e. A /\ ( R ` G ) .<_ W ) ) |
60 |
41
|
necomd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( R ` I ) =/= ( R ` G ) ) |
61 |
2 3 5 6
|
lhp2atne |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( ( [_ G / g ]_ X ` P ) e. A /\ -. ( [_ G / g ]_ X ` P ) .<_ W ) /\ ( [_ I / g ]_ X ` P ) e. A ) /\ ( ( ( R ` I ) e. A /\ ( R ` I ) .<_ W ) /\ ( ( R ` G ) e. A /\ ( R ` G ) .<_ W ) ) /\ ( R ` I ) =/= ( R ` G ) ) -> ( ( [_ G / g ]_ X ` P ) .\/ ( R ` I ) ) =/= ( ( [_ I / g ]_ X ` P ) .\/ ( R ` G ) ) ) |
62 |
13 22 33 56 59 60 61
|
syl321anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( ( [_ G / g ]_ X ` P ) .\/ ( R ` I ) ) =/= ( ( [_ I / g ]_ X ` P ) .\/ ( R ` G ) ) ) |
63 |
2 3 4 5
|
2atm |
|- ( ( ( K e. HL /\ ( [_ G / g ]_ X ` P ) e. A /\ ( R ` I ) e. A ) /\ ( ( [_ I / g ]_ X ` P ) e. A /\ ( R ` G ) e. A /\ ( [_ ( G o. I ) / g ]_ X ` P ) e. A ) /\ ( ( [_ ( G o. I ) / g ]_ X ` P ) .<_ ( ( [_ G / g ]_ X ` P ) .\/ ( R ` I ) ) /\ ( [_ ( G o. I ) / g ]_ X ` P ) .<_ ( ( [_ I / g ]_ X ` P ) .\/ ( R ` G ) ) /\ ( ( [_ G / g ]_ X ` P ) .\/ ( R ` I ) ) =/= ( ( [_ I / g ]_ X ` P ) .\/ ( R ` G ) ) ) ) -> ( [_ ( G o. I ) / g ]_ X ` P ) = ( ( ( [_ G / g ]_ X ` P ) .\/ ( R ` I ) ) ./\ ( ( [_ I / g ]_ X ` P ) .\/ ( R ` G ) ) ) ) |
64 |
12 23 27 33 37 48 51 53 62 63
|
syl333anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( [_ ( G o. I ) / g ]_ X ` P ) = ( ( ( [_ G / g ]_ X ` P ) .\/ ( R ` I ) ) ./\ ( ( [_ I / g ]_ X ` P ) .\/ ( R ` G ) ) ) ) |