Metamath Proof Explorer


Theorem cdleme42k

Description: Part of proof of Lemma E in Crawley p. 113. Since F ' S =/= F'R when S =/= R (i.e. 1-1); then ( ( F ' R ) .\/ ( F ' S ) ) is 2-dim therefore = ( ( F ' R ) .\/ V ) by cdleme42i and ps-1 TODO: FIX COMMENT. (Contributed by NM, 20-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 cdleme42k K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S F R ˙ F S = 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 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
17 simp22 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S R A ¬ R ˙ W
18 simp23 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S S A ¬ S ˙ W
19 simp21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S P Q
20 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 cdleme42i K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q F R ˙ F S ˙ F R ˙ V
21 16 17 18 19 20 syl121anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S F R ˙ F S ˙ F R ˙ V
22 simp11l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S K HL
23 1 2 3 4 5 6 7 8 9 10 11 12 13 14 cdleme32fvaw K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W F R A ¬ F R ˙ W
24 23 simpld K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W F R A
25 16 17 24 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S F R A
26 1 2 3 4 5 6 7 8 9 10 11 12 13 14 cdleme32fvaw K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W F S A ¬ F S ˙ W
27 26 simpld K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W F S A
28 16 18 27 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S F S A
29 1 2 3 4 5 6 7 8 9 10 11 12 13 14 cdleme41fva11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S F R F S
30 simp11r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S W H
31 simp22l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S R A
32 simp22r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S ¬ R ˙ W
33 simp23l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S S A
34 simp3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S R S
35 2 3 4 5 6 15 cdleme0a K HL W H R A ¬ R ˙ W S A R S V A
36 22 30 31 32 33 34 35 syl222anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S V A
37 2 3 5 ps-1 K HL F R A F S A F R F S F R A V A F R ˙ F S ˙ F R ˙ V F R ˙ F S = F R ˙ V
38 22 25 28 29 25 36 37 syl132anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S F R ˙ F S ˙ F R ˙ V F R ˙ F S = F R ˙ V
39 21 38 mpbid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S F R ˙ F S = F R ˙ V