cdlemg10c

Description: TODO: FIX COMMENT. TODO: Can this be moved up as a stand-alone theorem in trl* area? (Contributed by NM, 4-May-2013)

	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	cdlemg10c	$⊢ ((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)) \to (R (F) \underset{˙}{\leq} (G (P) \underset{˙}{\lor} G (Q)) \leftrightarrow R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} 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		simp1	$⊢ ((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)) \to (K \in HL \land W \in H)$
9		simp3l	$⊢ ((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)) \to F \in T$
10	1 5 6 7	trlle	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \underset{˙}{\leq} W$
11	8 9 10	syl2anc	$⊢ ((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)) \to R (F) \underset{˙}{\leq} W$
12	11	biantrud	$⊢ ((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)) \to (R (F) \underset{˙}{\leq} (G (P) \underset{˙}{\lor} G (Q)) \leftrightarrow (R (F) \underset{˙}{\leq} (G (P) \underset{˙}{\lor} G (Q)) \land R (F) \underset{˙}{\leq} W))$
13		simp1l	$⊢ ((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)) \to K \in HL$
14	13	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)) \to K \in Lat$
15		eqid	$⊢ {Base}_{K} = {Base}_{K}$
16	15 5 6 7	trlcl	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \in {Base}_{K}$
17	8 9 16	syl2anc	$⊢ ((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)) \to R (F) \in {Base}_{K}$
18		simp3r	$⊢ ((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)) \to G \in T$
19		simp2ll	$⊢ ((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)) \to P \in A$
20	1 4 5 6	ltrnat	$⊢ ((K \in HL \land W \in H) \land G \in T \land P \in A) \to G (P) \in A$
21	8 18 19 20	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)) \to G (P) \in A$
22		simp2rl	$⊢ ((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)) \to Q \in A$
23	1 4 5 6	ltrnat	$⊢ ((K \in HL \land W \in H) \land G \in T \land Q \in A) \to G (Q) \in A$
24	8 18 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)) \to G (Q) \in A$
25	15 2 4	hlatjcl	$⊢ (K \in HL \land G (P) \in A \land G (Q) \in A) \to G (P) \underset{˙}{\lor} G (Q) \in {Base}_{K}$
26	13 21 24 25	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)) \to G (P) \underset{˙}{\lor} G (Q) \in {Base}_{K}$
27		simp1r	$⊢ ((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)) \to W \in H$
28	15 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
29	27 28	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)) \to W \in {Base}_{K}$
30	15 1 3	latlem12	$⊢ (K \in Lat \land (R (F) \in {Base}_{K} \land G (P) \underset{˙}{\lor} G (Q) \in {Base}_{K} \land W \in {Base}_{K})) \to ((R (F) \underset{˙}{\leq} (G (P) \underset{˙}{\lor} G (Q)) \land R (F) \underset{˙}{\leq} W) \leftrightarrow R (F) \underset{˙}{\leq} ((G (P) \underset{˙}{\lor} G (Q)) \underset{˙}{\land} W))$
31	14 17 26 29 30	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)) \to ((R (F) \underset{˙}{\leq} (G (P) \underset{˙}{\lor} G (Q)) \land R (F) \underset{˙}{\leq} W) \leftrightarrow R (F) \underset{˙}{\leq} ((G (P) \underset{˙}{\lor} G (Q)) \underset{˙}{\land} W))$
32	15 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
33	13 19 22 32	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)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
34	15 1 3	latlem12	$⊢ (K \in Lat \land (R (F) \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K} \land W \in {Base}_{K})) \to ((R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \underset{˙}{\leq} W) \leftrightarrow R (F) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$
35	14 17 33 29 34	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)) \to ((R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \underset{˙}{\leq} W) \leftrightarrow R (F) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$
36	11	biantrud	$⊢ ((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)) \to (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \underset{˙}{\leq} W))$
37	1 2 3 4 5 6	cdlemg10b	$⊢ ((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 G \in T) \to (G (P) \underset{˙}{\lor} G (Q)) \underset{˙}{\land} W = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
38	37	3adant3l	$⊢ ((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)) \to (G (P) \underset{˙}{\lor} G (Q)) \underset{˙}{\land} W = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
39	38	breq2d	$⊢ ((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)) \to (R (F) \underset{˙}{\leq} ((G (P) \underset{˙}{\lor} G (Q)) \underset{˙}{\land} W) \leftrightarrow R (F) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$
40	35 36 39	3bitr4rd	$⊢ ((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)) \to (R (F) \underset{˙}{\leq} ((G (P) \underset{˙}{\lor} G (Q)) \underset{˙}{\land} W) \leftrightarrow R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
41	12 31 40	3bitrd	$⊢ ((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)) \to (R (F) \underset{˙}{\leq} (G (P) \underset{˙}{\lor} G (Q)) \leftrightarrow R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$

Metamath Proof Explorer

Theorem cdlemg10c

Proof