Metamath Proof Explorer

Theorem lclkrlem2d

Description: Lemma for lclkr . (Contributed by NM, 16-Jan-2015)

Ref Expression
Hypotheses lclkrlem2a.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
lclkrlem2a.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
lclkrlem2a.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lclkrlem2a.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
lclkrlem2a.z ⊢ 0 = ( 0g ‘ 𝑈 )
lclkrlem2a.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
lclkrlem2a.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
lclkrlem2a.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
lclkrlem2a.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
lclkrlem2a.b ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑉 ∖ { 0 } ) )
lclkrlem2a.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
lclkrlem2a.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
lclkrlem2a.e ⊢ ( 𝜑 → ( ⊥ ‘ { 𝑋 } ) ≠ ( ⊥ ‘ { 𝑌 } ) )
lclkrlem2b.da ⊢ ( 𝜑 → ( ¬ 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ∨ ¬ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) )
lclkrlem2d.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
Assertion lclkrlem2d ( 𝜑 → ( ( ( ⊥ ‘ { 𝑋 } ) ∩ ( ⊥ ‘ { 𝑌 } ) ) ⊕ ( 𝑁 ‘ { 𝐵 } ) ) ∈ ran 𝐼 )

Proof

Step Hyp Ref Expression
1 lclkrlem2a.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 lclkrlem2a.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 lclkrlem2a.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 lclkrlem2a.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 lclkrlem2a.z ⊢ 0 = ( 0g ‘ 𝑈 )
6 lclkrlem2a.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
7 lclkrlem2a.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
8 lclkrlem2a.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
9 lclkrlem2a.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10 lclkrlem2a.b ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑉 ∖ { 0 } ) )
11 lclkrlem2a.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
12 lclkrlem2a.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
13 lclkrlem2a.e ⊢ ( 𝜑 → ( ⊥ ‘ { 𝑋 } ) ≠ ( ⊥ ‘ { 𝑌 } ) )
14 lclkrlem2b.da ⊢ ( 𝜑 → ( ¬ 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ∨ ¬ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) )
15 lclkrlem2d.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
16 11 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
17 16 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑉 )
18 1 15 3 4 2 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝑋 } ⊆ 𝑉 ) → ( ⊥ ‘ { 𝑋 } ) ∈ ran 𝐼 )
19 9 17 18 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ { 𝑋 } ) ∈ ran 𝐼 )
20 12 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
21 20 snssd ⊢ ( 𝜑 → { 𝑌 } ⊆ 𝑉 )
22 1 15 3 4 2 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝑌 } ⊆ 𝑉 ) → ( ⊥ ‘ { 𝑌 } ) ∈ ran 𝐼 )
23 9 21 22 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ { 𝑌 } ) ∈ ran 𝐼 )
24 1 15 dihmeetcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ⊥ ‘ { 𝑋 } ) ∈ ran 𝐼 ∧ ( ⊥ ‘ { 𝑌 } ) ∈ ran 𝐼 ) ) → ( ( ⊥ ‘ { 𝑋 } ) ∩ ( ⊥ ‘ { 𝑌 } ) ) ∈ ran 𝐼 )
25 9 19 23 24 syl12anc ⊢ ( 𝜑 → ( ( ⊥ ‘ { 𝑋 } ) ∩ ( ⊥ ‘ { 𝑌 } ) ) ∈ ran 𝐼 )
26 10 eldifad ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
27 1 3 4 6 7 15 9 25 26 dihsmsprn ⊢ ( 𝜑 → ( ( ( ⊥ ‘ { 𝑋 } ) ∩ ( ⊥ ‘ { 𝑌 } ) ) ⊕ ( 𝑁 ‘ { 𝐵 } ) ) ∈ ran 𝐼 )