dihoml4

Description: Orthomodular law for constructed vector space H. Lemma 3.3(1) in Holland95 p. 215. ( poml4N analog.) (Contributed by NM, 15-Jan-2015)

	Ref	Expression
Hypotheses	dihoml4.h	$⊢ H = LHyp (K)$
	dihoml4.u	$⊢ U = DVecH (K) (W)$
	dihoml4.s	$⊢ S = LSubSp (U)$
	dihoml4.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	dihoml4.k	$⊢ φ \to (K \in HL \land W \in H)$
	dihoml4.x	$⊢ φ \to X \in S$
	dihoml4.y	$⊢ φ \to Y \in S$
	dihoml4.c	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y$
	dihoml4.l	$⊢ φ \to X \subseteq Y$
Assertion	dihoml4	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap Y) \cap Y = \underset{˙}{⊥} (\underset{˙}{⊥} (X))$

Proof

Step	Hyp	Ref	Expression
1		dihoml4.h	$⊢ H = LHyp (K)$
2		dihoml4.u	$⊢ U = DVecH (K) (W)$
3		dihoml4.s	$⊢ S = LSubSp (U)$
4		dihoml4.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
5		dihoml4.k	$⊢ φ \to (K \in HL \land W \in H)$
6		dihoml4.x	$⊢ φ \to X \in S$
7		dihoml4.y	$⊢ φ \to Y \in S$
8		dihoml4.c	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y$
9		dihoml4.l	$⊢ φ \to X \subseteq Y$
10		eqid	$⊢ {Base}_{U} = {Base}_{U}$
11	10 3	lssss	$⊢ X \in S \to X \subseteq {Base}_{U}$
12	6 11	syl	$⊢ φ \to X \subseteq {Base}_{U}$
13		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
14	1 13 2 10 4	dochcl	$⊢ ((K \in HL \land W \in H) \land X \subseteq {Base}_{U}) \to \underset{˙}{⊥} (X) \in ran DIsoH (K) (W)$
15	5 12 14	syl2anc	$⊢ φ \to \underset{˙}{⊥} (X) \in ran DIsoH (K) (W)$
16	1 13 4	dochoc	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \in ran DIsoH (K) (W)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) = \underset{˙}{⊥} (X)$
17	5 15 16	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) = \underset{˙}{⊥} (X)$
18	17	ineq1d	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) \cap Y = \underset{˙}{⊥} (X) \cap Y$
19	18	fveq2d	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) \cap Y) = \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap Y)$
20	19	ineq1d	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) \cap Y) \cap Y = \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap Y) \cap Y$
21	1 2 10 4	dochssv	$⊢ ((K \in HL \land W \in H) \land X \subseteq {Base}_{U}) \to \underset{˙}{⊥} (X) \subseteq {Base}_{U}$
22	5 12 21	syl2anc	$⊢ φ \to \underset{˙}{⊥} (X) \subseteq {Base}_{U}$
23	1 13 2 10 4	dochcl	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \subseteq {Base}_{U}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \in ran DIsoH (K) (W)$
24	5 22 23	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \in ran DIsoH (K) (W)$
25	10 3	lssss	$⊢ Y \in S \to Y \subseteq {Base}_{U}$
26	7 25	syl	$⊢ φ \to Y \subseteq {Base}_{U}$
27	1 13 2 10 4 5 26	dochoccl	$⊢ φ \to (Y \in ran DIsoH (K) (W) \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y)$
28	8 27	mpbird	$⊢ φ \to Y \in ran DIsoH (K) (W)$
29	1 2 10 4	dochss	$⊢ ((K \in HL \land W \in H) \land Y \subseteq {Base}_{U} \land X \subseteq Y) \to \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)$
30	5 26 9 29	syl3anc	$⊢ φ \to \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)$
31	1 2 10 4	dochss	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \subseteq {Base}_{U} \land \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Y))$
32	5 22 30 31	syl3anc	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Y))$
33	32 8	sseqtrd	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq Y$
34	1 13 4 5 24 28 33	dihoml4c	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) \cap Y) \cap Y = \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
35	20 34	eqtr3d	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap Y) \cap Y = \underset{˙}{⊥} (\underset{˙}{⊥} (X))$

Metamath Proof Explorer

Theorem dihoml4

Proof