Theorem dia2dimlem10

Description: Lemma for dia2dim . Convert membership in closed subspace ( I( U .\/ V ) ) to a lattice ordering. (Contributed by NM, 8-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dia2dimlem10.l	⊢ ≤ = ( le ‘ 𝐾 )
2		dia2dimlem10.j	⊢ ∨ = ( join ‘ 𝐾 )
3		dia2dimlem10.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		dia2dimlem10.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5		dia2dimlem10.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6		dia2dimlem10.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
7		dia2dimlem10.y	⊢ 𝑌 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
8		dia2dimlem10.s	⊢ 𝑆 = ( LSubSp ‘ 𝑌 )
9		dia2dimlem10.n	⊢ 𝑁 = ( LSpan ‘ 𝑌 )
10		dia2dimlem10.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
11		dia2dimlem10.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12		dia2dimlem10.u	⊢ ( 𝜑 → ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) )
13		dia2dimlem10.v	⊢ ( 𝜑 → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) )
14		dia2dimlem10.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑇 )
15		dia2dimlem10.fe	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) )
16	4 5 6 7 10 9	dia1dim2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) = ( 𝑁 ‘ { 𝐹 } ) )
17	11 14 16	syl2anc	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) = ( 𝑁 ‘ { 𝐹 } ) )
18	4 7	dvalvec	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑌 ∈ LVec )
19		lveclmod	⊢ ( 𝑌 ∈ LVec → 𝑌 ∈ LMod )
20	11 18 19	3syl	⊢ ( 𝜑 → 𝑌 ∈ LMod )
21	11	simpld	⊢ ( 𝜑 → 𝐾 ∈ HL )
22	12	simpld	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
23	13	simpld	⊢ ( 𝜑 → 𝑉 ∈ 𝐴 )
24		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
25	24 2 3	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) → ( 𝑈 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
26	21 22 23 25	syl3anc	⊢ ( 𝜑 → ( 𝑈 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
27	12	simprd	⊢ ( 𝜑 → 𝑈 ≤ 𝑊 )
28	13	simprd	⊢ ( 𝜑 → 𝑉 ≤ 𝑊 )
29	21	hllatd	⊢ ( 𝜑 → 𝐾 ∈ Lat )
30	24 3	atbase	⊢ ( 𝑈 ∈ 𝐴 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
31	22 30	syl	⊢ ( 𝜑 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
32	24 3	atbase	⊢ ( 𝑉 ∈ 𝐴 → 𝑉 ∈ ( Base ‘ 𝐾 ) )
33	23 32	syl	⊢ ( 𝜑 → 𝑉 ∈ ( Base ‘ 𝐾 ) )
34	11	simprd	⊢ ( 𝜑 → 𝑊 ∈ 𝐻 )
35	24 4	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
36	34 35	syl	⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
37	24 1 2	latjle12	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ 𝑉 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑈 ≤ 𝑊 ∧ 𝑉 ≤ 𝑊 ) ↔ ( 𝑈 ∨ 𝑉 ) ≤ 𝑊 ) )
38	29 31 33 36 37	syl13anc	⊢ ( 𝜑 → ( ( 𝑈 ≤ 𝑊 ∧ 𝑉 ≤ 𝑊 ) ↔ ( 𝑈 ∨ 𝑉 ) ≤ 𝑊 ) )
39	27 28 38	mpbi2and	⊢ ( 𝜑 → ( 𝑈 ∨ 𝑉 ) ≤ 𝑊 )
40	24 1 4 7 10 8	dialss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑈 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑈 ∨ 𝑉 ) ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) ∈ 𝑆 )
41	11 26 39 40	syl12anc	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) ∈ 𝑆 )
42	8 9 20 41 15	ellspsn5	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝐹 } ) ⊆ ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) )
43	17 42	eqsstrd	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) ⊆ ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) )
44	24 4 5 6	trlcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) )
45	11 14 44	syl2anc	⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) )
46	1 4 5 6	trlle	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ≤ 𝑊 )
47	11 14 46	syl2anc	⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≤ 𝑊 )
48	24 1 4 10	diaord	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) ≤ 𝑊 ) ∧ ( ( 𝑈 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑈 ∨ 𝑉 ) ≤ 𝑊 ) ) → ( ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) ⊆ ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) ↔ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑈 ∨ 𝑉 ) ) )
49	11 45 47 26 39 48	syl122anc	⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) ⊆ ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) ↔ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑈 ∨ 𝑉 ) ) )
50	43 49	mpbid	⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑈 ∨ 𝑉 ) )