Metamath Proof Explorer

Theorem cdlemefrs29cpre1

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 )
cdlemefrs27.rnb 
|- ( ( ( ( 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 / s ]_ N e. B )
Assertion cdlemefrs29cpre1 
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> E! z e. B A. s e. A ( ( ( -. s .<_ W /\ ph ) /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) )

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 cdlemefrs27.rnb 
 |-  ( ( ( ( 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 / s ]_ N e. B )
10 1 2 3 4 5 6 7 8 9 cdlemefrs29bpre1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> E. z e. B A. s e. A ( ( ( -. s .<_ W /\ ph ) /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) )
11 simp11 
 |-  ( ( ( ( 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 /\ W e. H ) )
12 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 )
13 1 5 atbase 
 |-  ( R e. A -> R e. B )
14 12 13 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 ) -> R e. B )
15 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 )
16 1 2 3 4 5 6 lhpmcvr2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( R e. B /\ -. R .<_ W ) ) -> E. s e. A ( -. s .<_ W /\ ( s .\/ ( R ./\ W ) ) = R ) )
17 11 14 15 16 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 ) -> E. s e. A ( -. s .<_ W /\ ( s .\/ ( R ./\ W ) ) = R ) )
18 simpl3 
 |-  ( ( ( ( ( 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 ) -> ps )
19 7 pm5.32ri 
 |-  ( ( ph /\ s = R ) <-> ( ps /\ s = R ) )
20 19 baibr 
 |-  ( ps -> ( s = R <-> ( ph /\ s = R ) ) )
21 18 20 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 = R <-> ( ph /\ s = R ) ) )
22 simp2r 
 |-  ( ( ( ( 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 /\ -. R .<_ W ) )
23 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
24 2 4 23 5 6 lhpmat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( R ./\ W ) = ( 0. ` K ) )
25 11 22 24 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 ) -> ( R ./\ W ) = ( 0. ` K ) )
26 25 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 ) -> ( R ./\ W ) = ( 0. ` K ) )
27 26 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 .\/ ( R ./\ W ) ) = ( s .\/ ( 0. ` K ) ) )
28 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 )
29 hlol 
 |-  ( K e. HL -> K e. OL )
30 28 29 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 )
31 1 5 atbase 
 |-  ( s e. A -> s e. B )
32 1 3 23 olj01 
 |-  ( ( K e. OL /\ s e. B ) -> ( s .\/ ( 0. ` K ) ) = s )
33 30 31 32 syl2an 
 |-  ( ( ( ( ( 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 .\/ ( 0. ` K ) ) = s )
34 27 33 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 .\/ ( R ./\ W ) ) = s )
35 34 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 .\/ ( R ./\ W ) ) = R <-> s = R ) )
36 35 anbi2d 
 |-  ( ( ( ( ( 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 ) -> ( ( ph /\ ( s .\/ ( R ./\ W ) ) = R ) <-> ( ph /\ s = R ) ) )
37 21 35 36 3bitr4d 
 |-  ( ( ( ( ( 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 .\/ ( R ./\ W ) ) = R <-> ( ph /\ ( s .\/ ( R ./\ W ) ) = R ) ) )
38 37 anbi2d 
 |-  ( ( ( ( ( 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 /\ ( s .\/ ( R ./\ W ) ) = R ) <-> ( -. s .<_ W /\ ( ph /\ ( s .\/ ( R ./\ W ) ) = R ) ) ) )
39 anass 
 |-  ( ( ( -. s .<_ W /\ ph ) /\ ( s .\/ ( R ./\ W ) ) = R ) <-> ( -. s .<_ W /\ ( ph /\ ( s .\/ ( R ./\ W ) ) = R ) ) )
40 38 39 bitr4di 
 |-  ( ( ( ( ( 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 /\ ( s .\/ ( R ./\ W ) ) = R ) <-> ( ( -. s .<_ W /\ ph ) /\ ( s .\/ ( R ./\ W ) ) = R ) ) )
41 40 rexbidva 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> ( E. s e. A ( -. s .<_ W /\ ( s .\/ ( R ./\ W ) ) = R ) <-> E. s e. A ( ( -. s .<_ W /\ ph ) /\ ( s .\/ ( R ./\ W ) ) = R ) ) )
42 17 41 mpbid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> E. s e. A ( ( -. s .<_ W /\ ph ) /\ ( s .\/ ( R ./\ W ) ) = R ) )
43 reusv1 
 |-  ( E. s e. A ( ( -. s .<_ W /\ ph ) /\ ( s .\/ ( R ./\ W ) ) = R ) -> ( E! z e. B A. s e. A ( ( ( -. s .<_ W /\ ph ) /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) <-> E. z e. B A. s e. A ( ( ( -. s .<_ W /\ ph ) /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) ) )
44 42 43 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 ) -> ( E! z e. B A. s e. A ( ( ( -. s .<_ W /\ ph ) /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) <-> E. z e. B A. s e. A ( ( ( -. s .<_ W /\ ph ) /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) ) )
45 10 44 mpbird 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ ps ) -> E! z e. B A. s e. A ( ( ( -. s .<_ W /\ ph ) /\ ( s .\/ ( R ./\ W ) ) = R ) -> z = ( N .\/ ( R ./\ W ) ) ) )