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 ( 𝜑𝐹 ∈ ( ( 𝐼𝑈 ) ( 𝐼𝑉 ) ) )