Metamath Proof Explorer

Theorem dia2dimlem6

Description: Lemma for dia2dim . Eliminate auxiliary translations G and D . (Contributed by NM, 8-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 dia2dimlem6.l ⊢ ≤ = ( le ‘ 𝐾 )
2 dia2dimlem6.j ⊢ ∨ = ( join ‘ 𝐾 )
3 dia2dimlem6.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 dia2dimlem6.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 dia2dimlem6.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 dia2dimlem6.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7 dia2dimlem6.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
8 dia2dimlem6.y ⊢ 𝑌 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
9 dia2dimlem6.s ⊢ 𝑆 = ( LSubSp ‘ 𝑌 )
10 dia2dimlem6.pl ⊢ ⊕ = ( LSSum ‘ 𝑌 )
11 dia2dimlem6.n ⊢ 𝑁 = ( LSpan ‘ 𝑌 )
12 dia2dimlem6.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
13 dia2dimlem6.q ⊢ 𝑄 = ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) )
14 dia2dimlem6.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
15 dia2dimlem6.u ⊢ ( 𝜑 → ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) )
16 dia2dimlem6.v ⊢ ( 𝜑 → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) )
17 dia2dimlem6.p ⊢ ( 𝜑 → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
18 dia2dimlem6.f ⊢ ( 𝜑 → ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) )
19 dia2dimlem6.rf ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑈 ∨ 𝑉 ) )
20 dia2dimlem6.uv ⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
21 dia2dimlem6.ru ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≠ 𝑈 )
22 dia2dimlem6.rv ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≠ 𝑉 )
23 1 2 3 4 5 6 7 13 14 15 16 17 18 19 20 21 dia2dimlem1 ⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
24 18 simpld ⊢ ( 𝜑 → 𝐹 ∈ 𝑇 )
25 1 4 5 6 ltrnel ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑃 ) ≤ 𝑊 ) )
26 14 24 17 25 syl3anc ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑃 ) ≤ 𝑊 ) )
27 1 4 5 6 cdleme50ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑃 ) ≤ 𝑊 ) ) → ∃ 𝑑 ∈ 𝑇 ( 𝑑 ‘ 𝑄 ) = ( 𝐹 ‘ 𝑃 ) )
28 14 23 26 27 syl3anc ⊢ ( 𝜑 → ∃ 𝑑 ∈ 𝑇 ( 𝑑 ‘ 𝑄 ) = ( 𝐹 ‘ 𝑃 ) )
29 1 4 5 6 cdleme50ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ∃ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 )
30 14 17 23 29 syl3anc ⊢ ( 𝜑 → ∃ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 )
31 14 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑔 ‘ 𝑃 ) = 𝑄 ∧ 𝑑 ∈ 𝑇 ) ∧ ( 𝑑 ‘ 𝑄 ) = ( 𝐹 ‘ 𝑃 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
32 15 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑔 ‘ 𝑃 ) = 𝑄 ∧ 𝑑 ∈ 𝑇 ) ∧ ( 𝑑 ‘ 𝑄 ) = ( 𝐹 ‘ 𝑃 ) ) → ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) )
33 16 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑔 ‘ 𝑃 ) = 𝑄 ∧ 𝑑 ∈ 𝑇 ) ∧ ( 𝑑 ‘ 𝑄 ) = ( 𝐹 ‘ 𝑃 ) ) → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) )
34 17 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑔 ‘ 𝑃 ) = 𝑄 ∧ 𝑑 ∈ 𝑇 ) ∧ ( 𝑑 ‘ 𝑄 ) = ( 𝐹 ‘ 𝑃 ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
35 18 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑔 ‘ 𝑃 ) = 𝑄 ∧ 𝑑 ∈ 𝑇 ) ∧ ( 𝑑 ‘ 𝑄 ) = ( 𝐹 ‘ 𝑃 ) ) → ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) )
36 19 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑔 ‘ 𝑃 ) = 𝑄 ∧ 𝑑 ∈ 𝑇 ) ∧ ( 𝑑 ‘ 𝑄 ) = ( 𝐹 ‘ 𝑃 ) ) → ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑈 ∨ 𝑉 ) )
37 20 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑔 ‘ 𝑃 ) = 𝑄 ∧ 𝑑 ∈ 𝑇 ) ∧ ( 𝑑 ‘ 𝑄 ) = ( 𝐹 ‘ 𝑃 ) ) → 𝑈 ≠ 𝑉 )
38 21 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑔 ‘ 𝑃 ) = 𝑄 ∧ 𝑑 ∈ 𝑇 ) ∧ ( 𝑑 ‘ 𝑄 ) = ( 𝐹 ‘ 𝑃 ) ) → ( 𝑅 ‘ 𝐹 ) ≠ 𝑈 )
39 22 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑔 ‘ 𝑃 ) = 𝑄 ∧ 𝑑 ∈ 𝑇 ) ∧ ( 𝑑 ‘ 𝑄 ) = ( 𝐹 ‘ 𝑃 ) ) → ( 𝑅 ‘ 𝐹 ) ≠ 𝑉 )
40 simp21 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑔 ‘ 𝑃 ) = 𝑄 ∧ 𝑑 ∈ 𝑇 ) ∧ ( 𝑑 ‘ 𝑄 ) = ( 𝐹 ‘ 𝑃 ) ) → 𝑔 ∈ 𝑇 )
41 simp22 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑔 ‘ 𝑃 ) = 𝑄 ∧ 𝑑 ∈ 𝑇 ) ∧ ( 𝑑 ‘ 𝑄 ) = ( 𝐹 ‘ 𝑃 ) ) → ( 𝑔 ‘ 𝑃 ) = 𝑄 )
42 simp23 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑔 ‘ 𝑃 ) = 𝑄 ∧ 𝑑 ∈ 𝑇 ) ∧ ( 𝑑 ‘ 𝑄 ) = ( 𝐹 ‘ 𝑃 ) ) → 𝑑 ∈ 𝑇 )
43 simp3 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑔 ‘ 𝑃 ) = 𝑄 ∧ 𝑑 ∈ 𝑇 ) ∧ ( 𝑑 ‘ 𝑄 ) = ( 𝐹 ‘ 𝑃 ) ) → ( 𝑑 ‘ 𝑄 ) = ( 𝐹 ‘ 𝑃 ) )
44 1 2 3 4 5 6 7 8 9 10 11 12 13 31 32 33 34 35 36 37 38 39 40 41 42 43 dia2dimlem5 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑔 ‘ 𝑃 ) = 𝑄 ∧ 𝑑 ∈ 𝑇 ) ∧ ( 𝑑 ‘ 𝑄 ) = ( 𝐹 ‘ 𝑃 ) ) → 𝐹 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )
45 44 3exp ⊢ ( 𝜑 → ( ( 𝑔 ∈ 𝑇 ∧ ( 𝑔 ‘ 𝑃 ) = 𝑄 ∧ 𝑑 ∈ 𝑇 ) → ( ( 𝑑 ‘ 𝑄 ) = ( 𝐹 ‘ 𝑃 ) → 𝐹 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) ) ) )
46 45 3expd ⊢ ( 𝜑 → ( 𝑔 ∈ 𝑇 → ( ( 𝑔 ‘ 𝑃 ) = 𝑄 → ( 𝑑 ∈ 𝑇 → ( ( 𝑑 ‘ 𝑄 ) = ( 𝐹 ‘ 𝑃 ) → 𝐹 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) ) ) ) ) )
47 46 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 → ( 𝑑 ∈ 𝑇 → ( ( 𝑑 ‘ 𝑄 ) = ( 𝐹 ‘ 𝑃 ) → 𝐹 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) ) ) ) )
48 30 47 mpd ⊢ ( 𝜑 → ( 𝑑 ∈ 𝑇 → ( ( 𝑑 ‘ 𝑄 ) = ( 𝐹 ‘ 𝑃 ) → 𝐹 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) ) ) )
49 48 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑑 ∈ 𝑇 ( 𝑑 ‘ 𝑄 ) = ( 𝐹 ‘ 𝑃 ) → 𝐹 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) ) )
50 28 49 mpd ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )