cdlemg7fvbwN

Description: Properties of a translation of an element not under W . TODO: Fix comment. Can this be simplified? Perhaps derived from cdleme48bw ? Done with a *ltrn* theorem? (Contributed by NM, 28-Apr-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdlemg4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemg4.a	$⊢ A = Atoms (K)$
	cdlemg4.h	$⊢ H = LHyp (K)$
	cdlemg4.t	$⊢ T = LTrn (K) (W)$
	cdlemg4.b	$⊢ B = {Base}_{K}$
Assertion	cdlemg7fvbwN	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \to (F (X) \in B \land \neg F (X) \underset{˙}{\leq} W)$

Proof

Step	Hyp	Ref	Expression
1		cdlemg4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemg4.a	$⊢ A = Atoms (K)$
3		cdlemg4.h	$⊢ H = LHyp (K)$
4		cdlemg4.t	$⊢ T = LTrn (K) (W)$
5		cdlemg4.b	$⊢ B = {Base}_{K}$
6		eqid	$⊢ join (K) = join (K)$
7		eqid	$⊢ meet (K) = meet (K)$
8	5 1 6 7 2 3	lhpmcvr2	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to \exists r \in A (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)$
9	8	3adant3	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \to \exists r \in A (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)$
10		simp11	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to (K \in HL \land W \in H)$
11		simp2	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to r \in A$
12		simp3l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to \neg r \underset{˙}{\leq} W$
13	11 12	jca	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to (r \in A \land \neg r \underset{˙}{\leq} W)$
14		simp12	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to (X \in B \land \neg X \underset{˙}{\leq} W)$
15		simp13	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to F \in T$
16		simp3r	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to r join (K) (X meet (K) W) = X$
17	3 4 1 6 2 7 5	cdlemg2fv	$⊢ ((K \in HL \land W \in H) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land r join (K) (X meet (K) W) = X)) \to F (X) = F (r) join (K) (X meet (K) W)$
18	10 13 14 15 16 17	syl122anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to F (X) = F (r) join (K) (X meet (K) W)$
19		simp11l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to K \in HL$
20	19	hllatd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to K \in Lat$
21	1 2 3 4	ltrnel	$⊢ ((K \in HL \land W \in H) \land F \in T \land (r \in A \land \neg r \underset{˙}{\leq} W)) \to (F (r) \in A \land \neg F (r) \underset{˙}{\leq} W)$
22	21	simpld	$⊢ ((K \in HL \land W \in H) \land F \in T \land (r \in A \land \neg r \underset{˙}{\leq} W)) \to F (r) \in A$
23	10 15 13 22	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to F (r) \in A$
24	5 2	atbase	$⊢ F (r) \in A \to F (r) \in B$
25	23 24	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to F (r) \in B$
26		simp12l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to X \in B$
27		simp11r	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to W \in H$
28	5 3	lhpbase	$⊢ W \in H \to W \in B$
29	27 28	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to W \in B$
30	5 7	latmcl	$⊢ (K \in Lat \land X \in B \land W \in B) \to X meet (K) W \in B$
31	20 26 29 30	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to X meet (K) W \in B$
32	5 6	latjcl	$⊢ (K \in Lat \land F (r) \in B \land X meet (K) W \in B) \to F (r) join (K) (X meet (K) W) \in B$
33	20 25 31 32	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to F (r) join (K) (X meet (K) W) \in B$
34	18 33	eqeltrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to F (X) \in B$
35	21	simprd	$⊢ ((K \in HL \land W \in H) \land F \in T \land (r \in A \land \neg r \underset{˙}{\leq} W)) \to \neg F (r) \underset{˙}{\leq} W$
36	10 15 13 35	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to \neg F (r) \underset{˙}{\leq} W$
37	5 1 6	latlej1	$⊢ (K \in Lat \land F (r) \in B \land X meet (K) W \in B) \to F (r) \underset{˙}{\leq} (F (r) join (K) (X meet (K) W))$
38	20 25 31 37	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to F (r) \underset{˙}{\leq} (F (r) join (K) (X meet (K) W))$
39	5 1	lattr	$⊢ (K \in Lat \land (F (r) \in B \land F (r) join (K) (X meet (K) W) \in B \land W \in B)) \to ((F (r) \underset{˙}{\leq} (F (r) join (K) (X meet (K) W)) \land (F (r) join (K) (X meet (K) W)) \underset{˙}{\leq} W) \to F (r) \underset{˙}{\leq} W)$
40	20 25 33 29 39	syl13anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to ((F (r) \underset{˙}{\leq} (F (r) join (K) (X meet (K) W)) \land (F (r) join (K) (X meet (K) W)) \underset{˙}{\leq} W) \to F (r) \underset{˙}{\leq} W)$
41	38 40	mpand	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to ((F (r) join (K) (X meet (K) W)) \underset{˙}{\leq} W \to F (r) \underset{˙}{\leq} W)$
42	36 41	mtod	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to \neg (F (r) join (K) (X meet (K) W)) \underset{˙}{\leq} W$
43	18	breq1d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to (F (X) \underset{˙}{\leq} W \leftrightarrow (F (r) join (K) (X meet (K) W)) \underset{˙}{\leq} W)$
44	42 43	mtbird	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to \neg F (X) \underset{˙}{\leq} W$
45	34 44	jca	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to (F (X) \in B \land \neg F (X) \underset{˙}{\leq} W)$
46	45	rexlimdv3a	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \to (\exists r \in A (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X) \to (F (X) \in B \land \neg F (X) \underset{˙}{\leq} W))$
47	9 46	mpd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land F \in T) \to (F (X) \in B \land \neg F (X) \underset{˙}{\leq} W)$

Metamath Proof Explorer

Theorem cdlemg7fvbwN

Proof