Metamath Proof Explorer


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 lspsnel5a ( 𝜑 → ( 𝑁 ‘ { 𝐹 } ) ⊆ ( 𝐼 ‘ ( 𝑈 𝑉 ) ) )
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 ( 𝜑 → ( 𝑅𝐹 ) ( 𝑈 𝑉 ) )