Metamath Proof Explorer

Theorem cdlemd6

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 31-May-2012)

Ref Expression
Hypotheses cdlemd4.l ⊢≤˙=≤K
cdlemd4.j ⊢∨˙=join⁡K
cdlemd4.a ⊢A=Atoms⁡K
cdlemd4.h ⊢H=LHyp⁡K
cdlemd4.t ⊢T=LTrn⁡K⁡W
Assertion cdlemd6 ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧¬Q≤˙P∨˙F⁡P∧F⁡P=G⁡P→F⁡Q=G⁡Q

Proof

Step Hyp Ref Expression
1 cdlemd4.l ⊢≤˙=≤K
2 cdlemd4.j ⊢∨˙=join⁡K
3 cdlemd4.a ⊢A=Atoms⁡K
4 cdlemd4.h ⊢H=LHyp⁡K
5 cdlemd4.t ⊢T=LTrn⁡K⁡W
6 simp3 ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧¬Q≤˙P∨˙F⁡P∧F⁡P=G⁡P→F⁡P=G⁡P
7 6 oveq2d ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧¬Q≤˙P∨˙F⁡P∧F⁡P=G⁡P→P∨˙F⁡P=P∨˙G⁡P
8 7 oveq1d ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧¬Q≤˙P∨˙F⁡P∧F⁡P=G⁡P→P∨˙F⁡Pmeet⁡KW=P∨˙G⁡Pmeet⁡KW
9 simp1l ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧¬Q≤˙P∨˙F⁡P∧F⁡P=G⁡P→K∈HL∧W∈H
10 simp1rl ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧¬Q≤˙P∨˙F⁡P∧F⁡P=G⁡P→F∈T
11 simp21 ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧¬Q≤˙P∨˙F⁡P∧F⁡P=G⁡P→P∈A∧¬P≤˙W
12 eqid ⊢meet⁡K=meet⁡K
13 eqid ⊢trL⁡K⁡W=trL⁡K⁡W
14 1 2 12 3 4 5 13 trlval2 ⊢K∈HL∧W∈H∧F∈T∧P∈A∧¬P≤˙W→trL⁡K⁡W⁡F=P∨˙F⁡Pmeet⁡KW
15 9 10 11 14 syl3anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧¬Q≤˙P∨˙F⁡P∧F⁡P=G⁡P→trL⁡K⁡W⁡F=P∨˙F⁡Pmeet⁡KW
16 simp1rr ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧¬Q≤˙P∨˙F⁡P∧F⁡P=G⁡P→G∈T
17 1 2 12 3 4 5 13 trlval2 ⊢K∈HL∧W∈H∧G∈T∧P∈A∧¬P≤˙W→trL⁡K⁡W⁡G=P∨˙G⁡Pmeet⁡KW
18 9 16 11 17 syl3anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧¬Q≤˙P∨˙F⁡P∧F⁡P=G⁡P→trL⁡K⁡W⁡G=P∨˙G⁡Pmeet⁡KW
19 8 15 18 3eqtr4d ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧¬Q≤˙P∨˙F⁡P∧F⁡P=G⁡P→trL⁡K⁡W⁡F=trL⁡K⁡W⁡G
20 19 oveq2d ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧¬Q≤˙P∨˙F⁡P∧F⁡P=G⁡P→Q∨˙trL⁡K⁡W⁡F=Q∨˙trL⁡K⁡W⁡G
21 6 oveq1d ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧¬Q≤˙P∨˙F⁡P∧F⁡P=G⁡P→F⁡P∨˙P∨˙Qmeet⁡KW=G⁡P∨˙P∨˙Qmeet⁡KW
22 20 21 oveq12d ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧¬Q≤˙P∨˙F⁡P∧F⁡P=G⁡P→Q∨˙trL⁡K⁡W⁡Fmeet⁡KF⁡P∨˙P∨˙Qmeet⁡KW=Q∨˙trL⁡K⁡W⁡Gmeet⁡KG⁡P∨˙P∨˙Qmeet⁡KW
23 simp22 ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧¬Q≤˙P∨˙F⁡P∧F⁡P=G⁡P→Q∈A∧¬Q≤˙W
24 simp23 ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧¬Q≤˙P∨˙F⁡P∧F⁡P=G⁡P→¬Q≤˙P∨˙F⁡P
25 1 2 12 3 4 5 13 cdlemc ⊢K∈HL∧W∈H∧F∈T∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧¬Q≤˙P∨˙F⁡P→F⁡Q=Q∨˙trL⁡K⁡W⁡Fmeet⁡KF⁡P∨˙P∨˙Qmeet⁡KW
26 9 10 11 23 24 25 syl131anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧¬Q≤˙P∨˙F⁡P∧F⁡P=G⁡P→F⁡Q=Q∨˙trL⁡K⁡W⁡Fmeet⁡KF⁡P∨˙P∨˙Qmeet⁡KW
27 oveq2 ⊢F⁡P=G⁡P→P∨˙F⁡P=P∨˙G⁡P
28 27 breq2d ⊢F⁡P=G⁡P→Q≤˙P∨˙F⁡P↔Q≤˙P∨˙G⁡P
29 28 notbid ⊢F⁡P=G⁡P→¬Q≤˙P∨˙F⁡P↔¬Q≤˙P∨˙G⁡P
30 29 biimpd ⊢F⁡P=G⁡P→¬Q≤˙P∨˙F⁡P→¬Q≤˙P∨˙G⁡P
31 6 24 30 sylc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧¬Q≤˙P∨˙F⁡P∧F⁡P=G⁡P→¬Q≤˙P∨˙G⁡P
32 1 2 12 3 4 5 13 cdlemc ⊢K∈HL∧W∈H∧G∈T∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧¬Q≤˙P∨˙G⁡P→G⁡Q=Q∨˙trL⁡K⁡W⁡Gmeet⁡KG⁡P∨˙P∨˙Qmeet⁡KW
33 9 16 11 23 31 32 syl131anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧¬Q≤˙P∨˙F⁡P∧F⁡P=G⁡P→G⁡Q=Q∨˙trL⁡K⁡W⁡Gmeet⁡KG⁡P∨˙P∨˙Qmeet⁡KW
34 22 26 33 3eqtr4d ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧¬Q≤˙P∨˙F⁡P∧F⁡P=G⁡P→F⁡Q=G⁡Q