Theorem dia2dimlem11

Description: Lemma for dia2dim . Convert ordering hypothesis on RF to subspace membership F e. ( I( U .\/ V ) ) . (Contributed by NM, 8-Sep-2014)

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

Proof

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