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

Metamath Proof Explorer

Theorem dia2dimlem8

Proof