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

Metamath Proof Explorer

Theorem dia2dimlem6

Proof