cdlemg10bALTN

Description: TODO: FIX COMMENT. TODO: Can this be moved up as a stand-alone theorem in ltrn* area? TODO: Compare this proof to cdlemg2m and pick best, if moved to ltrn* area. (Contributed by NM, 4-May-2013) (New usage is discouraged.)

	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)$
Assertion	cdlemg10bALTN	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (F (P) \underset{˙}{\lor} F (Q)) \underset{˙}{\land} W = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$

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		simp11	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to K \in HL$
8		simp12	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to W \in H$
9	7 8	jca	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
10		3simpc	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))$
11		simp13	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to F \in T$
12		eqid	$⊢ (P \underset{˙}{\lor} Q) \underset{˙}{\land} W = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
13	5 6 1 2 4 3 12	cdlemg2k	$⊢ ((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) \to F (P) \underset{˙}{\lor} F (Q) = F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$
14	9 10 11 13	syl3anc	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\lor} F (Q) = F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$
15	14	oveq1d	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (F (P) \underset{˙}{\lor} F (Q)) \underset{˙}{\land} W = (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \underset{˙}{\land} W$
16		simp2	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
17	1 4 5 6	ltrnel	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)$
18	9 11 16 17	syl3anc	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)$
19		eqid	$⊢ 0. (K) = 0. (K)$
20	1 3 19 4 5	lhpmat	$⊢ ((K \in HL \land W \in H) \land (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\land} W = 0. (K)$
21	9 18 20	syl2anc	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\land} W = 0. (K)$
22	21	oveq1d	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (F (P) \underset{˙}{\land} W) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = 0. (K) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$
23		simp2l	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to P \in A$
24	1 4 5 6	ltrnat	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in A) \to F (P) \in A$
25	9 11 23 24	syl3anc	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to F (P) \in A$
26	7	hllatd	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to K \in Lat$
27		simp3l	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to Q \in A$
28		eqid	$⊢ {Base}_{K} = {Base}_{K}$
29	28 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
30	7 23 27 29	syl3anc	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
31	28 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
32	8 31	syl	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to W \in {Base}_{K}$
33	28 3	latmcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land W \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in {Base}_{K}$
34	26 30 32 33	syl3anc	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in {Base}_{K}$
35	28 1 3	latmle2	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land W \in {Base}_{K}) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W$
36	26 30 32 35	syl3anc	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W$
37	28 1 2 3 4	atmod4i2	$⊢ (K \in HL \land (F (P) \in A \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in {Base}_{K} \land W \in {Base}_{K}) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W) \to (F (P) \underset{˙}{\land} W) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \underset{˙}{\land} W$
38	7 25 34 32 36 37	syl131anc	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (F (P) \underset{˙}{\land} W) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \underset{˙}{\land} W$
39		hlol	$⊢ K \in HL \to K \in OL$
40	7 39	syl	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to K \in OL$
41	28 2 19	olj02	$⊢ (K \in OL \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in {Base}_{K}) \to 0. (K) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
42	40 34 41	syl2anc	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to 0. (K) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
43	22 38 42	3eqtr3d	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \underset{˙}{\land} W = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
44	15 43	eqtrd	$⊢ ((K \in HL \land W \in H \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (F (P) \underset{˙}{\lor} F (Q)) \underset{˙}{\land} W = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$

Metamath Proof Explorer

Theorem cdlemg10bALTN

Proof