Metamath Proof Explorer


Theorem cdleme4gfv

Description: Part of proof of Lemma D in Crawley p. 113. TODO: Can this replace uses of cdleme32a ? TODO: Can this be used to help prove the R or S case where X is an atom? TODO: Would an antecedent transformer like cdleme46f2g2 help? (Contributed by NM, 8-Apr-2013)

Ref Expression
Hypotheses cdlemef47.b B = Base K
cdlemef47.l ˙ = K
cdlemef47.j ˙ = join K
cdlemef47.m ˙ = meet K
cdlemef47.a A = Atoms K
cdlemef47.h H = LHyp K
cdlemef47.v V = Q ˙ P ˙ W
cdlemef47.n N = v ˙ V ˙ P ˙ Q ˙ v ˙ W
cdlemefs47.o O = Q ˙ P ˙ N ˙ u ˙ v ˙ W
cdlemef47.g G = a B if Q P ¬ a ˙ W ι c B | u A ¬ u ˙ W u ˙ a ˙ W = a c = if u ˙ Q ˙ P ι b B | v A ¬ v ˙ W ¬ v ˙ Q ˙ P b = O u / v N ˙ a ˙ W a
Assertion cdleme4gfv K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W S A ¬ S ˙ W S ˙ X ˙ W = X G X = G S ˙ X ˙ W

Proof

Step Hyp Ref Expression
1 cdlemef47.b B = Base K
2 cdlemef47.l ˙ = K
3 cdlemef47.j ˙ = join K
4 cdlemef47.m ˙ = meet K
5 cdlemef47.a A = Atoms K
6 cdlemef47.h H = LHyp K
7 cdlemef47.v V = Q ˙ P ˙ W
8 cdlemef47.n N = v ˙ V ˙ P ˙ Q ˙ v ˙ W
9 cdlemefs47.o O = Q ˙ P ˙ N ˙ u ˙ v ˙ W
10 cdlemef47.g G = a B if Q P ¬ a ˙ W ι c B | u A ¬ u ˙ W u ˙ a ˙ W = a c = if u ˙ Q ˙ P ι b B | v A ¬ v ˙ W ¬ v ˙ Q ˙ P b = O u / v N ˙ a ˙ W a
11 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W S A ¬ S ˙ W S ˙ X ˙ W = X K HL W H
12 simp13 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W S A ¬ S ˙ W S ˙ X ˙ W = X Q A ¬ Q ˙ W
13 simp12 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W S A ¬ S ˙ W S ˙ X ˙ W = X P A ¬ P ˙ W
14 simp2l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W S A ¬ S ˙ W S ˙ X ˙ W = X P Q
15 14 necomd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W S A ¬ S ˙ W S ˙ X ˙ W = X Q P
16 simp2r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W S A ¬ S ˙ W S ˙ X ˙ W = X X B ¬ X ˙ W
17 simp3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W S A ¬ S ˙ W S ˙ X ˙ W = X S A ¬ S ˙ W S ˙ X ˙ W = X
18 1 2 3 4 5 6 7 8 9 10 cdleme48fv K HL W H Q A ¬ Q ˙ W P A ¬ P ˙ W Q P X B ¬ X ˙ W S A ¬ S ˙ W S ˙ X ˙ W = X G X = G S ˙ X ˙ W
19 11 12 13 15 16 17 18 syl321anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W S A ¬ S ˙ W S ˙ X ˙ W = X G X = G S ˙ X ˙ W