dihvalcq

Description: Value of isomorphism H for a lattice K when -. X .<_ W , given auxiliary atom Q . TODO: Use dihvalcq2 (with lhpmcvr3 for ( Q .\/ ( X ./\ W ) ) = X simplification) that changes C and D to I and make this obsolete. Do to other theorems as well. (Contributed by NM, 6-Mar-2014)

	Ref	Expression
Hypotheses	dihvalcq.b	$⊢ B = {Base}_{K}$
	dihvalcq.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihvalcq.j	$⊢ \underset{˙}{\lor} = join (K)$
	dihvalcq.m	$⊢ \underset{˙}{\land} = meet (K)$
	dihvalcq.a	$⊢ A = Atoms (K)$
	dihvalcq.h	$⊢ H = LHyp (K)$
	dihvalcq.i	$⊢ I = DIsoH (K) (W)$
	dihvalcq.d	$⊢ D = DIsoB (K) (W)$
	dihvalcq.c	$⊢ C = DIsoC (K) (W)$
	dihvalcq.u	$⊢ U = DVecH (K) (W)$
	dihvalcq.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
Assertion	dihvalcq	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to I (X) = C (Q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W)$

Proof

Step	Hyp	Ref	Expression
1		dihvalcq.b	$⊢ B = {Base}_{K}$
2		dihvalcq.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihvalcq.j	$⊢ \underset{˙}{\lor} = join (K)$
4		dihvalcq.m	$⊢ \underset{˙}{\land} = meet (K)$
5		dihvalcq.a	$⊢ A = Atoms (K)$
6		dihvalcq.h	$⊢ H = LHyp (K)$
7		dihvalcq.i	$⊢ I = DIsoH (K) (W)$
8		dihvalcq.d	$⊢ D = DIsoB (K) (W)$
9		dihvalcq.c	$⊢ C = DIsoC (K) (W)$
10		dihvalcq.u	$⊢ U = DVecH (K) (W)$
11		dihvalcq.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
12		eqid	$⊢ LSubSp (U) = LSubSp (U)$
13	1 2 3 4 5 6 7 8 9 10 12 11	dihvalcqpre	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to I (X) = C (Q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W)$

Metamath Proof Explorer

Theorem dihvalcq

Proof