Metamath Proof Explorer


Theorem cdlemeg47b

Description: TODO: FIX COMMENT. (Contributed by NM, 1-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 cdlemeg47b K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q G S = S / v N

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 3 5 cdleme46f2g2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q K HL W H Q A ¬ Q ˙ W P A ¬ P ˙ W Q P S A ¬ S ˙ W ¬ S ˙ Q ˙ P
12 1 2 3 4 5 6 7 8 10 cdlemefr45 K HL W H Q A ¬ Q ˙ W P A ¬ P ˙ W Q P S A ¬ S ˙ W ¬ S ˙ Q ˙ P G S = S / v N
13 11 12 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q G S = S / v N