dihvalcq2

Description: Value of isomorphism H for a lattice K when -. X .<_ W , given auxiliary atom Q . (Contributed by NM, 26-Sep-2014)

	Ref	Expression
Hypotheses	dihvalcq2.b	$⊢ B = {Base}_{K}$
	dihvalcq2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihvalcq2.j	$⊢ \underset{˙}{\lor} = join (K)$
	dihvalcq2.m	$⊢ \underset{˙}{\land} = meet (K)$
	dihvalcq2.a	$⊢ A = Atoms (K)$
	dihvalcq2.h	$⊢ H = LHyp (K)$
	dihvalcq2.i	$⊢ I = DIsoH (K) (W)$
	dihvalcq2.u	$⊢ U = DVecH (K) (W)$
	dihvalcq2.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
Assertion	dihvalcq2	$⊢ ((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{˙}{\leq} X)) \to I (X) = I (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W)$

Proof

Step	Hyp	Ref	Expression
1		dihvalcq2.b	$⊢ B = {Base}_{K}$
2		dihvalcq2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihvalcq2.j	$⊢ \underset{˙}{\lor} = join (K)$
4		dihvalcq2.m	$⊢ \underset{˙}{\land} = meet (K)$
5		dihvalcq2.a	$⊢ A = Atoms (K)$
6		dihvalcq2.h	$⊢ H = LHyp (K)$
7		dihvalcq2.i	$⊢ I = DIsoH (K) (W)$
8		dihvalcq2.u	$⊢ U = DVecH (K) (W)$
9		dihvalcq2.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
10		simp1	$⊢ ((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{˙}{\leq} X)) \to (K \in HL \land W \in H)$
11		simp2	$⊢ ((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{˙}{\leq} X)) \to (X \in B \land \neg X \underset{˙}{\leq} W)$
12		simp3l	$⊢ ((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{˙}{\leq} X)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
13		simp3r	$⊢ ((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{˙}{\leq} X)) \to Q \underset{˙}{\leq} X$
14	1 2 3 4 5 6	lhpmcvr3	$⊢ ((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)) \to (Q \underset{˙}{\leq} X \leftrightarrow Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)$
15	10 11 12 14	syl3anc	$⊢ ((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{˙}{\leq} X)) \to (Q \underset{˙}{\leq} X \leftrightarrow Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)$
16	13 15	mpbid	$⊢ ((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{˙}{\leq} X)) \to Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X$
17		eqid	$⊢ DIsoB (K) (W) = DIsoB (K) (W)$
18		eqid	$⊢ DIsoC (K) (W) = DIsoC (K) (W)$
19	1 2 3 4 5 6 7 17 18 8 9	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) = DIsoC (K) (W) (Q) \underset{˙}{\oplus} DIsoB (K) (W) (X \underset{˙}{\land} W)$
20	10 11 12 16 19	syl112anc	$⊢ ((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{˙}{\leq} X)) \to I (X) = DIsoC (K) (W) (Q) \underset{˙}{\oplus} DIsoB (K) (W) (X \underset{˙}{\land} W)$
21	2 5 6 18 7	dihvalcqat	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) = DIsoC (K) (W) (Q)$
22	10 12 21	syl2anc	$⊢ ((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{˙}{\leq} X)) \to I (Q) = DIsoC (K) (W) (Q)$
23		simp1l	$⊢ ((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{˙}{\leq} X)) \to K \in HL$
24	23	hllatd	$⊢ ((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{˙}{\leq} X)) \to K \in Lat$
25		simp2l	$⊢ ((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{˙}{\leq} X)) \to X \in B$
26		simp1r	$⊢ ((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{˙}{\leq} X)) \to W \in H$
27	1 6	lhpbase	$⊢ W \in H \to W \in B$
28	26 27	syl	$⊢ ((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{˙}{\leq} X)) \to W \in B$
29	1 4	latmcl	$⊢ (K \in Lat \land X \in B \land W \in B) \to X \underset{˙}{\land} W \in B$
30	24 25 28 29	syl3anc	$⊢ ((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{˙}{\leq} X)) \to X \underset{˙}{\land} W \in B$
31	1 2 4	latmle2	$⊢ (K \in Lat \land X \in B \land W \in B) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} W$
32	24 25 28 31	syl3anc	$⊢ ((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{˙}{\leq} X)) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} W$
33	1 2 6 7 17	dihvalb	$⊢ ((K \in HL \land W \in H) \land (X \underset{˙}{\land} W \in B \land (X \underset{˙}{\land} W) \underset{˙}{\leq} W)) \to I (X \underset{˙}{\land} W) = DIsoB (K) (W) (X \underset{˙}{\land} W)$
34	10 30 32 33	syl12anc	$⊢ ((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{˙}{\leq} X)) \to I (X \underset{˙}{\land} W) = DIsoB (K) (W) (X \underset{˙}{\land} W)$
35	22 34	oveq12d	$⊢ ((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{˙}{\leq} X)) \to I (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) = DIsoC (K) (W) (Q) \underset{˙}{\oplus} DIsoB (K) (W) (X \underset{˙}{\land} W)$
36	20 35	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{˙}{\leq} X)) \to I (X) = I (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W)$

Metamath Proof Explorer

Theorem dihvalcq2

Proof