Metamath Proof Explorer


Theorem cdleme42f

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 8-Mar-2013)

Ref Expression
Hypotheses cdleme41.b B = Base K
cdleme41.l ˙ = K
cdleme41.j ˙ = join K
cdleme41.m ˙ = meet K
cdleme41.a A = Atoms K
cdleme41.h H = LHyp K
cdleme41.u U = P ˙ Q ˙ W
cdleme41.d D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
cdleme41.e E = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdleme41.g G = P ˙ Q ˙ E ˙ s ˙ t ˙ W
cdleme41.i I = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = G
cdleme41.n N = if s ˙ P ˙ Q I D
cdleme41.o O = ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = N ˙ x ˙ W
cdleme41.f F = x B if P Q ¬ x ˙ W O x
cdleme34e.v V = R ˙ S ˙ W
Assertion cdleme42f K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q F R ˙ V = F R ˙ V

Proof

Step Hyp Ref Expression
1 cdleme41.b B = Base K
2 cdleme41.l ˙ = K
3 cdleme41.j ˙ = join K
4 cdleme41.m ˙ = meet K
5 cdleme41.a A = Atoms K
6 cdleme41.h H = LHyp K
7 cdleme41.u U = P ˙ Q ˙ W
8 cdleme41.d D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
9 cdleme41.e E = t ˙ U ˙ Q ˙ P ˙ t ˙ W
10 cdleme41.g G = P ˙ Q ˙ E ˙ s ˙ t ˙ W
11 cdleme41.i I = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = G
12 cdleme41.n N = if s ˙ P ˙ Q I D
13 cdleme41.o O = ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = N ˙ x ˙ W
14 cdleme41.f F = x B if P Q ¬ x ˙ W O x
15 cdleme34e.v V = R ˙ S ˙ W
16 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 cdleme42e K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q F R ˙ V = R / s N ˙ R ˙ V ˙ W
17 1 2 3 4 5 6 7 8 9 10 11 12 13 14 cdleme32fva1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q F R = R / s N
18 17 3adant2r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q F R = R / s N
19 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q K HL W H
20 simp2l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R A ¬ R ˙ W
21 simp2r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q S A ¬ S ˙ W
22 1 2 3 4 5 6 15 cdleme42a K HL W H R A ¬ R ˙ W S A ¬ S ˙ W R ˙ S = R ˙ V
23 19 20 21 22 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ S = R ˙ V
24 23 oveq1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ S ˙ W = R ˙ V ˙ W
25 15 24 syl5eq K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q V = R ˙ V ˙ W
26 18 25 oveq12d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q F R ˙ V = R / s N ˙ R ˙ V ˙ W
27 16 26 eqtr4d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q F R ˙ V = F R ˙ V