dihlsscpre

Description: Closure of isomorphism H for a lattice K when -. X .<_ W . (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	dihlsscpre	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to I (X) \in S$

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	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)))$
14		simp1l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land (\neg r \underset{˙}{\leq} W \land r \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to (K \in HL \land W \in H)$
15		simp2l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land (\neg r \underset{˙}{\leq} W \land r \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to q \in A$
16		simp3ll	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land (\neg r \underset{˙}{\leq} W \land r \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to \neg q \underset{˙}{\leq} W$
17	15 16	jca	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land (\neg r \underset{˙}{\leq} W \land r \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to (q \in A \land \neg q \underset{˙}{\leq} W)$
18		simp2r	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land (\neg r \underset{˙}{\leq} W \land r \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to r \in A$
19		simp3rl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land (\neg r \underset{˙}{\leq} W \land r \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to \neg r \underset{˙}{\leq} W$
20	18 19	jca	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land (\neg r \underset{˙}{\leq} W \land r \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to (r \in A \land \neg r \underset{˙}{\leq} W)$
21		simp1rl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land (\neg r \underset{˙}{\leq} W \land r \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to X \in B$
22		simp3lr	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land (\neg r \underset{˙}{\leq} W \land r \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X$
23		simp3rr	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land (\neg r \underset{˙}{\leq} W \land r \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to r \underset{˙}{\lor} (X \underset{˙}{\land} W) = X$
24	22 23	eqtr4d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land (\neg r \underset{˙}{\leq} W \land r \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to q \underset{˙}{\lor} (X \underset{˙}{\land} W) = r \underset{˙}{\lor} (X \underset{˙}{\land} W)$
25	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 (r \in A \land \neg r \underset{˙}{\leq} W) \land X \in B) \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = r \underset{˙}{\lor} (X \underset{˙}{\land} W)) \to C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) = C (r) \underset{˙}{\oplus} D (X \underset{˙}{\land} W)$
26	14 17 20 21 24 25	syl131anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (q \in A \land r \in A) \land ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land (\neg r \underset{˙}{\leq} W \land r \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) = C (r) \underset{˙}{\oplus} D (X \underset{˙}{\land} W)$
27	26	3exp	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to ((q \in A \land r \in A) \to (((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land (\neg r \underset{˙}{\leq} W \land r \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) = C (r) \underset{˙}{\oplus} D (X \underset{˙}{\land} W)))$
28	27	ralrimivv	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to \forall q \in A \forall r \in A (((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land (\neg r \underset{˙}{\leq} W \land r \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) = C (r) \underset{˙}{\oplus} D (X \underset{˙}{\land} W))$
29	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)$
30		simpll	$⊢ (((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 (K \in HL \land W \in H)$
31	6 10 30	dvhlmod	$⊢ (((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 U \in LMod$
32	2 5 6 10 9 11	diclss	$⊢ ((K \in HL \land W \in H) \land (q \in A \land \neg q \underset{˙}{\leq} W)) \to C (q) \in S$
33	32	adantlr	$⊢ (((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 C (q) \in S$
34		hllat	$⊢ K \in HL \to K \in Lat$
35	34	ad3antrrr	$⊢ (((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 K \in Lat$
36		simplrl	$⊢ (((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 X \in B$
37	1 6	lhpbase	$⊢ W \in H \to W \in B$
38	37	ad3antlr	$⊢ (((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 W \in B$
39	1 4	latmcl	$⊢ (K \in Lat \land X \in B \land W \in B) \to X \underset{˙}{\land} W \in B$
40	35 36 38 39	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)) \to X \underset{˙}{\land} W \in B$
41	1 2 4	latmle2	$⊢ (K \in Lat \land X \in B \land W \in B) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} W$
42	35 36 38 41	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)) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} W$
43	1 2 6 10 8 11	diblss	$⊢ ((K \in HL \land W \in H) \land (X \underset{˙}{\land} W \in B \land (X \underset{˙}{\land} W) \underset{˙}{\leq} W)) \to D (X \underset{˙}{\land} W) \in S$
44	30 40 42 43	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)) \to D (X \underset{˙}{\land} W) \in S$
45	11 12	lsmcl	$⊢ (U \in LMod \land C (q) \in S \land D (X \underset{˙}{\land} W) \in S) \to C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) \in S$
46	31 33 44 45	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)) \to C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) \in S$
47	46	a1d	$⊢ (((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{˙}{\lor} (X \underset{˙}{\land} W) = X \to C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) \in S)$
48	47	expr	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land q \in A) \to (\neg q \underset{˙}{\leq} W \to (q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \to C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) \in S))$
49	48	impd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land q \in A) \to ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) \in S)$
50	49	ancld	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land q \in A) \to ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) \in S))$
51	50	reximdva	$⊢ ((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) \to \exists q \in A ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) \in S))$
52	29 51	mpd	$⊢ ((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) \land C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) \in S)$
53		breq1	$⊢ q = r \to (q \underset{˙}{\leq} W \leftrightarrow r \underset{˙}{\leq} W)$
54	53	notbid	$⊢ q = r \to (\neg q \underset{˙}{\leq} W \leftrightarrow \neg r \underset{˙}{\leq} W)$
55		oveq1	$⊢ q = r \to q \underset{˙}{\lor} (X \underset{˙}{\land} W) = r \underset{˙}{\lor} (X \underset{˙}{\land} W)$
56	55	eqeq1d	$⊢ q = r \to (q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \leftrightarrow r \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)$
57	54 56	anbi12d	$⊢ q = r \to ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \leftrightarrow (\neg r \underset{˙}{\leq} W \land r \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))$
58		fveq2	$⊢ q = r \to C (q) = C (r)$
59	58	oveq1d	$⊢ q = r \to C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) = C (r) \underset{˙}{\oplus} D (X \underset{˙}{\land} W)$
60	57 59	reusv3	$⊢ \exists q \in A ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) \in S) \to (\forall q \in A \forall r \in A (((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land (\neg r \underset{˙}{\leq} W \land r \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) = C (r) \underset{˙}{\oplus} D (X \underset{˙}{\land} W)) \leftrightarrow \exists 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)))$
61	52 60	syl	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to (\forall q \in A \forall r \in A (((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \land (\neg r \underset{˙}{\leq} W \land r \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to C (q) \underset{˙}{\oplus} D (X \underset{˙}{\land} W) = C (r) \underset{˙}{\oplus} D (X \underset{˙}{\land} W)) \leftrightarrow \exists 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)))$
62	28 61	mpbid	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to \exists 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))$
63		reusv1	$⊢ \exists q \in A (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to (\exists! 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)) \leftrightarrow \exists 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)))$
64	29 63	syl	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to (\exists! 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)) \leftrightarrow \exists 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)))$
65	62 64	mpbird	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to \exists! 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))$
66		riotacl	$⊢ \exists! 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)) \to (ι 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))) \in S$
67	65 66	syl	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to (ι 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))) \in S$
68	13 67	eqeltrd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to I (X) \in S$

Metamath Proof Explorer

Theorem dihlsscpre

Proof