cdlemg2fv2

Description: Value of a translation in terms of an associated atom. TODO: FIX COMMENT. TODO: Is this useful elsewhere e.g. around cdlemeg46fjv that use more complex proofs? TODO: Use ltrnj to vastly simplify. (Contributed by NM, 23-Apr-2013)

	Ref	Expression
Hypotheses	cdlemg2inv.h	$⊢ H = LHyp (K)$
	cdlemg2inv.t	$⊢ T = LTrn (K) (W)$
	cdlemg2j.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemg2j.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemg2j.a	$⊢ A = Atoms (K)$
	cdlemg2j.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemg2j.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
Assertion	cdlemg2fv2	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to F (R \underset{˙}{\lor} U) = F (R) \underset{˙}{\lor} U$

Proof

Step	Hyp	Ref	Expression
1		cdlemg2inv.h	$⊢ H = LHyp (K)$
2		cdlemg2inv.t	$⊢ T = LTrn (K) (W)$
3		cdlemg2j.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
4		cdlemg2j.j	$⊢ \underset{˙}{\lor} = join (K)$
5		cdlemg2j.a	$⊢ A = Atoms (K)$
6		cdlemg2j.m	$⊢ \underset{˙}{\land} = meet (K)$
7		cdlemg2j.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} 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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to (K \in HL \land W \in H)$
9		simp23	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
10		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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to K \in HL$
11	10	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to K \in Lat$
12		simp23l	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to R \in A$
13		eqid	$⊢ {Base}_{K} = {Base}_{K}$
14	13 5	atbase	$⊢ R \in A \to R \in {Base}_{K}$
15	12 14	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to R \in {Base}_{K}$
16		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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to W \in H$
17		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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to P \in A$
18		simp22l	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to Q \in A$
19	3 4 6 5 1 7 13	cdleme0aa	$⊢ ((K \in HL \land W \in H) \land P \in A \land Q \in A) \to U \in {Base}_{K}$
20	10 16 17 18 19	syl211anc	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to U \in {Base}_{K}$
21	13 4	latjcl	$⊢ (K \in Lat \land R \in {Base}_{K} \land U \in {Base}_{K}) \to R \underset{˙}{\lor} U \in {Base}_{K}$
22	11 15 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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to R \underset{˙}{\lor} U \in {Base}_{K}$
23		simp23r	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to \neg R \underset{˙}{\leq} W$
24	13 3 4	latlej1	$⊢ (K \in Lat \land R \in {Base}_{K} \land U \in {Base}_{K}) \to R \underset{˙}{\leq} (R \underset{˙}{\lor} U)$
25	11 15 20 24	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to R \underset{˙}{\leq} (R \underset{˙}{\lor} U)$
26	13 1	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
27	16 26	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to W \in {Base}_{K}$
28	13 3	lattr	$⊢ (K \in Lat \land (R \in {Base}_{K} \land R \underset{˙}{\lor} U \in {Base}_{K} \land W \in {Base}_{K})) \to ((R \underset{˙}{\leq} (R \underset{˙}{\lor} U) \land (R \underset{˙}{\lor} U) \underset{˙}{\leq} W) \to R \underset{˙}{\leq} W)$
29	11 15 22 27 28	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to ((R \underset{˙}{\leq} (R \underset{˙}{\lor} U) \land (R \underset{˙}{\lor} U) \underset{˙}{\leq} W) \to R \underset{˙}{\leq} W)$
30	25 29	mpand	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to ((R \underset{˙}{\lor} U) \underset{˙}{\leq} W \to R \underset{˙}{\leq} W)$
31	23 30	mtod	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to \neg (R \underset{˙}{\lor} U) \underset{˙}{\leq} W$
32	22 31	jca	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to (R \underset{˙}{\lor} U \in {Base}_{K} \land \neg (R \underset{˙}{\lor} U) \underset{˙}{\leq} W)$
33		simp3	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to F \in T$
34		eqid	$⊢ 0. (K) = 0. (K)$
35	3 6 34 5 1	lhpmat	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to R \underset{˙}{\land} W = 0. (K)$
36	8 9 35	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to R \underset{˙}{\land} W = 0. (K)$
37	36	oveq1d	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to (R \underset{˙}{\land} W) \underset{˙}{\lor} U = 0. (K) \underset{˙}{\lor} U$
38	13 4 5	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
39	10 17 18 38	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
40	13 3 6	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$
41	11 39 27 40	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W$
42	7 41	eqbrtrid	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to U \underset{˙}{\leq} W$
43	13 3 4 6 5	atmod4i2	$⊢ (K \in HL \land (R \in A \land U \in {Base}_{K} \land W \in {Base}_{K}) \land U \underset{˙}{\leq} W) \to (R \underset{˙}{\land} W) \underset{˙}{\lor} U = (R \underset{˙}{\lor} U) \underset{˙}{\land} W$
44	10 12 20 27 42 43	syl131anc	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to (R \underset{˙}{\land} W) \underset{˙}{\lor} U = (R \underset{˙}{\lor} U) \underset{˙}{\land} W$
45		hlol	$⊢ K \in HL \to K \in OL$
46	10 45	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to K \in OL$
47	13 4 34	olj02	$⊢ (K \in OL \land U \in {Base}_{K}) \to 0. (K) \underset{˙}{\lor} U = U$
48	46 20 47	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to 0. (K) \underset{˙}{\lor} U = U$
49	37 44 48	3eqtr3d	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to (R \underset{˙}{\lor} U) \underset{˙}{\land} W = U$
50	49	oveq2d	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to R \underset{˙}{\lor} ((R \underset{˙}{\lor} U) \underset{˙}{\land} W) = R \underset{˙}{\lor} U$
51	1 2 3 4 5 6 13	cdlemg2fv	$⊢ ((K \in HL \land W \in H) \land ((R \in A \land \neg R \underset{˙}{\leq} W) \land (R \underset{˙}{\lor} U \in {Base}_{K} \land \neg (R \underset{˙}{\lor} U) \underset{˙}{\leq} W)) \land (F \in T \land R \underset{˙}{\lor} ((R \underset{˙}{\lor} U) \underset{˙}{\land} W) = R \underset{˙}{\lor} U)) \to F (R \underset{˙}{\lor} U) = F (R) \underset{˙}{\lor} ((R \underset{˙}{\lor} U) \underset{˙}{\land} W)$
52	8 9 32 33 50 51	syl122anc	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to F (R \underset{˙}{\lor} U) = F (R) \underset{˙}{\lor} ((R \underset{˙}{\lor} U) \underset{˙}{\land} W)$
53	49	oveq2d	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to F (R) \underset{˙}{\lor} ((R \underset{˙}{\lor} U) \underset{˙}{\land} W) = F (R) \underset{˙}{\lor} U$
54	52 53	eqtrd	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land F \in T) \to F (R \underset{˙}{\lor} U) = F (R) \underset{˙}{\lor} U$

Metamath Proof Explorer

Theorem cdlemg2fv2

Proof