This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dochexmid

Description: Excluded middle law for closed subspaces, which is equivalent to (and derived from) the orthomodular law dihoml4 . Lemma 3.3(2) in Holland95 p. 215. In our proof, we use the variables X , M , p , q , r in place of Hollands' l, m, P, Q, L respectively. ( pexmidALTN analog.) (Contributed by NM, 15-Jan-2015)

Ref Expression
Hypotheses dochexmid.h ⊢ H = LHyp ⁡ K
dochexmid.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
dochexmid.u ⊢ U = DVecH ⁡ K ⁡ W
dochexmid.v ⊢ V = Base U
dochexmid.s ⊢ S = LSubSp ⁡ U
dochexmid.p ⊢ ⊕ ˙ = LSSum ⁡ U
dochexmid.k ⊢ φ → K ∈ HL ∧ W ∈ H
dochexmid.x ⊢ φ → X ∈ S
dochexmid.c ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X
Assertion dochexmid ⊢ φ → X ⊕ ˙ ⊥ ˙ ⁡ X = V

Proof

Step Hyp Ref Expression
1 dochexmid.h ⊢ H = LHyp ⁡ K
2 dochexmid.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
3 dochexmid.u ⊢ U = DVecH ⁡ K ⁡ W
4 dochexmid.v ⊢ V = Base U
5 dochexmid.s ⊢ S = LSubSp ⁡ U
6 dochexmid.p ⊢ ⊕ ˙ = LSSum ⁡ U
7 dochexmid.k ⊢ φ → K ∈ HL ∧ W ∈ H
8 dochexmid.x ⊢ φ → X ∈ S
9 dochexmid.c ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X
10 id ⊢ X = 0 U → X = 0 U
11 fveq2 ⊢ X = 0 U → ⊥ ˙ ⁡ X = ⊥ ˙ ⁡ 0 U
12 10 11 oveq12d ⊢ X = 0 U → X ⊕ ˙ ⊥ ˙ ⁡ X = 0 U ⊕ ˙ ⊥ ˙ ⁡ 0 U
13 1 3 7 dvhlmod ⊢ φ → U ∈ LMod
14 eqid ⊢ 0 U = 0 U
15 4 14 lmod0vcl ⊢ U ∈ LMod → 0 U ∈ V
16 13 15 syl ⊢ φ → 0 U ∈ V
17 16 snssd ⊢ φ → 0 U ⊆ V
18 1 3 4 5 2 dochlss ⊢ K ∈ HL ∧ W ∈ H ∧ 0 U ⊆ V → ⊥ ˙ ⁡ 0 U ∈ S
19 7 17 18 syl2anc ⊢ φ → ⊥ ˙ ⁡ 0 U ∈ S
20 5 lsssubg ⊢ U ∈ LMod ∧ ⊥ ˙ ⁡ 0 U ∈ S → ⊥ ˙ ⁡ 0 U ∈ SubGrp ⁡ U
21 13 19 20 syl2anc ⊢ φ → ⊥ ˙ ⁡ 0 U ∈ SubGrp ⁡ U
22 14 6 lsm02 ⊢ ⊥ ˙ ⁡ 0 U ∈ SubGrp ⁡ U → 0 U ⊕ ˙ ⊥ ˙ ⁡ 0 U = ⊥ ˙ ⁡ 0 U
23 21 22 syl ⊢ φ → 0 U ⊕ ˙ ⊥ ˙ ⁡ 0 U = ⊥ ˙ ⁡ 0 U
24 1 3 2 4 14 doch0 ⊢ K ∈ HL ∧ W ∈ H → ⊥ ˙ ⁡ 0 U = V
25 7 24 syl ⊢ φ → ⊥ ˙ ⁡ 0 U = V
26 23 25 eqtrd ⊢ φ → 0 U ⊕ ˙ ⊥ ˙ ⁡ 0 U = V
27 12 26 sylan9eqr ⊢ φ ∧ X = 0 U → X ⊕ ˙ ⊥ ˙ ⁡ X = V
28 eqid ⊢ LSpan ⁡ U = LSpan ⁡ U
29 eqid ⊢ LSAtoms ⁡ U = LSAtoms ⁡ U
30 7 adantr ⊢ φ ∧ X ≠ 0 U → K ∈ HL ∧ W ∈ H
31 8 adantr ⊢ φ ∧ X ≠ 0 U → X ∈ S
32 simpr ⊢ φ ∧ X ≠ 0 U → X ≠ 0 U
33 9 adantr ⊢ φ ∧ X ≠ 0 U → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X
34 1 2 3 4 5 28 6 29 30 31 14 32 33 dochexmidlem8 ⊢ φ ∧ X ≠ 0 U → X ⊕ ˙ ⊥ ˙ ⁡ X = V
35 27 34 pm2.61dane ⊢ φ → X ⊕ ˙ ⊥ ˙ ⁡ X = V