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 ˙ = K
cdlemefrs27.j ˙ = join K
cdlemefrs27.m ˙ = meet K
cdlemefrs27.a A = Atoms K
cdlemefrs27.h H = LHyp K
cdlemefrs27.eq s = R φ ψ
cdlemefrs27.nb K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W φ N B
cdlemefrs27.rnb K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ R / s N B
Assertion cdlemefrs29cpre1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ ∃! z B s A ¬ s ˙ W φ s ˙ R ˙ W = R z = N ˙ R ˙ W

Proof

Step Hyp Ref Expression
1 cdlemefrs27.b B = Base K
2 cdlemefrs27.l ˙ = 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 φ ψ
8 cdlemefrs27.nb K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W φ N B
9 cdlemefrs27.rnb K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ R / s N B
10 1 2 3 4 5 6 7 8 9 cdlemefrs29bpre1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ z B s A ¬ s ˙ W φ s ˙ R ˙ W = R z = N ˙ R ˙ W
11 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ K HL W H
12 simp2rl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ R A
13 1 5 atbase R A R B
14 12 13 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ R B
15 simp2rr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ ¬ R ˙ W
16 1 2 3 4 5 6 lhpmcvr2 K HL W H R B ¬ R ˙ W s A ¬ s ˙ W s ˙ R ˙ W = R
17 11 14 15 16 syl12anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ s A ¬ s ˙ W s ˙ R ˙ W = R
18 simpl3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ s A ψ
19 7 pm5.32ri φ s = R ψ s = R
20 19 baibr ψ s = R φ s = R
21 18 20 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ s A s = R φ s = R
22 simp2r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ R A ¬ R ˙ W
23 eqid 0. K = 0. K
24 2 4 23 5 6 lhpmat K HL W H R A ¬ R ˙ W R ˙ W = 0. K
25 11 22 24 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ R ˙ W = 0. K
26 25 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ s A R ˙ W = 0. K
27 26 oveq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ s A s ˙ R ˙ W = s ˙ 0. K
28 simp11l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ K HL
29 hlol K HL K OL
30 28 29 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ K OL
31 1 5 atbase s A s B
32 1 3 23 olj01 K OL s B s ˙ 0. K = s
33 30 31 32 syl2an K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ s A s ˙ 0. K = s
34 27 33 eqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ s A s ˙ R ˙ W = s
35 34 eqeq1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ s A s ˙ R ˙ W = R s = R
36 35 anbi2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ s A φ s ˙ R ˙ W = R φ s = R
37 21 35 36 3bitr4d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ s A s ˙ R ˙ W = R φ s ˙ R ˙ W = R
38 37 anbi2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ s A ¬ s ˙ W s ˙ R ˙ W = R ¬ s ˙ W φ s ˙ R ˙ W = R
39 anass ¬ s ˙ W φ s ˙ R ˙ W = R ¬ s ˙ W φ s ˙ R ˙ W = R
40 38 39 bitr4di K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ s A ¬ s ˙ W s ˙ R ˙ W = R ¬ s ˙ W φ s ˙ R ˙ W = R
41 40 rexbidva K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ s A ¬ s ˙ W s ˙ R ˙ W = R s A ¬ s ˙ W φ s ˙ R ˙ W = R
42 17 41 mpbid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ s A ¬ s ˙ W φ s ˙ R ˙ W = R
43 reusv1 s A ¬ s ˙ W φ s ˙ R ˙ W = R ∃! z B s A ¬ s ˙ W φ s ˙ R ˙ W = R z = N ˙ R ˙ W z B s A ¬ s ˙ W φ s ˙ R ˙ W = R z = N ˙ R ˙ W
44 42 43 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ ∃! z B s A ¬ s ˙ W φ s ˙ R ˙ W = R z = N ˙ R ˙ W z B s A ¬ s ˙ W φ s ˙ R ˙ W = R z = N ˙ R ˙ W
45 10 44 mpbird K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ ∃! z B s A ¬ s ˙ W φ s ˙ R ˙ W = R z = N ˙ R ˙ W