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		simpl3	$⊢ (((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land ψ) \land s \in A) \to ψ$
9	7	pm5.32ri	$⊢ (φ \land s = R) \leftrightarrow (ψ \land s = R)$
10	9	baibr	$⊢ ψ \to (s = R \leftrightarrow (φ \land s = R))$
11	8 10	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))$
12		eqid	$⊢ 0. (K) = 0. (K)$
13	2 4 12 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)$
14	13	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)$
15	14	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)$
16	15	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)$
17		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$
18		hlol	$⊢ K \in HL \to K \in OL$
19	17 18	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$
20	1 5	atbase	$⊢ s \in A \to s \in B$
21	20	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$
22	1 3 12	olj01	$⊢ (K \in OL \land s \in B) \to s \underset{˙}{\lor} 0. (K) = s$
23	19 21 22	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$
24	16 23	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$
25	24	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)$
26	25	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))$
27	11 25 26	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))$
28	27	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)))$
29		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))$
30	28 29	syl6rbbr	$⊢ (((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