dochdmj1

Description: De Morgan-like law for subspace orthocomplement. (Contributed by NM, 5-Aug-2014)

	Ref	Expression
Hypotheses	dochdmj1.h	$⊢ H = LHyp (K)$
	dochdmj1.u	$⊢ U = DVecH (K) (W)$
	dochdmj1.v	$⊢ V = {Base}_{U}$
	dochdmj1.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
Assertion	dochdmj1	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to \underset{˙}{⊥} (X \cup Y) = \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y)$

Proof

Step	Hyp	Ref	Expression
1		dochdmj1.h	$⊢ H = LHyp (K)$
2		dochdmj1.u	$⊢ U = DVecH (K) (W)$
3		dochdmj1.v	$⊢ V = {Base}_{U}$
4		dochdmj1.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
5		simp1	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to (K \in HL \land W \in H)$
6		simp2	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to X \subseteq V$
7		simp3	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to Y \subseteq V$
8	6 7	unssd	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to X \cup Y \subseteq V$
9		ssun1	$⊢ X \subseteq X \cup Y$
10	9	a1i	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to X \subseteq X \cup Y$
11	1 2 3 4	dochss	$⊢ ((K \in HL \land W \in H) \land X \cup Y \subseteq V \land X \subseteq X \cup Y) \to \underset{˙}{⊥} (X \cup Y) \subseteq \underset{˙}{⊥} (X)$
12	5 8 10 11	syl3anc	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to \underset{˙}{⊥} (X \cup Y) \subseteq \underset{˙}{⊥} (X)$
13		ssun2	$⊢ Y \subseteq X \cup Y$
14	13	a1i	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to Y \subseteq X \cup Y$
15	1 2 3 4	dochss	$⊢ ((K \in HL \land W \in H) \land X \cup Y \subseteq V \land Y \subseteq X \cup Y) \to \underset{˙}{⊥} (X \cup Y) \subseteq \underset{˙}{⊥} (Y)$
16	5 8 14 15	syl3anc	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to \underset{˙}{⊥} (X \cup Y) \subseteq \underset{˙}{⊥} (Y)$
17	12 16	ssind	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to \underset{˙}{⊥} (X \cup Y) \subseteq \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y)$
18		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
19	1 18 2 3 4	dochcl	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \underset{˙}{⊥} (X) \in ran DIsoH (K) (W)$
20	19	3adant3	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to \underset{˙}{⊥} (X) \in ran DIsoH (K) (W)$
21	1 18 2 3 4	dochcl	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V) \to \underset{˙}{⊥} (Y) \in ran DIsoH (K) (W)$
22	21	3adant2	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to \underset{˙}{⊥} (Y) \in ran DIsoH (K) (W)$
23	1 18	dihmeetcl	$⊢ ((K \in HL \land W \in H) \land (\underset{˙}{⊥} (X) \in ran DIsoH (K) (W) \land \underset{˙}{⊥} (Y) \in ran DIsoH (K) (W))) \to \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y) \in ran DIsoH (K) (W)$
24	5 20 22 23	syl12anc	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y) \in ran DIsoH (K) (W)$
25	1 18 4	dochoc	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y) \in ran DIsoH (K) (W)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y))) = \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y)$
26	5 24 25	syl2anc	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y))) = \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y)$
27	1 2 3 4	dochssv	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \underset{˙}{⊥} (X) \subseteq V$
28	27	3adant3	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to \underset{˙}{⊥} (X) \subseteq V$
29		ssinss1	$⊢ \underset{˙}{⊥} (X) \subseteq V \to \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y) \subseteq V$
30	28 29	syl	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y) \subseteq V$
31	1 2 3 4	dochssv	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y) \subseteq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y)) \subseteq V$
32	5 30 31	syl2anc	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y)) \subseteq V$
33	1 2 3 4	dochocss	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to X \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
34	33	3adant3	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to X \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
35	1 2 3 4	dochocss	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V) \to Y \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Y))$
36	35	3adant2	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to Y \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Y))$
37		unss12	$⊢ (X \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \land Y \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Y))) \to X \cup Y \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \cup \underset{˙}{⊥} (\underset{˙}{⊥} (Y))$
38	34 36 37	syl2anc	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to X \cup Y \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \cup \underset{˙}{⊥} (\underset{˙}{⊥} (Y))$
39		inss1	$⊢ \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)$
40	39	a1i	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)$
41	1 2 3 4	dochss	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \subseteq V \land \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y))$
42	5 28 40 41	syl3anc	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y))$
43	1 2 3 4	dochssv	$⊢ ((K \in HL \land W \in H) \land Y \subseteq V) \to \underset{˙}{⊥} (Y) \subseteq V$
44	43	3adant2	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to \underset{˙}{⊥} (Y) \subseteq V$
45		inss2	$⊢ \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (Y)$
46	45	a1i	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (Y)$
47	1 2 3 4	dochss	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (Y) \subseteq V \land \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (Y)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y))$
48	5 44 46 47	syl3anc	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y))$
49	42 48	unssd	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \cup \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y))$
50	38 49	sstrd	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to X \cup Y \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y))$
51	1 2 3 4	dochss	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y)) \subseteq V \land X \cup Y \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y))) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y))) \subseteq \underset{˙}{⊥} (X \cup Y)$
52	5 32 50 51	syl3anc	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y))) \subseteq \underset{˙}{⊥} (X \cup Y)$
53	26 52	eqsstrrd	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X \cup Y)$
54	17 53	eqssd	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to \underset{˙}{⊥} (X \cup Y) = \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y)$

Metamath Proof Explorer

Theorem dochdmj1

Proof