Metamath Proof Explorer


Theorem cdlemeg46nlpq

Description: Show that ( GS ) is not under P .\/ Q when S isn't. (Contributed by NM, 3-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 cdlemeg46nlpq K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q ¬ G S ˙ P ˙ Q

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 simp11 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
16 simp13 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q Q A ¬ Q ˙ W
17 simp12 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q P A ¬ P ˙ W
18 simp2l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q P Q
19 18 necomd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q Q P
20 simp2r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q S A ¬ S ˙ W
21 simp3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q ¬ S ˙ P ˙ Q
22 simp11l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q K HL
23 simp12l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q P A
24 simp13l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q Q A
25 3 5 hlatjcom K HL P A Q A P ˙ Q = Q ˙ P
26 22 23 24 25 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q P ˙ Q = Q ˙ P
27 26 breq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q S ˙ P ˙ Q S ˙ Q ˙ P
28 21 27 mtbid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q ¬ S ˙ Q ˙ P
29 1 2 3 4 5 6 11 12 13 14 cdleme46frvlpq K HL W H Q A ¬ Q ˙ W P A ¬ P ˙ W Q P S A ¬ S ˙ W ¬ S ˙ Q ˙ P ¬ G S ˙ Q ˙ P
30 15 16 17 19 20 28 29 syl321anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q ¬ G S ˙ Q ˙ P
31 26 breq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q G S ˙ P ˙ Q G S ˙ Q ˙ P
32 30 31 mtbird K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q ¬ G S ˙ P ˙ Q