Metamath Proof Explorer


Theorem cdlemefrs32fva1

Description: Part of proof of Lemma E in Crawley p. 113. 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
cdleme29frs.o O = ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = N ˙ x ˙ W
cdleme29frs.f F = x B if P Q ¬ x ˙ W O x
Assertion cdlemefrs32fva1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ F R = R / s N

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 cdleme29frs.o O = ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = N ˙ x ˙ W
11 cdleme29frs.f F = x B if P Q ¬ x ˙ W O x
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 simp2l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ P Q
16 simp2rr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ ¬ R ˙ W
17 10 11 cdleme31fv1s R B P Q ¬ R ˙ W F R = R / x O
18 14 15 16 17 syl12anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ F R = R / x O
19 1 2 3 4 5 6 7 8 9 10 cdlemefrs32fva K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ R / x O = R / s N
20 18 19 eqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ F R = R / s N