# Metamath Proof Explorer

## Theorem cdlemefrs29cpre1

Description: TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013)

Ref Expression
Hypotheses cdlemefrs27.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
cdlemefrs27.l
cdlemefrs27.j
cdlemefrs27.m
cdlemefrs27.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdlemefrs27.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdlemefrs27.eq ${⊢}{s}={R}\to \left({\phi }↔{\psi }\right)$
cdlemefrs27.nb
cdlemefrs27.rnb
Assertion cdlemefrs29cpre1

### Proof

Step Hyp Ref Expression
1 cdlemefrs27.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cdlemefrs27.l
3 cdlemefrs27.j
4 cdlemefrs27.m
5 cdlemefrs27.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
6 cdlemefrs27.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
7 cdlemefrs27.eq ${⊢}{s}={R}\to \left({\phi }↔{\psi }\right)$
8 cdlemefrs27.nb
9 cdlemefrs27.rnb
10 1 2 3 4 5 6 7 8 9 cdlemefrs29bpre1
11 simp11
12 simp2rl
13 1 5 atbase ${⊢}{R}\in {A}\to {R}\in {B}$
14 12 13 syl
15 simp2rr
16 1 2 3 4 5 6 lhpmcvr2
17 11 14 15 16 syl12anc
18 simpl3
19 7 pm5.32ri ${⊢}\left({\phi }\wedge {s}={R}\right)↔\left({\psi }\wedge {s}={R}\right)$
20 19 baibr ${⊢}{\psi }\to \left({s}={R}↔\left({\phi }\wedge {s}={R}\right)\right)$
21 18 20 syl
22 simp2r
23 eqid ${⊢}\mathrm{0.}\left({K}\right)=\mathrm{0.}\left({K}\right)$
24 2 4 23 5 6 lhpmat
25 11 22 24 syl2anc
27 26 oveq2d
28 simp11l
29 hlol ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OL}$
30 28 29 syl
31 1 5 atbase ${⊢}{s}\in {A}\to {s}\in {B}$
32 1 3 23 olj01
33 30 31 32 syl2an
34 27 33 eqtrd
35 34 eqeq1d
36 35 anbi2d
37 21 35 36 3bitr4d
38 37 anbi2d
39 anass
40 38 39 syl6bbr
41 40 rexbidva
42 17 41 mpbid
43 reusv1
44 42 43 syl
45 10 44 mpbird