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

Metamath Proof Explorer

Theorem dochexmidlem2

Description: Lemma for dochexmid . (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
dochexmidlem2.pp ⊢ φ → p ∈ A
dochexmidlem2.qq ⊢ φ → q ∈ A
dochexmidlem2.rr ⊢ φ → r ∈ A
dochexmidlem2.ql ⊢ φ → q ⊆ ⊥ ˙ ⁡ X
dochexmidlem2.rl ⊢ φ → r ⊆ X
dochexmidlem2.pl ⊢ φ → p ⊆ r ⊕ ˙ q
Assertion dochexmidlem2 ⊢ φ → 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 dochexmidlem2.pp ⊢ φ → p ∈ A
12 dochexmidlem2.qq ⊢ φ → q ∈ A
13 dochexmidlem2.rr ⊢ φ → r ∈ A
14 dochexmidlem2.ql ⊢ φ → q ⊆ ⊥ ˙ ⁡ X
15 dochexmidlem2.rl ⊢ φ → r ⊆ X
16 dochexmidlem2.pl ⊢ φ → p ⊆ r ⊕ ˙ q
17 1 3 9 dvhlmod ⊢ φ → U ∈ LMod
18 5 lsssssubg ⊢ U ∈ LMod → S ⊆ SubGrp ⁡ U
19 17 18 syl ⊢ φ → S ⊆ SubGrp ⁡ U
20 19 10 sseldd ⊢ φ → X ∈ SubGrp ⁡ U
21 4 5 lssss ⊢ X ∈ S → X ⊆ V
22 10 21 syl ⊢ φ → X ⊆ V
23 1 3 4 5 2 dochlss ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X ∈ S
24 9 22 23 syl2anc ⊢ φ → ⊥ ˙ ⁡ X ∈ S
25 19 24 sseldd ⊢ φ → ⊥ ˙ ⁡ X ∈ SubGrp ⁡ U
26 7 lsmless12 ⊢ X ∈ SubGrp ⁡ U ∧ ⊥ ˙ ⁡ X ∈ SubGrp ⁡ U ∧ r ⊆ X ∧ q ⊆ ⊥ ˙ ⁡ X → r ⊕ ˙ q ⊆ X ⊕ ˙ ⊥ ˙ ⁡ X
27 20 25 15 14 26 syl22anc ⊢ φ → r ⊕ ˙ q ⊆ X ⊕ ˙ ⊥ ˙ ⁡ X
28 16 27 sstrd ⊢ φ → p ⊆ X ⊕ ˙ ⊥ ˙ ⁡ X