Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lclkrlem2d Structured version   Visualization version   GIF version

Theorem lclkrlem2d 37116
 Description: Lemma for lclkr 37139. (Contributed by NM, 16-Jan-2015.)
Hypotheses
Ref Expression
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
Ref Expression
lclkrlem2d (𝜑 → ((( ‘{𝑋}) ∩ ( ‘{𝑌})) (𝑁‘{𝐵})) ∈ ran 𝐼)

Proof of Theorem lclkrlem2d
StepHypRef Expression
1 lclkrlem2a.h . 2 𝐻 = (LHyp‘𝐾)
2 lclkrlem2a.u . 2 𝑈 = ((DVecH‘𝐾)‘𝑊)
3 lclkrlem2a.v . 2 𝑉 = (Base‘𝑈)
4 lclkrlem2a.p . 2 = (LSSum‘𝑈)
5 lclkrlem2a.n . 2 𝑁 = (LSpan‘𝑈)
6 lclkrlem2d.i . 2 𝐼 = ((DIsoH‘𝐾)‘𝑊)
7 lclkrlem2a.k . 2 (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
8 lclkrlem2a.x . . . . . 6 (𝜑𝑋 ∈ (𝑉 ∖ { 0 }))
98eldifad 3619 . . . . 5 (𝜑𝑋𝑉)
109snssd 4372 . . . 4 (𝜑 → {𝑋} ⊆ 𝑉)
11 lclkrlem2a.o . . . . 5 = ((ocH‘𝐾)‘𝑊)
121, 6, 2, 3, 11dochcl 36959 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ {𝑋} ⊆ 𝑉) → ( ‘{𝑋}) ∈ ran 𝐼)
137, 10, 12syl2anc 694 . . 3 (𝜑 → ( ‘{𝑋}) ∈ ran 𝐼)
14 lclkrlem2a.y . . . . . 6 (𝜑𝑌 ∈ (𝑉 ∖ { 0 }))
1514eldifad 3619 . . . . 5 (𝜑𝑌𝑉)
1615snssd 4372 . . . 4 (𝜑 → {𝑌} ⊆ 𝑉)
171, 6, 2, 3, 11dochcl 36959 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ {𝑌} ⊆ 𝑉) → ( ‘{𝑌}) ∈ ran 𝐼)
187, 16, 17syl2anc 694 . . 3 (𝜑 → ( ‘{𝑌}) ∈ ran 𝐼)
191, 6dihmeetcl 36951 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (( ‘{𝑋}) ∈ ran 𝐼 ∧ ( ‘{𝑌}) ∈ ran 𝐼)) → (( ‘{𝑋}) ∩ ( ‘{𝑌})) ∈ ran 𝐼)
207, 13, 18, 19syl12anc 1364 . 2 (𝜑 → (( ‘{𝑋}) ∩ ( ‘{𝑌})) ∈ ran 𝐼)
21 lclkrlem2a.b . . 3 (𝜑𝐵 ∈ (𝑉 ∖ { 0 }))