djhexmid

Description: Excluded middle property of DVecH vector space closed subspace join. (Contributed by NM, 22-Jul-2014)

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

Proof

Step	Hyp	Ref	Expression
1		djhexmid.h	$⊢ H = LHyp (K)$
2		djhexmid.u	$⊢ U = DVecH (K) (W)$
3		djhexmid.v	$⊢ V = {Base}_{U}$
4		djhexmid.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
5		djhexmid.j	$⊢ \underset{˙}{\lor} = joinH (K) (W)$
6		simpl	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to (K \in HL \land W \in H)$
7		simpr	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to X \subseteq V$
8	1 2 3 4	dochssv	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \underset{˙}{⊥} (X) \subseteq V$
9	1 2 3 4 5	djhval	$⊢ ((K \in HL \land W \in H) \land (X \subseteq V \land \underset{˙}{⊥} (X) \subseteq V)) \to X \underset{˙}{\lor} \underset{˙}{⊥} (X) = \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (\underset{˙}{⊥} (X)))$
10	6 7 8 9	syl12anc	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to X \underset{˙}{\lor} \underset{˙}{⊥} (X) = \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (\underset{˙}{⊥} (X)))$
11		eqid	$⊢ LSubSp (U) = LSubSp (U)$
12	1 2 3 11 4	dochlss	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \underset{˙}{⊥} (X) \in LSubSp (U)$
13		eqid	$⊢ 0_{U} = 0_{U}$
14	1 2 11 13 4	dochnoncon	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \in LSubSp (U)) \to \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = \{0_{U}\}$
15	12 14	syldan	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = \{0_{U}\}$
16	1 2 4 3 13	doch1	$⊢ (K \in HL \land W \in H) \to \underset{˙}{⊥} (V) = \{0_{U}\}$
17	16	adantr	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \underset{˙}{⊥} (V) = \{0_{U}\}$
18	15 17	eqtr4d	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = \underset{˙}{⊥} (V)$
19	18	fveq2d	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (\underset{˙}{⊥} (X))) = \underset{˙}{⊥} (\underset{˙}{⊥} (V))$
20		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
21	1 20 2 3	dih1rn	$⊢ (K \in HL \land W \in H) \to V \in ran DIsoH (K) (W)$
22	21	adantr	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to V \in ran DIsoH (K) (W)$
23	1 20 4	dochoc	$⊢ ((K \in HL \land W \in H) \land V \in ran DIsoH (K) (W)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (V)) = V$
24	22 23	syldan	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (V)) = V$
25	10 19 24	3eqtrd	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to X \underset{˙}{\lor} \underset{˙}{⊥} (X) = V$

Metamath Proof Explorer

Theorem djhexmid

Proof