cdlemg35

Description: TODO: Fix comment. TODO: should we have a more general version of hlsupr to avoid the =/= conditions? (Contributed by NM, 31-May-2013)

	Ref	Expression
Hypotheses	cdlemg35.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemg35.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemg35.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemg35.a	$⊢ A = Atoms (K)$
	cdlemg35.h	$⊢ H = LHyp (K)$
	cdlemg35.t	$⊢ T = LTrn (K) (W)$
	cdlemg35.r	$⊢ R = trL (K) (W)$
Assertion	cdlemg35	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to \exists v \in A (v \underset{˙}{\leq} W \land (v \neq R (F) \land v \neq R (G)))$

Proof

Step	Hyp	Ref	Expression
1		cdlemg35.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemg35.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemg35.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdlemg35.a	$⊢ A = Atoms (K)$
5		cdlemg35.h	$⊢ H = LHyp (K)$
6		cdlemg35.t	$⊢ T = LTrn (K) (W)$
7		cdlemg35.r	$⊢ R = trL (K) (W)$
8		simp1l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to K \in HL$
9		simp1	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to (K \in HL \land W \in H)$
10		simp21	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
11		simp22	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to F \in T$
12		simp31	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to F (P) \neq P$
13	1 4 5 6 7	trlat	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F \in T \land F (P) \neq P)) \to R (F) \in A$
14	9 10 11 12 13	syl112anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to R (F) \in A$
15		simp23	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to G \in T$
16		simp32	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to G (P) \neq P$
17	1 4 5 6 7	trlat	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (G \in T \land G (P) \neq P)) \to R (G) \in A$
18	9 10 15 16 17	syl112anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to R (G) \in A$
19		simp33	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to R (F) \neq R (G)$
20	1 2 4	hlsupr	$⊢ ((K \in HL \land R (F) \in A \land R (G) \in A) \land R (F) \neq R (G)) \to \exists v \in A (v \neq R (F) \land v \neq R (G) \land v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G)))$
21	8 14 18 19 20	syl31anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to \exists v \in A (v \neq R (F) \land v \neq R (G) \land v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G)))$
22		eqid	$⊢ {Base}_{K} = {Base}_{K}$
23		simp11l	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \land v \in A \land (v \neq R (F) \land v \neq R (G) \land v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G)))) \to K \in HL$
24	23	hllatd	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \land v \in A \land (v \neq R (F) \land v \neq R (G) \land v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G)))) \to K \in Lat$
25	22 4	atbase	$⊢ v \in A \to v \in {Base}_{K}$
26	25	3ad2ant2	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \land v \in A \land (v \neq R (F) \land v \neq R (G) \land v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G)))) \to v \in {Base}_{K}$
27		simp11	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \land v \in A \land (v \neq R (F) \land v \neq R (G) \land v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G)))) \to (K \in HL \land W \in H)$
28		simp122	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \land v \in A \land (v \neq R (F) \land v \neq R (G) \land v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G)))) \to F \in T$
29	22 5 6 7	trlcl	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \in {Base}_{K}$
30	27 28 29	syl2anc	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \land v \in A \land (v \neq R (F) \land v \neq R (G) \land v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G)))) \to R (F) \in {Base}_{K}$
31		simp123	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \land v \in A \land (v \neq R (F) \land v \neq R (G) \land v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G)))) \to G \in T$
32	22 5 6 7	trlcl	$⊢ ((K \in HL \land W \in H) \land G \in T) \to R (G) \in {Base}_{K}$
33	27 31 32	syl2anc	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \land v \in A \land (v \neq R (F) \land v \neq R (G) \land v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G)))) \to R (G) \in {Base}_{K}$
34	22 2	latjcl	$⊢ (K \in Lat \land R (F) \in {Base}_{K} \land R (G) \in {Base}_{K}) \to R (F) \underset{˙}{\lor} R (G) \in {Base}_{K}$
35	24 30 33 34	syl3anc	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \land v \in A \land (v \neq R (F) \land v \neq R (G) \land v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G)))) \to R (F) \underset{˙}{\lor} R (G) \in {Base}_{K}$
36		simp11r	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \land v \in A \land (v \neq R (F) \land v \neq R (G) \land v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G)))) \to W \in H$
37	22 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
38	36 37	syl	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \land v \in A \land (v \neq R (F) \land v \neq R (G) \land v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G)))) \to W \in {Base}_{K}$
39		simp33	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \land v \in A \land (v \neq R (F) \land v \neq R (G) \land v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G)))) \to v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G))$
40	1 5 6 7	trlle	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \underset{˙}{\leq} W$
41	27 28 40	syl2anc	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \land v \in A \land (v \neq R (F) \land v \neq R (G) \land v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G)))) \to R (F) \underset{˙}{\leq} W$
42	1 5 6 7	trlle	$⊢ ((K \in HL \land W \in H) \land G \in T) \to R (G) \underset{˙}{\leq} W$
43	27 31 42	syl2anc	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \land v \in A \land (v \neq R (F) \land v \neq R (G) \land v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G)))) \to R (G) \underset{˙}{\leq} W$
44	22 1 2	latjle12	$⊢ (K \in Lat \land (R (F) \in {Base}_{K} \land R (G) \in {Base}_{K} \land W \in {Base}_{K})) \to ((R (F) \underset{˙}{\leq} W \land R (G) \underset{˙}{\leq} W) \leftrightarrow (R (F) \underset{˙}{\lor} R (G)) \underset{˙}{\leq} W)$
45	24 30 33 38 44	syl13anc	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \land v \in A \land (v \neq R (F) \land v \neq R (G) \land v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G)))) \to ((R (F) \underset{˙}{\leq} W \land R (G) \underset{˙}{\leq} W) \leftrightarrow (R (F) \underset{˙}{\lor} R (G)) \underset{˙}{\leq} W)$
46	41 43 45	mpbi2and	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \land v \in A \land (v \neq R (F) \land v \neq R (G) \land v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G)))) \to (R (F) \underset{˙}{\lor} R (G)) \underset{˙}{\leq} W$
47	22 1 24 26 35 38 39 46	lattrd	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \land v \in A \land (v \neq R (F) \land v \neq R (G) \land v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G)))) \to v \underset{˙}{\leq} W$
48		simp31	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \land v \in A \land (v \neq R (F) \land v \neq R (G) \land v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G)))) \to v \neq R (F)$
49		simp32	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \land v \in A \land (v \neq R (F) \land v \neq R (G) \land v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G)))) \to v \neq R (G)$
50	47 48 49	jca32	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \land v \in A \land (v \neq R (F) \land v \neq R (G) \land v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G)))) \to (v \underset{˙}{\leq} W \land (v \neq R (F) \land v \neq R (G)))$
51	50	3expia	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \land v \in A) \to ((v \neq R (F) \land v \neq R (G) \land v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G))) \to (v \underset{˙}{\leq} W \land (v \neq R (F) \land v \neq R (G))))$
52	51	reximdva	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to (\exists v \in A (v \neq R (F) \land v \neq R (G) \land v \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G))) \to \exists v \in A (v \underset{˙}{\leq} W \land (v \neq R (F) \land v \neq R (G))))$
53	21 52	mpd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to \exists v \in A (v \underset{˙}{\leq} W \land (v \neq R (F) \land v \neq R (G)))$

Metamath Proof Explorer

Theorem cdlemg35

Proof