Step |
Hyp |
Ref |
Expression |
1 |
|
cdleme41.b |
|- B = ( Base ` K ) |
2 |
|
cdleme41.l |
|- .<_ = ( le ` K ) |
3 |
|
cdleme41.j |
|- .\/ = ( join ` K ) |
4 |
|
cdleme41.m |
|- ./\ = ( meet ` K ) |
5 |
|
cdleme41.a |
|- A = ( Atoms ` K ) |
6 |
|
cdleme41.h |
|- H = ( LHyp ` K ) |
7 |
|
cdleme41.u |
|- U = ( ( P .\/ Q ) ./\ W ) |
8 |
|
cdleme41.d |
|- D = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) ) |
9 |
|
cdleme41.e |
|- E = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) ) |
10 |
|
cdleme41.g |
|- G = ( ( P .\/ Q ) ./\ ( E .\/ ( ( s .\/ t ) ./\ W ) ) ) |
11 |
|
cdleme41.i |
|- I = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = G ) ) |
12 |
|
cdleme41.n |
|- N = if ( s .<_ ( P .\/ Q ) , I , D ) |
13 |
|
cdleme41.o |
|- O = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( x ./\ W ) ) = x ) -> z = ( N .\/ ( x ./\ W ) ) ) ) |
14 |
|
cdleme41.f |
|- F = ( x e. B |-> if ( ( P =/= Q /\ -. x .<_ W ) , O , x ) ) |
15 |
1
|
fvexi |
|- B e. _V |
16 |
|
nfv |
|- F/ s ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( X e. B /\ ( P =/= Q /\ -. X .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( R .\/ ( X ./\ W ) ) = X ) ) |
17 |
|
nfcsb1v |
|- F/_ s [_ R / s ]_ N |
18 |
|
nfcv |
|- F/_ s .\/ |
19 |
|
nfcv |
|- F/_ s ( X ./\ W ) |
20 |
17 18 19
|
nfov |
|- F/_ s ( [_ R / s ]_ N .\/ ( X ./\ W ) ) |
21 |
20
|
a1i |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( X e. B /\ ( P =/= Q /\ -. X .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( R .\/ ( X ./\ W ) ) = X ) ) -> F/_ s ( [_ R / s ]_ N .\/ ( X ./\ W ) ) ) |
22 |
|
nfvd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( X e. B /\ ( P =/= Q /\ -. X .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( R .\/ ( X ./\ W ) ) = X ) ) -> F/ s ( -. R .<_ W /\ ( R .\/ ( X ./\ W ) ) = X ) ) |
23 |
|
eqid |
|- ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) -> z = ( N .\/ ( X ./\ W ) ) ) ) = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) -> z = ( N .\/ ( X ./\ W ) ) ) ) |
24 |
13 14 23
|
cdleme31fv1 |
|- ( ( X e. B /\ ( P =/= Q /\ -. X .<_ W ) ) -> ( F ` X ) = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) -> z = ( N .\/ ( X ./\ W ) ) ) ) ) |
25 |
24
|
3ad2ant2 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( X e. B /\ ( P =/= Q /\ -. X .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( R .\/ ( X ./\ W ) ) = X ) ) -> ( F ` X ) = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) -> z = ( N .\/ ( X ./\ W ) ) ) ) ) |
26 |
|
breq1 |
|- ( s = R -> ( s .<_ W <-> R .<_ W ) ) |
27 |
26
|
notbid |
|- ( s = R -> ( -. s .<_ W <-> -. R .<_ W ) ) |
28 |
|
oveq1 |
|- ( s = R -> ( s .\/ ( X ./\ W ) ) = ( R .\/ ( X ./\ W ) ) ) |
29 |
28
|
eqeq1d |
|- ( s = R -> ( ( s .\/ ( X ./\ W ) ) = X <-> ( R .\/ ( X ./\ W ) ) = X ) ) |
30 |
27 29
|
anbi12d |
|- ( s = R -> ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) <-> ( -. R .<_ W /\ ( R .\/ ( X ./\ W ) ) = X ) ) ) |
31 |
30
|
adantl |
|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( X e. B /\ ( P =/= Q /\ -. X .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( R .\/ ( X ./\ W ) ) = X ) ) /\ s = R ) -> ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) <-> ( -. R .<_ W /\ ( R .\/ ( X ./\ W ) ) = X ) ) ) |
32 |
|
csbeq1a |
|- ( s = R -> N = [_ R / s ]_ N ) |
33 |
32
|
oveq1d |
|- ( s = R -> ( N .\/ ( X ./\ W ) ) = ( [_ R / s ]_ N .\/ ( X ./\ W ) ) ) |
34 |
33
|
adantl |
|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( X e. B /\ ( P =/= Q /\ -. X .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( R .\/ ( X ./\ W ) ) = X ) ) /\ s = R ) -> ( N .\/ ( X ./\ W ) ) = ( [_ R / s ]_ N .\/ ( X ./\ W ) ) ) |
35 |
|
simp1 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( X e. B /\ ( P =/= Q /\ -. X .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( R .\/ ( X ./\ W ) ) = X ) ) -> ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) ) |
36 |
|
simp2l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( X e. B /\ ( P =/= Q /\ -. X .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( R .\/ ( X ./\ W ) ) = X ) ) -> X e. B ) |
37 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14
|
cdleme32fvcl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ X e. B ) -> ( F ` X ) e. B ) |
38 |
35 36 37
|
syl2anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( X e. B /\ ( P =/= Q /\ -. X .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( R .\/ ( X ./\ W ) ) = X ) ) -> ( F ` X ) e. B ) |
39 |
|
simp3ll |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( X e. B /\ ( P =/= Q /\ -. X .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( R .\/ ( X ./\ W ) ) = X ) ) -> R e. A ) |
40 |
|
simp3lr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( X e. B /\ ( P =/= Q /\ -. X .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( R .\/ ( X ./\ W ) ) = X ) ) -> -. R .<_ W ) |
41 |
|
simp3r |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( X e. B /\ ( P =/= Q /\ -. X .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( R .\/ ( X ./\ W ) ) = X ) ) -> ( R .\/ ( X ./\ W ) ) = X ) |
42 |
40 41
|
jca |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( X e. B /\ ( P =/= Q /\ -. X .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( R .\/ ( X ./\ W ) ) = X ) ) -> ( -. R .<_ W /\ ( R .\/ ( X ./\ W ) ) = X ) ) |
43 |
16 21 22 25 31 34 38 39 42
|
riotasv2d |
|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( X e. B /\ ( P =/= Q /\ -. X .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( R .\/ ( X ./\ W ) ) = X ) ) /\ B e. _V ) -> ( F ` X ) = ( [_ R / s ]_ N .\/ ( X ./\ W ) ) ) |
44 |
15 43
|
mpan2 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( X e. B /\ ( P =/= Q /\ -. X .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( R .\/ ( X ./\ W ) ) = X ) ) -> ( F ` X ) = ( [_ R / s ]_ N .\/ ( X ./\ W ) ) ) |