cdlemg11b

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

Proof

Step	Hyp	Ref	Expression
1		cdlemg8.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemg8.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemg8.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdlemg8.a	$⊢ A = Atoms (K)$
5		cdlemg8.h	$⊢ H = LHyp (K)$
6		cdlemg8.t	$⊢ T = LTrn (K) (W)$
7		cdlemg10.r	$⊢ R = trL (K) (W)$
8		simp33	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
9		simpl1	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to (K \in HL \land W \in H)$
10		simpl31	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to G \in T$
11		simpl2l	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
12	1 2 3 4 5 6 7	trlval2	$⊢ ((K \in HL \land W \in H) \land G \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to R (G) = (P \underset{˙}{\lor} G (P)) \underset{˙}{\land} W$
13	9 10 11 12	syl3anc	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to R (G) = (P \underset{˙}{\lor} G (P)) \underset{˙}{\land} W$
14		eqid	$⊢ {Base}_{K} = {Base}_{K}$
15		simpl1l	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to K \in HL$
16	15	hllatd	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to K \in Lat$
17		simp2ll	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \in A$
18	17	adantr	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to P \in A$
19	14 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
20	18 19	syl	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to P \in {Base}_{K}$
21	14 5 6	ltrncl	$⊢ ((K \in HL \land W \in H) \land G \in T \land P \in {Base}_{K}) \to G (P) \in {Base}_{K}$
22	9 10 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 (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to G (P) \in {Base}_{K}$
23	14 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land G (P) \in {Base}_{K}) \to P \underset{˙}{\lor} G (P) \in {Base}_{K}$
24	16 20 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 (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to P \underset{˙}{\lor} G (P) \in {Base}_{K}$
25		simpl1r	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to W \in H$
26	14 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
27	25 26	syl	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to W \in {Base}_{K}$
28	14 3	latmcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} G (P) \in {Base}_{K} \land W \in {Base}_{K}) \to (P \underset{˙}{\lor} G (P)) \underset{˙}{\land} W \in {Base}_{K}$
29	16 24 27 28	syl3anc	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to (P \underset{˙}{\lor} G (P)) \underset{˙}{\land} W \in {Base}_{K}$
30		simpl2r	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to Q \in A$
31	14 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
32	30 31	syl	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to Q \in {Base}_{K}$
33	14 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land Q \in {Base}_{K}) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
34	16 20 32 33	syl3anc	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
35	14 1 3	latmle1	$⊢ (K \in Lat \land P \underset{˙}{\lor} G (P) \in {Base}_{K} \land W \in {Base}_{K}) \to ((P \underset{˙}{\lor} G (P)) \underset{˙}{\land} W) \underset{˙}{\leq} (P \underset{˙}{\lor} G (P))$
36	16 24 27 35	syl3anc	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to ((P \underset{˙}{\lor} G (P)) \underset{˙}{\land} W) \underset{˙}{\leq} (P \underset{˙}{\lor} G (P))$
37	14 1 2	latlej1	$⊢ (K \in Lat \land P \in {Base}_{K} \land Q \in {Base}_{K}) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
38	16 20 32 37	syl3anc	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
39	14 5 6	ltrncl	$⊢ ((K \in HL \land W \in H) \land G \in T \land Q \in {Base}_{K}) \to G (Q) \in {Base}_{K}$
40	9 10 32 39	syl3anc	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to G (Q) \in {Base}_{K}$
41	14 1 2	latlej1	$⊢ (K \in Lat \land G (P) \in {Base}_{K} \land G (Q) \in {Base}_{K}) \to G (P) \underset{˙}{\leq} (G (P) \underset{˙}{\lor} G (Q))$
42	16 22 40 41	syl3anc	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to G (P) \underset{˙}{\leq} (G (P) \underset{˙}{\lor} G (Q))$
43		simpr	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)$
44	42 43	breqtrrd	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to G (P) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
45	14 1 2	latjle12	$⊢ (K \in Lat \land (P \in {Base}_{K} \land G (P) \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K})) \to ((P \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land G (P) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \leftrightarrow (P \underset{˙}{\lor} G (P)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
46	16 20 22 34 45	syl13anc	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to ((P \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land G (P) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \leftrightarrow (P \underset{˙}{\lor} G (P)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
47	38 44 46	mpbi2and	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to (P \underset{˙}{\lor} G (P)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
48	14 1 16 29 24 34 36 47	lattrd	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to ((P \underset{˙}{\lor} G (P)) \underset{˙}{\land} W) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
49	13 48	eqbrtrd	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q)) \to R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
50	49	ex	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (P \underset{˙}{\lor} Q = G (P) \underset{˙}{\lor} G (Q) \to R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
51	50	necon3bd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (\neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to P \underset{˙}{\lor} Q \neq G (P) \underset{˙}{\lor} G (Q))$
52	8 51	mpd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \underset{˙}{\lor} Q \neq G (P) \underset{˙}{\lor} G (Q)$

Metamath Proof Explorer

Theorem cdlemg11b

Proof