cdlemg17dALTN

Description: Same as cdlemg17dN with fewer antecedents but longer proof TODO: fix comment. (Contributed by NM, 9-May-2013) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cdlemg12.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemg12.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemg12.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdlemg12.a	$⊢ A = Atoms (K)$
5		cdlemg12.h	$⊢ H = LHyp (K)$
6		cdlemg12.t	$⊢ T = LTrn (K) (W)$
7		cdlemg12b.r	$⊢ R = trL (K) (W)$
8		simp3l	$⊢ ((K \in HL \land W \in H \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land P \neq Q) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land G (P) \neq P)) \to R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
9		simp11	$⊢ ((K \in HL \land W \in H \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land P \neq Q) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land G (P) \neq P)) \to K \in HL$
10		simp12	$⊢ ((K \in HL \land W \in H \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land P \neq Q) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land G (P) \neq P)) \to W \in H$
11		simp13	$⊢ ((K \in HL \land W \in H \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land P \neq Q) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land G (P) \neq P)) \to G \in T$
12	1 5 6 7	trlle	$⊢ ((K \in HL \land W \in H) \land G \in T) \to R (G) \underset{˙}{\leq} W$
13	9 10 11 12	syl21anc	$⊢ ((K \in HL \land W \in H \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land P \neq Q) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land G (P) \neq P)) \to R (G) \underset{˙}{\leq} W$
14	9	hllatd	$⊢ ((K \in HL \land W \in H \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land P \neq Q) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land G (P) \neq P)) \to K \in Lat$
15		eqid	$⊢ {Base}_{K} = {Base}_{K}$
16	15 5 6 7	trlcl	$⊢ ((K \in HL \land W \in H) \land G \in T) \to R (G) \in {Base}_{K}$
17	9 10 11 16	syl21anc	$⊢ ((K \in HL \land W \in H \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land P \neq Q) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land G (P) \neq P)) \to R (G) \in {Base}_{K}$
18		simp21l	$⊢ ((K \in HL \land W \in H \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land P \neq Q) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land G (P) \neq P)) \to P \in A$
19		simp22	$⊢ ((K \in HL \land W \in H \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land P \neq Q) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land G (P) \neq P)) \to Q \in A$
20	15 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
21	9 18 19 20	syl3anc	$⊢ ((K \in HL \land W \in H \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land P \neq Q) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land G (P) \neq P)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
22	15 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
23	10 22	syl	$⊢ ((K \in HL \land W \in H \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land P \neq Q) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land G (P) \neq P)) \to W \in {Base}_{K}$
24	15 1 3	latlem12	$⊢ (K \in Lat \land (R (G) \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K} \land W \in {Base}_{K})) \to ((R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (G) \underset{˙}{\leq} W) \leftrightarrow R (G) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$
25	14 17 21 23 24	syl13anc	$⊢ ((K \in HL \land W \in H \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land P \neq Q) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land G (P) \neq P)) \to ((R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (G) \underset{˙}{\leq} W) \leftrightarrow R (G) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$
26	8 13 25	mpbi2and	$⊢ ((K \in HL \land W \in H \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land P \neq Q) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land G (P) \neq P)) \to R (G) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$
27		hlatl	$⊢ K \in HL \to K \in AtLat$
28	9 27	syl	$⊢ ((K \in HL \land W \in H \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land P \neq Q) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land G (P) \neq P)) \to K \in AtLat$
29		simp21	$⊢ ((K \in HL \land W \in H \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land P \neq Q) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land G (P) \neq P)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
30		simp3r	$⊢ ((K \in HL \land W \in H \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land P \neq Q) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land G (P) \neq P)) \to G (P) \neq P$
31	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$
32	9 10 29 11 30 31	syl212anc	$⊢ ((K \in HL \land W \in H \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land P \neq Q) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land G (P) \neq P)) \to R (G) \in A$
33		simp23	$⊢ ((K \in HL \land W \in H \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land P \neq Q) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land G (P) \neq P)) \to P \neq Q$
34	1 2 3 4 5	lhpat	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land P \neq Q)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in A$
35	9 10 29 19 33 34	syl212anc	$⊢ ((K \in HL \land W \in H \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land P \neq Q) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land G (P) \neq P)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in A$
36	1 4	atcmp	$⊢ (K \in AtLat \land R (G) \in A \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in A) \to (R (G) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \leftrightarrow R (G) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$
37	28 32 35 36	syl3anc	$⊢ ((K \in HL \land W \in H \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land P \neq Q) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land G (P) \neq P)) \to (R (G) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \leftrightarrow R (G) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$
38	26 37	mpbid	$⊢ ((K \in HL \land W \in H \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land P \neq Q) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land G (P) \neq P)) \to R (G) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$

Metamath Proof Explorer

Theorem cdlemg17dALTN

Proof