Metamath Proof Explorer

Theorem dia2dimlem8

Description: Lemma for dia2dim . Eliminate no-longer used auxiliary atoms P and Q . (Contributed by NM, 8-Sep-2014)

Ref Expression
Hypotheses dia2dimlem8.l ⊢ ≤ = ( le ‘ 𝐾 )
dia2dimlem8.j ⊢ ∨ = ( join ‘ 𝐾 )
dia2dimlem8.m ⊢ ∧ = ( meet ‘ 𝐾 )
dia2dimlem8.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dia2dimlem8.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dia2dimlem8.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dia2dimlem8.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
dia2dimlem8.y ⊢ 𝑌 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
dia2dimlem8.s ⊢ 𝑆 = ( LSubSp ‘ 𝑌 )
dia2dimlem8.pl ⊢ ⊕ = ( LSSum ‘ 𝑌 )
dia2dimlem8.n ⊢ 𝑁 = ( LSpan ‘ 𝑌 )
dia2dimlem8.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
dia2dimlem8.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dia2dimlem8.u ⊢ ( 𝜑 → ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) )
dia2dimlem8.v ⊢ ( 𝜑 → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) )
dia2dimlem8.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑇 )
dia2dimlem8.rf ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑈 ∨ 𝑉 ) )
dia2dimlem8.uv ⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
dia2dimlem8.ru ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≠ 𝑈 )
dia2dimlem8.rv ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≠ 𝑉 )
Assertion dia2dimlem8 ( 𝜑 → 𝐹 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )

Proof

Step Hyp Ref Expression
1 dia2dimlem8.l ⊢ ≤ = ( le ‘ 𝐾 )
2 dia2dimlem8.j ⊢ ∨ = ( join ‘ 𝐾 )
3 dia2dimlem8.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 dia2dimlem8.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 dia2dimlem8.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 dia2dimlem8.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7 dia2dimlem8.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
8 dia2dimlem8.y ⊢ 𝑌 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
9 dia2dimlem8.s ⊢ 𝑆 = ( LSubSp ‘ 𝑌 )
10 dia2dimlem8.pl ⊢ ⊕ = ( LSSum ‘ 𝑌 )
11 dia2dimlem8.n ⊢ 𝑁 = ( LSpan ‘ 𝑌 )
12 dia2dimlem8.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
13 dia2dimlem8.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
14 dia2dimlem8.u ⊢ ( 𝜑 → ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) )
15 dia2dimlem8.v ⊢ ( 𝜑 → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) )
16 dia2dimlem8.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑇 )
17 dia2dimlem8.rf ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑈 ∨ 𝑉 ) )
18 dia2dimlem8.uv ⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
19 dia2dimlem8.ru ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≠ 𝑈 )
20 dia2dimlem8.rv ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≠ 𝑉 )
21 eqid ⊢ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∨ 𝑈 ) ∧ ( ( 𝐹 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ∨ 𝑉 ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∨ 𝑈 ) ∧ ( ( 𝐹 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ∨ 𝑉 ) )
22 eqid ⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
23 1 22 4 5 lhpocnel ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐴 ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ≤ 𝑊 ) )
24 13 23 syl ⊢ ( 𝜑 → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐴 ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ≤ 𝑊 ) )
25 1 2 3 4 5 6 7 8 9 10 11 12 21 13 14 15 24 16 17 18 19 20 dia2dimlem7 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )