Metamath Proof Explorer


Theorem cdlemefr31fv1

Description: Value of ( FR ) when -. R .<_ ( P .\/ Q ) . TODO This may be useful for shortening others that now use riotasv 3d . TODO: FIX COMMENT. (Contributed by NM, 30-Mar-2013)

Ref Expression
Hypotheses cdlemefr27.b B = Base K
cdlemefr27.l ˙ = K
cdlemefr27.j ˙ = join K
cdlemefr27.m ˙ = meet K
cdlemefr27.a A = Atoms K
cdlemefr27.h H = LHyp K
cdlemefr27.u U = P ˙ Q ˙ W
cdlemefr27.c C = s ˙ U ˙ Q ˙ P ˙ s ˙ W
cdlemefr27.n N = if s ˙ P ˙ Q I C
cdleme29fr.o O = ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = N ˙ x ˙ W
cdleme29fr.f F = x B if P Q ¬ x ˙ W O x
cdleme43frv.x X = R ˙ U ˙ Q ˙ P ˙ R ˙ W
Assertion cdlemefr31fv1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q F R = X

Proof

Step Hyp Ref Expression
1 cdlemefr27.b B = Base K
2 cdlemefr27.l ˙ = K
3 cdlemefr27.j ˙ = join K
4 cdlemefr27.m ˙ = meet K
5 cdlemefr27.a A = Atoms K
6 cdlemefr27.h H = LHyp K
7 cdlemefr27.u U = P ˙ Q ˙ W
8 cdlemefr27.c C = s ˙ U ˙ Q ˙ P ˙ s ˙ W
9 cdlemefr27.n N = if s ˙ P ˙ Q I C
10 cdleme29fr.o O = ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = N ˙ x ˙ W
11 cdleme29fr.f F = x B if P Q ¬ x ˙ W O x
12 cdleme43frv.x X = R ˙ U ˙ Q ˙ P ˙ R ˙ W
13 1 2 3 4 5 6 7 8 9 10 11 cdlemefr32fva1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q F R = R / s N
14 simp2rl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q R A
15 simp3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q ¬ R ˙ P ˙ Q
16 8 9 12 cdleme31sn2 R A ¬ R ˙ P ˙ Q R / s N = X
17 14 15 16 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q R / s N = X
18 13 17 eqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q F R = X