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

Metamath Proof Explorer

Theorem dihvalc

Description: Value of isomorphism H for a lattice K when -. X .<_ W . (Contributed by NM, 4-Mar-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dihval.b	$⊢ B = {Base}_{K}$
2		dihval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihval.j	$⊢ \underset{˙}{\lor} = join (K)$
4		dihval.m	$⊢ \underset{˙}{\land} = meet (K)$
5		dihval.a	$⊢ A = Atoms (K)$
6		dihval.h	$⊢ H = LHyp (K)$
7		dihval.i	$⊢ I = DIsoH (K) (W)$
8		dihval.d	$⊢ D = DIsoB (K) (W)$
9		dihval.c	$⊢ C = DIsoC (K) (W)$
10		dihval.u	$⊢ U = DVecH (K) (W)$
11		dihval.s	$⊢ S = LSubSp (U)$
12		dihval.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
13	1 2 3 4 5 6 7 8 9 10 11 12	dihval	$⊢ ((K \in V \land W \in H) \land X \in B) \to I (X) = if (X \underset{˙}{\leq} W, D (X), (ι u \in S \| \forall q \in A ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to u = C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W))))$
14		iffalse	$⊢ \neg X \underset{˙}{\leq} W \to if (X \underset{˙}{\leq} W, D (X), (ι u \in S \| \forall q \in A ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to u = C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W)))) = (ι u \in S \| \forall q \in A ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to u = C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W)))$
15	13 14	sylan9eq	$⊢ (((K \in V \land W \in H) \land X \in B) \land \neg X \underset{˙}{\leq} W) \to I (X) = (ι u \in S \| \forall q \in A ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to u = C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W)))$
16	15	anasss	$⊢ ((K \in V \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to I (X) = (ι u \in S \| \forall q \in A ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to u = C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W)))$