cdlemg19a

Description: Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-2013)

	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	cdlemg19a	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (Q \underset{˙}{\lor} F (G (Q))) = (P \underset{˙}{\lor} F (G (P))) \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		simp11l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to K \in HL$
9	8	hllatd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to K \in Lat$
10		simp12l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to P \in A$
11		simp11	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (K \in HL \land W \in H)$
12		simp21	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (F \in T \land G \in T)$
13	1 4 5 6	ltrncoat	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land P \in A) \to F (G (P)) \in A$
14	11 12 10 13	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to F (G (P)) \in A$
15		eqid	$⊢ {Base}_{K} = {Base}_{K}$
16	15 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land F (G (P)) \in A) \to P \underset{˙}{\lor} F (G (P)) \in {Base}_{K}$
17	8 10 14 16	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to P \underset{˙}{\lor} F (G (P)) \in {Base}_{K}$
18		simp13l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to Q \in A$
19	1 4 5 6	ltrncoat	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land Q \in A) \to F (G (Q)) \in A$
20	11 12 18 19	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to F (G (Q)) \in A$
21	15 2 4	hlatjcl	$⊢ (K \in HL \land Q \in A \land F (G (Q)) \in A) \to Q \underset{˙}{\lor} F (G (Q)) \in {Base}_{K}$
22	8 18 20 21	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to Q \underset{˙}{\lor} F (G (Q)) \in {Base}_{K}$
23	15 1 3	latmle1	$⊢ (K \in Lat \land P \underset{˙}{\lor} F (G (P)) \in {Base}_{K} \land Q \underset{˙}{\lor} F (G (Q)) \in {Base}_{K}) \to ((P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (Q \underset{˙}{\lor} F (G (Q)))) \underset{˙}{\leq} (P \underset{˙}{\lor} F (G (P)))$
24	9 17 22 23	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to ((P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (Q \underset{˙}{\lor} F (G (Q)))) \underset{˙}{\leq} (P \underset{˙}{\lor} F (G (P)))$
25	1 2 3 4 5 6 7	cdlemg18	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to ((P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (Q \underset{˙}{\lor} F (G (Q)))) \underset{˙}{\leq} W$
26	1 2 3 4 5 6 7	cdlemg18d	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (Q \underset{˙}{\lor} F (G (Q))) \in A$
27	15 4	atbase	$⊢ (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (Q \underset{˙}{\lor} F (G (Q))) \in A \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (Q \underset{˙}{\lor} F (G (Q))) \in {Base}_{K}$
28	26 27	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (Q \underset{˙}{\lor} F (G (Q))) \in {Base}_{K}$
29		simp11r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to W \in H$
30	15 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
31	29 30	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to W \in {Base}_{K}$
32	15 1 3	latlem12	$⊢ (K \in Lat \land ((P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (Q \underset{˙}{\lor} F (G (Q))) \in {Base}_{K} \land P \underset{˙}{\lor} F (G (P)) \in {Base}_{K} \land W \in {Base}_{K})) \to ((((P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (Q \underset{˙}{\lor} F (G (Q)))) \underset{˙}{\leq} (P \underset{˙}{\lor} F (G (P))) \land ((P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (Q \underset{˙}{\lor} F (G (Q)))) \underset{˙}{\leq} W) \leftrightarrow ((P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (Q \underset{˙}{\lor} F (G (Q)))) \underset{˙}{\leq} ((P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W))$
33	9 28 17 31 32	syl13anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to ((((P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (Q \underset{˙}{\lor} F (G (Q)))) \underset{˙}{\leq} (P \underset{˙}{\lor} F (G (P))) \land ((P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (Q \underset{˙}{\lor} F (G (Q)))) \underset{˙}{\leq} W) \leftrightarrow ((P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (Q \underset{˙}{\lor} F (G (Q)))) \underset{˙}{\leq} ((P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W))$
34	24 25 33	mpbi2and	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to ((P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (Q \underset{˙}{\lor} F (G (Q)))) \underset{˙}{\leq} ((P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W)$
35		hlatl	$⊢ K \in HL \to K \in AtLat$
36	8 35	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to K \in AtLat$
37		simp12	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
38		simp13	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
39		simp21l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to F \in T$
40		simp21r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to G \in T$
41		simp32	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q$
42	1 2 3 4 5 6	cdlemg11a	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q)) \to F (G (P)) \neq P$
43	11 37 38 39 40 41 42	syl123anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to F (G (P)) \neq P$
44	43	necomd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to P \neq F (G (P))$
45	1 2 3 4 5	lhpat	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F (G (P)) \in A \land P \neq F (G (P)))) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W \in A$
46	11 37 14 44 45	syl112anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W \in A$
47	1 4	atcmp	$⊢ (K \in AtLat \land (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (Q \underset{˙}{\lor} F (G (Q))) \in A \land (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W \in A) \to (((P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (Q \underset{˙}{\lor} F (G (Q)))) \underset{˙}{\leq} ((P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W) \leftrightarrow (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (Q \underset{˙}{\lor} F (G (Q))) = (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W)$
48	36 26 46 47	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (((P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (Q \underset{˙}{\lor} F (G (Q)))) \underset{˙}{\leq} ((P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W) \leftrightarrow (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (Q \underset{˙}{\lor} F (G (Q))) = (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W)$
49	34 48	mpbid	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land G (P) \neq P) \land (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (Q \underset{˙}{\lor} F (G (Q))) = (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W$

Metamath Proof Explorer

Theorem cdlemg19a

Proof