Metamath Proof Explorer

Theorem cdlemefrs29bpre0

Description: TODO fix comment. (Contributed by NM, 29-Mar-2013)

Ref Expression
Hypotheses cdlemefrs27.b 
|- B = ( Base ` K )
cdlemefrs27.l 
|- .<_ = ( le ` K )
cdlemefrs27.j 
|- .\/ = ( join ` K )
cdlemefrs27.m 
|- ./\ = ( meet ` K )
cdlemefrs27.a 
|- A = ( Atoms ` K )
cdlemefrs27.h 
|- H = ( LHyp ` K )
cdlemefrs27.eq 
|- ( s = R -> ( ph <-> ps ) )
cdlemefrs27.nb 
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q /\ ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) -> N e. B )
Assertion cdlemefrs29bpre0 
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> ( A. s e. A ( ( ( -. s .<_ W /\ ph ) /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) <-> z = [_ R / s ]_ N ) )

Proof

Step Hyp Ref Expression
1 cdlemefrs27.b 
 |-  B = ( Base ` K )
2 cdlemefrs27.l 
 |-  .<_ = ( le ` K )
3 cdlemefrs27.j 
 |-  .\/ = ( join ` K )
4 cdlemefrs27.m 
 |-  ./\ = ( meet ` K )
5 cdlemefrs27.a 
 |-  A = ( Atoms ` K )
6 cdlemefrs27.h 
 |-  H = ( LHyp ` K )
7 cdlemefrs27.eq 
 |-  ( s = R -> ( ph <-> ps ) )
8 cdlemefrs27.nb 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q /\ ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) -> N e. B )
9 df-ral 
 |-  ( A. s e. A ( ( ( -. s .<_ W /\ ph ) /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) <-> A. s ( s e. A -> ( ( ( -. s .<_ W /\ ph ) /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) ) )
10 anass 
 |-  ( ( ( s e. A /\ ( -. s .<_ W /\ ph ) ) /\ ( s .\/ ( R ./\ W ) ) = R ) <-> ( s e. A /\ ( ( -. s .<_ W /\ ph ) /\ ( s .\/ ( R ./\ W ) ) = R ) ) )
11 10 imbi1i 
 |-  ( ( ( ( s e. A /\ ( -. s .<_ W /\ ph ) ) /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) <-> ( ( s e. A /\ ( ( -. s .<_ W /\ ph ) /\ ( s .\/ ( R ./\ W ) ) = R ) ) -> z = ( N .\/ ( R ./\ W ) ) ) )
12 impexp 
 |-  ( ( ( ( s e. A /\ ( -. s .<_ W /\ ph ) ) /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) <-> ( ( s e. A /\ ( -. s .<_ W /\ ph ) ) -> ( ( s .\/ ( R ./\ W ) ) = R -> z = ( N .\/ ( R ./\ W ) ) ) ) )
13 impexp 
 |-  ( ( ( s e. A /\ ( ( -. s .<_ W /\ ph ) /\ ( s .\/ ( R ./\ W ) ) = R ) ) -> z = ( N .\/ ( R ./\ W ) ) ) <-> ( s e. A -> ( ( ( -. s .<_ W /\ ph ) /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) ) )
14 11 12 13 3bitr3ri 
 |-  ( ( s e. A -> ( ( ( -. s .<_ W /\ ph ) /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) ) <-> ( ( s e. A /\ ( -. s .<_ W /\ ph ) ) -> ( ( s .\/ ( R ./\ W ) ) = R -> z = ( N .\/ ( R ./\ W ) ) ) ) )
15 simpl11 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) /\ ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) -> ( K e. HL /\ W e. H ) )
16 simpl2r 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) /\ ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) -> ( R e. A /\ -. R .<_ W ) )
17 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
18 2 4 17 5 6 lhpmat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( R ./\ W ) = ( 0. ` K ) )
19 15 16 18 syl2anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) /\ ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) -> ( R ./\ W ) = ( 0. ` K ) )
20 19 oveq2d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) /\ ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) -> ( s .\/ ( R ./\ W ) ) = ( s .\/ ( 0. ` K ) ) )
21 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> K e. HL )
22 hlol 
 |-  ( K e. HL -> K e. OL )
23 21 22 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> K e. OL )
24 23 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) /\ ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) -> K e. OL )
25 simprl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) /\ ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) -> s e. A )
26 1 5 atbase 
 |-  ( s e. A -> s e. B )
27 25 26 syl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) /\ ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) -> s e. B )
28 1 3 17 olj01 
 |-  ( ( K e. OL /\ s e. B ) -> ( s .\/ ( 0. ` K ) ) = s )
