Metamath Proof Explorer

Theorem dochexmidlem2

Description: Lemma for dochexmid . (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 ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
dochexmidlem2.pp ⊢ ( 𝜑 → 𝑝 ∈ 𝐴 )
dochexmidlem2.qq ⊢ ( 𝜑 → 𝑞 ∈ 𝐴 )
dochexmidlem2.rr ⊢ ( 𝜑 → 𝑟 ∈ 𝐴 )
dochexmidlem2.ql ⊢ ( 𝜑 → 𝑞 ⊆ ( ⊥ ‘ 𝑋 ) )
dochexmidlem2.rl ⊢ ( 𝜑 → 𝑟 ⊆ 𝑋 )
dochexmidlem2.pl ⊢ ( 𝜑 → 𝑝 ⊆ ( 𝑟 ⊕ 𝑞 ) )
Assertion dochexmidlem2 ( 𝜑 → 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) )

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 dochexmidlem2.pp ⊢ ( 𝜑 → 𝑝 ∈ 𝐴 )
12 dochexmidlem2.qq ⊢ ( 𝜑 → 𝑞 ∈ 𝐴 )
13 dochexmidlem2.rr ⊢ ( 𝜑 → 𝑟 ∈ 𝐴 )
14 dochexmidlem2.ql ⊢ ( 𝜑 → 𝑞 ⊆ ( ⊥ ‘ 𝑋 ) )
15 dochexmidlem2.rl ⊢ ( 𝜑 → 𝑟 ⊆ 𝑋 )
16 dochexmidlem2.pl ⊢ ( 𝜑 → 𝑝 ⊆ ( 𝑟 ⊕ 𝑞 ) )
17 1 3 9 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
18 5 lsssssubg ⊢ ( 𝑈 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑈 ) )
19 17 18 syl ⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝑈 ) )
20 19 10 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ( SubGrp ‘ 𝑈 ) )
21 4 5 lssss ⊢ ( 𝑋 ∈ 𝑆 → 𝑋 ⊆ 𝑉 )
22 10 21 syl ⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
23 1 3 4 5 2 dochlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝑆 )
24 9 22 23 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) ∈ 𝑆 )
25 19 24 sseldd ⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) ∈ ( SubGrp ‘ 𝑈 ) )
26 7 lsmless12 ⊢ ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑈 ) ∧ ( ⊥ ‘ 𝑋 ) ∈ ( SubGrp ‘ 𝑈 ) ) ∧ ( 𝑟 ⊆ 𝑋 ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑋 ) ) ) → ( 𝑟 ⊕ 𝑞 ) ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) )
27 20 25 15 14 26 syl22anc ⊢ ( 𝜑 → ( 𝑟 ⊕ 𝑞 ) ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) )
28 16 27 sstrd ⊢ ( 𝜑 → 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) )