dihvalcqpre

Description: Value of isomorphism H for a lattice K when -. X .<_ W , given auxiliary atom Q . (Contributed by NM, 6-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	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)$

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	11	fvexi	$⊢ S \in V$
14		nfv	$⊢ Ⅎ q ((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))$
15		nfvd	$⊢ ((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 Ⅎ q I (X) = C (Q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W)$
16	1 2 3 4 5 6 7 8 9 10 11 12	dihvalc	$⊢ ((K \in HL \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)))$
17	16	3adant3	$⊢ ((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) = (ι 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)))$
18		eqeq1	$⊢ C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) = I (X) \to (C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) = C (Q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) \leftrightarrow I (X) = C (Q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W))$
19	18	adantl	$⊢ (((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)) \land C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) = I (X)) \to (C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) = C (Q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) \leftrightarrow I (X) = C (Q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W))$
20		simpl1	$⊢ (((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)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to (K \in HL \land W \in H)$
21		simprl	$⊢ (((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)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to q \in A$
22		simprrl	$⊢ (((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)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to \neg q \underset{˙}{\leq} W$
23	21 22	jca	$⊢ (((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)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to (q \in A \land \neg q \underset{˙}{\leq} W)$
24		simpl3l	$⊢ (((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)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
25		simpl2l	$⊢ (((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)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to X \in B$
26		simprrr	$⊢ (((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)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X$
27		simpl3r	$⊢ (((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)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X$
28	26 27	eqtr4d	$⊢ (((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)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to q \underset{˙}{\lor} (X \underset{˙}{\land} W) = Q \underset{˙}{\lor} (X \underset{˙}{\land} W)$
29	1 2 3 4 5 6 8 9 10 12	dihjust	$⊢ ((K \in HL \land W \in H) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land X \in B) \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = Q \underset{˙}{\lor} (X \underset{˙}{\land} W)) \to C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) = C (Q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W)$
30	20 23 24 25 28 29	syl131anc	$⊢ (((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)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) = C (Q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W)$
31	30	ex	$⊢ ((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 ((q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) = C (Q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W))$
32	1 2 3 4 5 6 7 8 9 10 11 12	dihlsscpre	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to I (X) \in S$
33	32	3adant3	$⊢ ((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) \in S$
34	1 2 3 4 5 6	lhpmcvr2	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to \exists q \in A (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)$
35	34	3adant3	$⊢ ((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 \exists q \in A (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)$
36	14 15 17 19 31 33 35	riotasv3d	$⊢ (((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)) \land S \in V) \to I (X) = C (Q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W)$
37	13 36	mpan2	$⊢ ((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 dihvalcqpre

Proof