29 24 27 28 syl2anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) /\ ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) -> ( s .\/ ( 0. ` K ) ) = s )
30 20 29 eqtrd 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) /\ ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) -> ( s .\/ ( R ./\ W ) ) = s )
31 30 eqeq1d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) /\ ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) -> ( ( s .\/ ( R ./\ W ) ) = R <-> s = R ) )
32 19 oveq2d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) /\ ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) -> ( N .\/ ( R ./\ W ) ) = ( N .\/ ( 0. ` K ) ) )
33 simpl1 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) /\ ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) -> ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) )
34 simpl2l 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) /\ ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) -> P =/= Q )
35 simprr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) /\ ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) -> ( -. s .<_ W /\ ph ) )
36 33 34 25 35 8 syl112anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) /\ ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) -> N e. B )
37 1 3 17 olj01 
 |-  ( ( K e. OL /\ N e. B ) -> ( N .\/ ( 0. ` K ) ) = N )
38 24 36 37 syl2anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) /\ ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) -> ( N .\/ ( 0. ` K ) ) = N )
39 32 38 eqtrd 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) /\ ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) -> ( N .\/ ( R ./\ W ) ) = N )
40 39 eqeq2d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) /\ ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) -> ( z = ( N .\/ ( R ./\ W ) ) <-> z = N ) )
41 31 40 imbi12d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) /\ ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) -> ( ( ( s .\/ ( R ./\ W ) ) = R -> z = ( N .\/ ( R ./\ W ) ) ) <-> ( s = R -> z = N ) ) )
42 41 pm5.74da 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> ( ( ( s e. A /\ ( -. s .<_ W /\ ph ) ) -> ( ( s .\/ ( R ./\ W ) ) = R -> z = ( N .\/ ( R ./\ W ) ) ) ) <-> ( ( s e. A /\ ( -. s .<_ W /\ ph ) ) -> ( s = R -> z = N ) ) ) )
43 impexp 
 |-  ( ( ( ( s e. A /\ ( -. s .<_ W /\ ph ) ) /\ s = R ) -> z = N ) <-> ( ( s e. A /\ ( -. s .<_ W /\ ph ) ) -> ( s = R -> z = N ) ) )
44 simp2rl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> R e. A )
45 simp2rr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> -. R .<_ W )
46 simp3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> ps )
47 eleq1 
 |-  ( s = R -> ( s e. A <-> R e. A ) )
48 breq1 
 |-  ( s = R -> ( s .<_ W <-> R .<_ W ) )
49 48 notbid 
 |-  ( s = R -> ( -. s .<_ W <-> -. R .<_ W ) )
50 49 7 anbi12d 
 |-  ( s = R -> ( ( -. s .<_ W /\ ph ) <-> ( -. R .<_ W /\ ps ) ) )
51 47 50 anbi12d 
 |-  ( s = R -> ( ( s e. A /\ ( -. s .<_ W /\ ph ) ) <-> ( R e. A /\ ( -. R .<_ W /\ ps ) ) ) )
52 51 biimprcd 
 |-  ( ( R e. A /\ ( -. R .<_ W /\ ps ) ) -> ( s = R -> ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) )
53 44 45 46 52 syl12anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> ( s = R -> ( s e. A /\ ( -. s .<_ W /\ ph ) ) ) )
54 53 pm4.71rd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> ( s = R <-> ( ( s e. A /\ ( -. s .<_ W /\ ph ) ) /\ s = R ) ) )
55 54 imbi1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> ( ( s = R -> z = N ) <-> ( ( ( s e. A /\ ( -. s .<_ W /\ ph ) ) /\ s = R ) -> z = N ) ) )
56 eqcom 
 |-  ( z = N <-> N = z )
57 56 imbi2i 
 |-  ( ( s = R -> z = N ) <-> ( s = R -> N = z ) )
58 55 57 bitr3di 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> ( ( ( ( s e. A /\ ( -. s .<_ W /\ ph ) ) /\ s = R ) -> z = N ) <-> ( s = R -> N = z ) ) )
59 43 58 bitr3id 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> ( ( ( s e. A /\ ( -. s .<_ W /\ ph ) ) -> ( s = R -> z = N ) ) <-> ( s = R -> N = z ) ) )
60 42 59 bitrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> ( ( ( s e. A /\ ( -. s .<_ W /\ ph ) ) -> ( ( s .\/ ( R ./\ W ) ) = R -> z = ( N .\/ ( R ./\ W ) ) ) ) <-> ( s = R -> N = z ) ) )
61 14 60 bitrid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> ( ( s e. A -> ( ( ( -. s .<_ W /\ ph ) /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) ) <-> ( s = R -> N = z ) ) )
62 61 albidv 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> ( A. s ( s e. A -> ( ( ( -. s .<_ W /\ ph ) /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) ) <-> A. s ( s = R -> N = z ) ) )
63 9 62 bitrid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> ( A. s e. A ( ( ( -. s .<_ W /\ ph ) /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) <-> A. s ( s = R -> N = z ) ) )
64 nfcv 
 |-  F/_ s z
65 64 csbiebg 
 |-  ( R e. A -> ( A. s ( s = R -> N = z ) <-> [_ R / s ]_ N = z ) )
66 44 65 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> ( A. s ( s = R -> N = z ) <-> [_ R / s ]_ N = z ) )
67 eqcom 
 |-  ( [_ R / s ]_ N = z <-> z = [_ R / s ]_ N )
68 66 67 bitrdi 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> ( A. s ( s = R -> N = z ) <-> z = [_ R / s ]_ N ) )
69 63 68 bitrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> ( A. s e. A ( ( ( -. s .<_ W /\ ph ) /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) <-> z = [_ R / s ]_ N ) )