Metamath Proof Explorer

Theorem 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 ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
djhexmid.j ⊢ ∨ ˙ = joinH ⁡ K ⁡ W
Assertion djhexmid ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → X ∨ ˙ ⊥ ˙ ⁡ 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 ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
5 djhexmid.j ⊢ ∨ ˙ = joinH ⁡ K ⁡ W
6 simpl ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → K ∈ HL ∧ W ∈ H
7 simpr ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → X ⊆ V
8 1 2 3 4 dochssv ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X ⊆ V
9 1 2 3 4 5 djhval ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V ∧ ⊥ ˙ ⁡ X ⊆ V → X ∨ ˙ ⊥ ˙ ⁡ X = ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X
10 6 7 8 9 syl12anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → X ∨ ˙ ⊥ ˙ ⁡ X = ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X
11 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
12 1 2 3 11 4 dochlss ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X ∈ LSubSp ⁡ U
13 eqid ⊢ 0 U = 0 U
14 1 2 11 13 4 dochnoncon ⊢ K ∈ HL ∧ W ∈ H ∧ ⊥ ˙ ⁡ X ∈ LSubSp ⁡ U → ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = 0 U
15 12 14 syldan ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = 0 U
16 1 2 4 3 13 doch1 ⊢ K ∈ HL ∧ W ∈ H → ⊥ ˙ ⁡ V = 0 U
17 16 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ V = 0 U
18 15 17 eqtr4d ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = ⊥ ˙ ⁡ V
19 18 fveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = ⊥ ˙ ⁡ ⊥ ˙ ⁡ V
20 eqid ⊢ DIsoH ⁡ K ⁡ W = DIsoH ⁡ K ⁡ W
21 1 20 2 3 dih1rn ⊢ K ∈ HL ∧ W ∈ H → V ∈ ran ⁡ DIsoH ⁡ K ⁡ W
22 21 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → V ∈ ran ⁡ DIsoH ⁡ K ⁡ W
23 1 20 4 dochoc ⊢ K ∈ HL ∧ W ∈ H ∧ V ∈ ran ⁡ DIsoH ⁡ K ⁡ W → ⊥ ˙ ⁡ ⊥ ˙ ⁡ V = V
24 22 23 syldan ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ V = V
25 10 19 24 3eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → X ∨ ˙ ⊥ ˙ ⁡ X = V