Metamath Proof Explorer


Theorem cdleme48d

Description: TODO: fix comment. (Contributed by NM, 8-Apr-2013)

Ref Expression
Hypotheses cdlemef46g.b B = Base K
cdlemef46g.l ˙ = K
cdlemef46g.j ˙ = join K
cdlemef46g.m ˙ = meet K
cdlemef46g.a A = Atoms K
cdlemef46g.h H = LHyp K
cdlemef46g.u U = P ˙ Q ˙ W
cdlemef46g.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdlemefs46g.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
cdlemef46g.f F = x B if P Q ¬ x ˙ W ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D ˙ x ˙ W x
cdlemef46.v V = Q ˙ P ˙ W
cdlemef46.n N = v ˙ V ˙ P ˙ Q ˙ v ˙ W
cdlemefs46.o O = Q ˙ P ˙ N ˙ u ˙ v ˙ W
cdlemef46.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 cdleme48d 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 F X = X

Proof

Step Hyp Ref Expression
1 cdlemef46g.b B = Base K
2 cdlemef46g.l ˙ = K
3 cdlemef46g.j ˙ = join K
4 cdlemef46g.m ˙ = meet K
5 cdlemef46g.a A = Atoms K
6 cdlemef46g.h H = LHyp K
7 cdlemef46g.u U = P ˙ Q ˙ W
8 cdlemef46g.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
9 cdlemefs46g.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
10 cdlemef46g.f F = x B if P Q ¬ x ˙ W ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D ˙ x ˙ W x
11 cdlemef46.v V = Q ˙ P ˙ W
12 cdlemef46.n N = v ˙ V ˙ P ˙ Q ˙ v ˙ W
13 cdlemefs46.o O = Q ˙ P ˙ N ˙ u ˙ v ˙ W
14 cdlemef46.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
15 simp1 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 P A ¬ P ˙ W Q A ¬ Q ˙ W
16 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
17 simp2rl 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
18 vex s V
19 eqid s ˙ U ˙ Q ˙ P ˙ s ˙ W = s ˙ U ˙ Q ˙ P ˙ s ˙ W
20 8 19 cdleme31sc s V s / t D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
21 18 20 ax-mp s / t D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
22 eqid ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E
23 eqid if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D
24 eqid ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D ˙ x ˙ W = ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D ˙ x ˙ W
25 1 2 3 4 5 6 7 21 8 9 22 23 24 10 cdleme32fvcl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B F X B
26 15 17 25 syl2anc 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 F X B
27 1 2 3 4 5 6 7 8 9 10 cdleme48bw 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 ¬ F X ˙ W
28 26 27 jca 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 F X B ¬ F X ˙ W
29 simp3l 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
30 1 2 3 4 5 6 7 8 9 10 cdleme46fvaw K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W F S A ¬ F S ˙ W
31 15 29 30 syl2anc 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 F S A ¬ F S ˙ W
32 1 2 3 4 5 6 7 8 9 10 cdleme48b 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 F X ˙ W = X ˙ W
33 32 oveq2d 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 F S ˙ F X ˙ W = F S ˙ X ˙ W
34 1 2 3 4 5 6 7 8 9 10 cdleme48fv 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 F X = F S ˙ X ˙ W
35 33 34 eqtr4d 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 F S ˙ F X ˙ W = F X
36 1 2 3 4 5 6 11 12 13 14 cdleme4gfv K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q F X B ¬ F X ˙ W F S A ¬ F S ˙ W F S ˙ F X ˙ W = F X G F X = G F S ˙ F X ˙ W
37 15 16 28 31 35 36 syl122anc 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 F X = G F S ˙ F X ˙ W
38 1 2 3 4 5 6 7 8 9 10 11 12 13 14 cdlemeg46gf K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W G F S = S
39 15 16 29 38 syl12anc 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 F S = S
40 39 32 oveq12d 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 F S ˙ F X ˙ W = S ˙ X ˙ W
41 simp3r 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 ˙ X ˙ W = X
42 37 40 41 3eqtrd 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 F X = X