This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdlemg2k

Description: cdleme42keg with simpler hypotheses. TODO: FIX COMMENT. TODO: derive from cdlemg3a , cdlemg2fv2 , cdlemg2jOLDN , ltrnel ? (Contributed by NM, 22-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	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} 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		eqid	$⊢ {Base}_{K} = {Base}_{K}$
9		eqid	$⊢ (p \underset{˙}{\lor} q) \underset{˙}{\land} W = (p \underset{˙}{\lor} q) \underset{˙}{\land} W$
10		eqid	$⊢ (t \underset{˙}{\lor} ((p \underset{˙}{\lor} q) \underset{˙}{\land} W)) \underset{˙}{\land} (q \underset{˙}{\lor} ((p \underset{˙}{\lor} t) \underset{˙}{\land} W)) = (t \underset{˙}{\lor} ((p \underset{˙}{\lor} q) \underset{˙}{\land} W)) \underset{˙}{\land} (q \underset{˙}{\lor} ((p \underset{˙}{\lor} t) \underset{˙}{\land} W))$
11		eqid	$⊢ (p \underset{˙}{\lor} q) \underset{˙}{\land} (((t \underset{˙}{\lor} ((p \underset{˙}{\lor} q) \underset{˙}{\land} W)) \underset{˙}{\land} (q \underset{˙}{\lor} ((p \underset{˙}{\lor} t) \underset{˙}{\land} W))) \underset{˙}{\lor} ((s \underset{˙}{\lor} t) \underset{˙}{\land} W)) = (p \underset{˙}{\lor} q) \underset{˙}{\land} (((t \underset{˙}{\lor} ((p \underset{˙}{\lor} q) \underset{˙}{\land} W)) \underset{˙}{\land} (q \underset{˙}{\lor} ((p \underset{˙}{\lor} t) \underset{˙}{\land} W))) \underset{˙}{\lor} ((s \underset{˙}{\lor} t) \underset{˙}{\land} W))$
12		eqid	$⊢ (x \in {Base}_{K} ⟼ if ((p \neq q \land \neg x \underset{˙}{\leq} W), (ι z \in {Base}_{K} \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (x \underset{˙}{\land} W) = x) \to z = if (s \underset{˙}{\leq} (p \underset{˙}{\lor} q), (ι y \in {Base}_{K} \| \forall t \in A ((\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (p \underset{˙}{\lor} q)) \to y = (p \underset{˙}{\lor} q) \underset{˙}{\land} (((t \underset{˙}{\lor} ((p \underset{˙}{\lor} q) \underset{˙}{\land} W)) \underset{˙}{\land} (q \underset{˙}{\lor} ((p \underset{˙}{\lor} t) \underset{˙}{\land} W))) \underset{˙}{\lor} ((s \underset{˙}{\lor} t) \underset{˙}{\land} W)))), ⦋ s / t ⦌ ((t \underset{˙}{\lor} ((p \underset{˙}{\lor} q) \underset{˙}{\land} W)) \underset{˙}{\land} (q \underset{˙}{\lor} ((p \underset{˙}{\lor} t) \underset{˙}{\land} W)))) \underset{˙}{\lor} (x \underset{˙}{\land} W))), x)) = (x \in {Base}_{K} ⟼ if ((p \neq q \land \neg x \underset{˙}{\leq} W), (ι z \in {Base}_{K} \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (x \underset{˙}{\land} W) = x) \to z = if (s \underset{˙}{\leq} (p \underset{˙}{\lor} q), (ι y \in {Base}_{K} \| \forall t \in A ((\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (p \underset{˙}{\lor} q)) \to y = (p \underset{˙}{\lor} q) \underset{˙}{\land} (((t \underset{˙}{\lor} ((p \underset{˙}{\lor} q) \underset{˙}{\land} W)) \underset{˙}{\land} (q \underset{˙}{\lor} ((p \underset{˙}{\lor} t) \underset{˙}{\land} W))) \underset{˙}{\lor} ((s \underset{˙}{\lor} t) \underset{˙}{\land} W)))), ⦋ s / t ⦌ ((t \underset{˙}{\lor} ((p \underset{˙}{\lor} q) \underset{˙}{\land} W)) \underset{˙}{\land} (q \underset{˙}{\lor} ((p \underset{˙}{\lor} t) \underset{˙}{\land} W)))) \underset{˙}{\lor} (x \underset{˙}{\land} W))), x))$
13	8 3 4 6 5 1 2 9 10 11 12 7	cdlemg2klem	$⊢ ((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} U$