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

Metamath Proof Explorer

Theorem dochexmidlem3

Description: Lemma for dochexmid . Use atom exchange lsatexch1 to swap p and q . (Contributed by NM, 14-Jan-2015)

Ref Expression
Hypotheses dochexmidlem1.h ⊢ H = LHyp ⁡ K
dochexmidlem1.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
dochexmidlem1.u ⊢ U = DVecH ⁡ K ⁡ W
dochexmidlem1.v ⊢ V = Base U
dochexmidlem1.s ⊢ S = LSubSp ⁡ U
dochexmidlem1.n ⊢ N = LSpan ⁡ U
dochexmidlem1.p ⊢ ⊕ ˙ = LSSum ⁡ U
dochexmidlem1.a ⊢ A = LSAtoms ⁡ U
dochexmidlem1.k ⊢ φ → K ∈ HL ∧ W ∈ H
dochexmidlem1.x ⊢ φ → X ∈ S
dochexmidlem3.pp ⊢ φ → p ∈ A
dochexmidlem3.qq ⊢ φ → q ∈ A
dochexmidlem3.rr ⊢ φ → r ∈ A
dochexmidlem3.ql ⊢ φ → q ⊆ ⊥ ˙ ⁡ X
dochexmidlem3.rl ⊢ φ → r ⊆ X
dochexmidlem3.pl ⊢ φ → q ⊆ r ⊕ ˙ p
Assertion dochexmidlem3 ⊢ φ → p ⊆ X ⊕ ˙ ⊥ ˙ ⁡ X

Proof

Step Hyp Ref Expression
1 dochexmidlem1.h ⊢ H = LHyp ⁡ K
2 dochexmidlem1.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
3 dochexmidlem1.u ⊢ U = DVecH ⁡ K ⁡ W
4 dochexmidlem1.v ⊢ V = Base U
5 dochexmidlem1.s ⊢ S = LSubSp ⁡ U
6 dochexmidlem1.n ⊢ N = LSpan ⁡ U
7 dochexmidlem1.p ⊢ ⊕ ˙ = LSSum ⁡ U
8 dochexmidlem1.a ⊢ A = LSAtoms ⁡ U
9 dochexmidlem1.k ⊢ φ → K ∈ HL ∧ W ∈ H
10 dochexmidlem1.x ⊢ φ → X ∈ S
11 dochexmidlem3.pp ⊢ φ → p ∈ A
12 dochexmidlem3.qq ⊢ φ → q ∈ A
13 dochexmidlem3.rr ⊢ φ → r ∈ A
14 dochexmidlem3.ql ⊢ φ → q ⊆ ⊥ ˙ ⁡ X
15 dochexmidlem3.rl ⊢ φ → r ⊆ X
16 dochexmidlem3.pl ⊢ φ → q ⊆ r ⊕ ˙ p
17 1 3 9 dvhlvec ⊢ φ → U ∈ LVec
18 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 dochexmidlem1 ⊢ φ → q ≠ r
19 7 8 17 12 11 13 16 18 lsatexch1 ⊢ φ → p ⊆ r ⊕ ˙ q
20 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 19 dochexmidlem2 ⊢ φ → p ⊆ X ⊕ ˙ ⊥ ˙ ⁡ X