Metamath Proof Explorer


Theorem cdlemefrs32fva

Description: Part of proof of Lemma E in Crawley p. 113. Value of F at an atom not under W . TODO: FIX COMMENT. TODO: consolidate uses of lhpmat here and elsewhere, and presence/absence of s .<_ ( P .\/ Q ) term. Also, why can proof be shortened with cdleme29cl ? What is difference from cdlemefs27cl ? (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
Assertion 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

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 simp2rl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ R A
12 1 5 atbase R A R B
13 eqid ι 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
14 10 13 cdleme31so R B R / x O = ι z B | s A ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W
15 11 12 14 3syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ R / x O = ι z B | s A ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W
16 ssidd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ B B
17 simpll ¬ s ˙ W φ s ˙ R ˙ W = R ¬ s ˙ W
18 simpr ¬ s ˙ W φ s ˙ R ˙ W = R s ˙ R ˙ W = R
19 17 18 jca ¬ s ˙ W φ s ˙ R ˙ W = R ¬ s ˙ W s ˙ R ˙ W = R
20 19 imim1i ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W ¬ s ˙ W φ s ˙ R ˙ W = R z = N ˙ R ˙ W
21 20 ralimi s A ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W s A ¬ s ˙ W φ s ˙ R ˙ W = R z = N ˙ R ˙ W
22 21 rgenw z B s A ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W s A ¬ s ˙ W φ s ˙ R ˙ W = R z = N ˙ R ˙ W
23 22 a1i 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 s A ¬ s ˙ W φ s ˙ R ˙ W = R z = N ˙ R ˙ W
24 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
25 simpl11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ s A K HL W H
26 simpl2r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ s A R A ¬ R ˙ W
27 simpl3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ s A ψ
28 simpr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ s A s A
29 1 2 3 4 5 6 7 cdlemefrs29pre00 K HL W H R A ¬ R ˙ W ψ s A ¬ s ˙ W φ s ˙ R ˙ W = R ¬ s ˙ W s ˙ R ˙ W = R
30 25 26 27 28 29 syl31anc 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
31 30 imbi1d 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 z = N ˙ R ˙ W ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W
32 31 ralbidva 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 z = N ˙ R ˙ W s A ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W
33 32 rexbidv 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
34 24 33 mpbid 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
35 1 2 3 4 5 6 7 8 9 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
36 riotass2 B B z B s A ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W 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 ∃! 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 = ι z B | s A ¬ s ˙ W φ s ˙ R ˙ W = R z = N ˙ R ˙ W
37 16 23 34 35 36 syl22anc 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
38 1 2 3 4 5 6 7 8 cdlemefrs29bpre0 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 z = N ˙ R ˙ W z = R / s N
39 38 adantr 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 = R / s N
40 9 39 riota5 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 = R / s N
41 15 37 40 3eqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ψ R / x O = R / s N