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

Metamath Proof Explorer

Theorem cdlemg2fv

Description: Value of a translation in terms of an associated atom. cdleme48fvg with simpler hypotheses. 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.b	$⊢ B = {Base}_{K}$
	Assertion	cdlemg2fv	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to F (X) = F (P) \underset{˙}{\lor} (X \underset{˙}{\land} W)$

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.b	$⊢ B = {Base}_{K}$
8		eqid	$⊢ (p \underset{˙}{\lor} q) \underset{˙}{\land} W = (p \underset{˙}{\lor} q) \underset{˙}{\land} W$
9		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))$
10		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))$
11		eqid	$⊢ (x \in B ⟼ if ((p \neq q \land \neg x \underset{˙}{\leq} W), (ι z \in B \| \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 B \| \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 B ⟼ if ((p \neq q \land \neg x \underset{˙}{\leq} W), (ι z \in B \| \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 B \| \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))$
12	7 3 4 6 5 1 2 8 9 10 11	cdlemg2fvlem	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to F (X) = F (P) \underset{˙}{\lor} (X \underset{˙}{\land} W)$