dochpolN

Description: The subspace orthocomplement for the DVecH vector space is a polarity. (Contributed by NM, 27-Dec-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dochpol.h	$⊢ H = LHyp (K)$
	dochpol.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	dochpol.u	$⊢ U = DVecH (K) (W)$
	dochpol.p	$⊢ P = LPol (U)$
	dochpol.k	$⊢ φ \to (K \in HL \land W \in H)$
Assertion	dochpolN	$⊢ φ \to \underset{˙}{⊥} \in P$

Proof

Step	Hyp	Ref	Expression
1		dochpol.h	$⊢ H = LHyp (K)$
2		dochpol.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		dochpol.u	$⊢ U = DVecH (K) (W)$
4		dochpol.p	$⊢ P = LPol (U)$
5		dochpol.k	$⊢ φ \to (K \in HL \land W \in H)$
6		eqid	$⊢ {Base}_{U} = {Base}_{U}$
7		eqid	$⊢ LSubSp (U) = LSubSp (U)$
8		eqid	$⊢ 0_{U} = 0_{U}$
9		eqid	$⊢ LSAtoms (U) = LSAtoms (U)$
10		eqid	$⊢ LSHyp (U) = LSHyp (U)$
11	3	fvexi	$⊢ U \in V$
12	11	a1i	$⊢ φ \to U \in V$
13		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
14	1 13 3 6 2 5	dochfN	$⊢ φ \to \underset{˙}{⊥} : 𝒫 {Base}_{U} ⟶ ran DIsoH (K) (W)$
15	1 3 13 7	dihsslss	$⊢ (K \in HL \land W \in H) \to ran DIsoH (K) (W) \subseteq LSubSp (U)$
16	5 15	syl	$⊢ φ \to ran DIsoH (K) (W) \subseteq LSubSp (U)$
17	14 16	fssd	$⊢ φ \to \underset{˙}{⊥} : 𝒫 {Base}_{U} ⟶ LSubSp (U)$
18	1 3 2 6 8	doch1	$⊢ (K \in HL \land W \in H) \to \underset{˙}{⊥} ({Base}_{U}) = \{0_{U}\}$
19	5 18	syl	$⊢ φ \to \underset{˙}{⊥} ({Base}_{U}) = \{0_{U}\}$
20	5	adantr	$⊢ (φ \land (x \subseteq {Base}_{U} \land y \subseteq {Base}_{U} \land x \subseteq y)) \to (K \in HL \land W \in H)$
21		simpr2	$⊢ (φ \land (x \subseteq {Base}_{U} \land y \subseteq {Base}_{U} \land x \subseteq y)) \to y \subseteq {Base}_{U}$
22		simpr3	$⊢ (φ \land (x \subseteq {Base}_{U} \land y \subseteq {Base}_{U} \land x \subseteq y)) \to x \subseteq y$
23	1 3 6 2	dochss	$⊢ ((K \in HL \land W \in H) \land y \subseteq {Base}_{U} \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)$
24	20 21 22 23	syl3anc	$⊢ (φ \land (x \subseteq {Base}_{U} \land y \subseteq {Base}_{U} \land x \subseteq y)) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)$
25	5	adantr	$⊢ (φ \land x \in LSAtoms (U)) \to (K \in HL \land W \in H)$
26		simpr	$⊢ (φ \land x \in LSAtoms (U)) \to x \in LSAtoms (U)$
27	1 3 2 9 10 25 26	dochsatshp	$⊢ (φ \land x \in LSAtoms (U)) \to \underset{˙}{⊥} (x) \in LSHyp (U)$
28	1 3 13 9	dih1dimat	$⊢ ((K \in HL \land W \in H) \land x \in LSAtoms (U)) \to x \in ran DIsoH (K) (W)$
29	25 26 28	syl2anc	$⊢ (φ \land x \in LSAtoms (U)) \to x \in ran DIsoH (K) (W)$
30	1 13 2	dochoc	$⊢ ((K \in HL \land W \in H) \land x \in ran DIsoH (K) (W)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x$
31	25 29 30	syl2anc	$⊢ (φ \land x \in LSAtoms (U)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x$
32	6 7 8 9 10 4 12 17 19 24 27 31	islpoldN	$⊢ φ \to \underset{˙}{⊥} \in P$

Metamath Proof Explorer

Theorem dochpolN

Proof