dihoml4c

Description: Version of dihoml4 with closed subspaces. (Contributed by NM, 15-Jan-2015)

	Ref	Expression
Hypotheses	dihoml4c.h	$⊢ H = LHyp (K)$
	dihoml4c.i	$⊢ I = DIsoH (K) (W)$
	dihoml4c.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	dihoml4c.k	$⊢ φ \to (K \in HL \land W \in H)$
	dihoml4c.x	$⊢ φ \to X \in ran I$
	dihoml4c.y	$⊢ φ \to Y \in ran I$
	dihoml4c.l	$⊢ φ \to X \subseteq Y$
Assertion	dihoml4c	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap Y) \cap Y = X$

Proof

Step	Hyp	Ref	Expression
1		dihoml4c.h	$⊢ H = LHyp (K)$
2		dihoml4c.i	$⊢ I = DIsoH (K) (W)$
3		dihoml4c.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
4		dihoml4c.k	$⊢ φ \to (K \in HL \land W \in H)$
5		dihoml4c.x	$⊢ φ \to X \in ran I$
6		dihoml4c.y	$⊢ φ \to Y \in ran I$
7		dihoml4c.l	$⊢ φ \to X \subseteq Y$
8		eqid	$⊢ meet (K) = meet (K)$
9		inss1	$⊢ \underset{˙}{⊥} (X) \cap Y \subseteq \underset{˙}{⊥} (X)$
10		eqid	$⊢ DVecH (K) (W) = DVecH (K) (W)$
11		eqid	$⊢ {Base}_{DVecH (K) (W)} = {Base}_{DVecH (K) (W)}$
12	1 10 2 11	dihrnss	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to X \subseteq {Base}_{DVecH (K) (W)}$
13	4 5 12	syl2anc	$⊢ φ \to X \subseteq {Base}_{DVecH (K) (W)}$
14	1 10 11 3	dochssv	$⊢ ((K \in HL \land W \in H) \land X \subseteq {Base}_{DVecH (K) (W)}) \to \underset{˙}{⊥} (X) \subseteq {Base}_{DVecH (K) (W)}$
15	4 13 14	syl2anc	$⊢ φ \to \underset{˙}{⊥} (X) \subseteq {Base}_{DVecH (K) (W)}$
16	9 15	sstrid	$⊢ φ \to \underset{˙}{⊥} (X) \cap Y \subseteq {Base}_{DVecH (K) (W)}$
17	1 2 10 11 3	dochcl	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \cap Y \subseteq {Base}_{DVecH (K) (W)}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap Y) \in ran I$
18	4 16 17	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap Y) \in ran I$
19	8 1 2 4 18 6	dihmeet2	$⊢ φ \to I^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap Y) \cap Y) = I^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap Y)) meet (K) I^{-1} (Y)$
20		eqid	$⊢ oc (K) = oc (K)$
21	1 2 10 11 3	dochcl	$⊢ ((K \in HL \land W \in H) \land X \subseteq {Base}_{DVecH (K) (W)}) \to \underset{˙}{⊥} (X) \in ran I$
22	4 13 21	syl2anc	$⊢ φ \to \underset{˙}{⊥} (X) \in ran I$
23	1 2	dihmeetcl	$⊢ ((K \in HL \land W \in H) \land (\underset{˙}{⊥} (X) \in ran I \land Y \in ran I)) \to \underset{˙}{⊥} (X) \cap Y \in ran I$
24	4 22 6 23	syl12anc	$⊢ φ \to \underset{˙}{⊥} (X) \cap Y \in ran I$
25	20 1 2 3 4 24	dochvalr3	$⊢ φ \to oc (K) (I^{-1} (\underset{˙}{⊥} (X) \cap Y)) = I^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap Y))$
26	8 1 2 4 22 6	dihmeet2	$⊢ φ \to I^{-1} (\underset{˙}{⊥} (X) \cap Y) = I^{-1} (\underset{˙}{⊥} (X)) meet (K) I^{-1} (Y)$
27	20 1 2 3 4 5	dochvalr3	$⊢ φ \to oc (K) (I^{-1} (X)) = I^{-1} (\underset{˙}{⊥} (X))$
28	27	oveq1d	$⊢ φ \to oc (K) (I^{-1} (X)) meet (K) I^{-1} (Y) = I^{-1} (\underset{˙}{⊥} (X)) meet (K) I^{-1} (Y)$
29	26 28	eqtr4d	$⊢ φ \to I^{-1} (\underset{˙}{⊥} (X) \cap Y) = oc (K) (I^{-1} (X)) meet (K) I^{-1} (Y)$
30	29	fveq2d	$⊢ φ \to oc (K) (I^{-1} (\underset{˙}{⊥} (X) \cap Y)) = oc (K) (oc (K) (I^{-1} (X)) meet (K) I^{-1} (Y))$
31	25 30	eqtr3d	$⊢ φ \to I^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap Y)) = oc (K) (oc (K) (I^{-1} (X)) meet (K) I^{-1} (Y))$
32	31	oveq1d	$⊢ φ \to I^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap Y)) meet (K) I^{-1} (Y) = oc (K) (oc (K) (I^{-1} (X)) meet (K) I^{-1} (Y)) meet (K) I^{-1} (Y)$
33		eqid	$⊢ \leq_{K} = \leq_{K}$
34	33 1 2 4 5 6	dihcnvord	$⊢ φ \to (I^{-1} (X) \leq_{K} I^{-1} (Y) \leftrightarrow X \subseteq Y)$
35	7 34	mpbird	$⊢ φ \to I^{-1} (X) \leq_{K} I^{-1} (Y)$
36	4	simpld	$⊢ φ \to K \in HL$
37		hloml	$⊢ K \in HL \to K \in OML$
38	36 37	syl	$⊢ φ \to K \in OML$
39		eqid	$⊢ {Base}_{K} = {Base}_{K}$
40	39 1 2	dihcnvcl	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to I^{-1} (X) \in {Base}_{K}$
41	4 5 40	syl2anc	$⊢ φ \to I^{-1} (X) \in {Base}_{K}$
42	39 1 2	dihcnvcl	$⊢ ((K \in HL \land W \in H) \land Y \in ran I) \to I^{-1} (Y) \in {Base}_{K}$
43	4 6 42	syl2anc	$⊢ φ \to I^{-1} (Y) \in {Base}_{K}$
44	39 33 8 20	omllaw4	$⊢ (K \in OML \land I^{-1} (X) \in {Base}_{K} \land I^{-1} (Y) \in {Base}_{K}) \to (I^{-1} (X) \leq_{K} I^{-1} (Y) \to oc (K) (oc (K) (I^{-1} (X)) meet (K) I^{-1} (Y)) meet (K) I^{-1} (Y) = I^{-1} (X))$
45	38 41 43 44	syl3anc	$⊢ φ \to (I^{-1} (X) \leq_{K} I^{-1} (Y) \to oc (K) (oc (K) (I^{-1} (X)) meet (K) I^{-1} (Y)) meet (K) I^{-1} (Y) = I^{-1} (X))$
46	35 45	mpd	$⊢ φ \to oc (K) (oc (K) (I^{-1} (X)) meet (K) I^{-1} (Y)) meet (K) I^{-1} (Y) = I^{-1} (X)$
47	19 32 46	3eqtrd	$⊢ φ \to I^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap Y) \cap Y) = I^{-1} (X)$
48	1 2	dihmeetcl	$⊢ ((K \in HL \land W \in H) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap Y) \in ran I \land Y \in ran I)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap Y) \cap Y \in ran I$
49	4 18 6 48	syl12anc	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap Y) \cap Y \in ran I$
50	1 2 4 49 5	dihcnv11	$⊢ φ \to (I^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap Y) \cap Y) = I^{-1} (X) \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap Y) \cap Y = X)$
51	47 50	mpbid	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap Y) \cap Y = X$

Metamath Proof Explorer

Theorem dihoml4c

Proof