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 ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochexmidlem1.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochexmidlem1.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochexmidlem1.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dochexmidlem1.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
dochexmidlem1.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
dochexmidlem1.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
dochexmidlem1.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
dochexmidlem1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dochexmidlem1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
dochexmidlem3.pp ⊢ ( 𝜑 → 𝑝 ∈ 𝐴 )
dochexmidlem3.qq ⊢ ( 𝜑 → 𝑞 ∈ 𝐴 )
dochexmidlem3.rr ⊢ ( 𝜑 → 𝑟 ∈ 𝐴 )
dochexmidlem3.ql ⊢ ( 𝜑 → 𝑞 ⊆ ( ⊥ ‘ 𝑋 ) )
dochexmidlem3.rl ⊢ ( 𝜑 → 𝑟 ⊆ 𝑋 )
dochexmidlem3.pl ⊢ ( 𝜑 → 𝑞 ⊆ ( 𝑟 ⊕ 𝑝 ) )
Assertion dochexmidlem3 ( 𝜑 → 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 dochexmidlem1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochexmidlem1.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 dochexmidlem1.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochexmidlem1.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 dochexmidlem1.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
6 dochexmidlem1.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
7 dochexmidlem1.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
8 dochexmidlem1.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
9 dochexmidlem1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10 dochexmidlem1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
11 dochexmidlem3.pp ⊢ ( 𝜑 → 𝑝 ∈ 𝐴 )
12 dochexmidlem3.qq ⊢ ( 𝜑 → 𝑞 ∈ 𝐴 )
13 dochexmidlem3.rr ⊢ ( 𝜑 → 𝑟 ∈ 𝐴 )
14 dochexmidlem3.ql ⊢ ( 𝜑 → 𝑞 ⊆ ( ⊥ ‘ 𝑋 ) )
15 dochexmidlem3.rl ⊢ ( 𝜑 → 𝑟 ⊆ 𝑋 )
16 dochexmidlem3.pl ⊢ ( 𝜑 → 𝑞 ⊆ ( 𝑟 ⊕ 𝑝 ) )
17 1 3 9 dvhlvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
18 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 dochexmidlem1 ⊢ ( 𝜑 → 𝑞 ≠ 𝑟 )
19 7 8 17 12 11 13 16 18 lsatexch1 ⊢ ( 𝜑 → 𝑝 ⊆ ( 𝑟 ⊕ 𝑞 ) )
20 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 19 dochexmidlem2 ⊢ ( 𝜑 → 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) )