cdlemefrs29pre00

Description: ***START OF VALUE AT ATOM STUFF TO REPLACE ONES BELOW*** FIX COMMENT. TODO: see if this is the optimal utility theorem using lhpmat . (Contributed by NM, 29-Mar-2013)

	Ref	Expression
Hypotheses	cdlemefrs29.b	$⊢ B = {Base}_{K}$
	cdlemefrs29.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemefrs29.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemefrs29.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemefrs29.a	$⊢ A = Atoms (K)$
	cdlemefrs29.h	$⊢ H = LHyp (K)$
	cdlemefrs29.eq	$⊢ s = R \to (φ \leftrightarrow ψ)$
Assertion	cdlemefrs29pre00	$⊢ (((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land ψ) \land s \in A) \to (((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \leftrightarrow (\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R))$

Proof

Step	Hyp	Ref	Expression
1		cdlemefrs29.b	$⊢ B = {Base}_{K}$
2		cdlemefrs29.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemefrs29.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemefrs29.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdlemefrs29.a	$⊢ A = Atoms (K)$
6		cdlemefrs29.h	$⊢ H = LHyp (K)$
7		cdlemefrs29.eq	$⊢ s = R \to (φ \leftrightarrow ψ)$
8		anass	$⊢ ((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \leftrightarrow (\neg s \underset{˙}{\leq} W \land (φ \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R))$
9		simpl3	$⊢ (((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land ψ) \land s \in A) \to ψ$
10	7	pm5.32ri	$⊢ (φ \land s = R) \leftrightarrow (ψ \land s = R)$
11	10	baibr	$⊢ ψ \to (s = R \leftrightarrow (φ \land s = R))$
12	9 11	syl	$⊢ (((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land ψ) \land s \in A) \to (s = R \leftrightarrow (φ \land s = R))$
13		eqid	$⊢ 0. (K) = 0. (K)$
14	2 4 13 5 6	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)$
15	14	3adant3	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land ψ) \to R \underset{˙}{\land} W = 0. (K)$
16	15	adantr	$⊢ (((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land ψ) \land s \in A) \to R \underset{˙}{\land} W = 0. (K)$
17	16	oveq2d	$⊢ (((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land ψ) \land s \in A) \to s \underset{˙}{\lor} (R \underset{˙}{\land} W) = s \underset{˙}{\lor} 0. (K)$
18		simpl1l	$⊢ (((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land ψ) \land s \in A) \to K \in HL$
19		hlol	$⊢ K \in HL \to K \in OL$
20	18 19	syl	$⊢ (((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land ψ) \land s \in A) \to K \in OL$
21	1 5	atbase	$⊢ s \in A \to s \in B$
22	21	adantl	$⊢ (((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land ψ) \land s \in A) \to s \in B$
23	1 3 13	olj01	$⊢ (K \in OL \land s \in B) \to s \underset{˙}{\lor} 0. (K) = s$
24	20 22 23	syl2anc	$⊢ (((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land ψ) \land s \in A) \to s \underset{˙}{\lor} 0. (K) = s$
25	17 24	eqtrd	$⊢ (((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land ψ) \land s \in A) \to s \underset{˙}{\lor} (R \underset{˙}{\land} W) = s$
26	25	eqeq1d	$⊢ (((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land ψ) \land s \in A) \to (s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R \leftrightarrow s = R)$
27	26	anbi2d	$⊢ (((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land ψ) \land s \in A) \to ((φ \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \leftrightarrow (φ \land s = R))$
28	12 26 27	3bitr4d	$⊢ (((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land ψ) \land s \in A) \to (s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R \leftrightarrow (φ \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R))$
29	28	anbi2d	$⊢ (((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land ψ) \land s \in A) \to ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \leftrightarrow (\neg s \underset{˙}{\leq} W \land (φ \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R)))$
30	8 29	bitr4id	$⊢ (((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land ψ) \land s \in A) \to (((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \leftrightarrow (\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R))$

Metamath Proof Explorer

Theorem cdlemefrs29pre00

Proof