Metamath Proof Explorer


Theorem dia2dimlem13

Description: Lemma for dia2dim . Eliminate U =/= V condition. (Contributed by NM, 8-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 dia2dimlem12.l = ( le ‘ 𝐾 )
2 dia2dimlem12.j = ( join ‘ 𝐾 )
3 dia2dimlem12.m = ( meet ‘ 𝐾 )
4 dia2dimlem12.a 𝐴 = ( Atoms ‘ 𝐾 )
5 dia2dimlem12.h 𝐻 = ( LHyp ‘ 𝐾 )
6 dia2dimlem12.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7 dia2dimlem12.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
8 dia2dimlem12.y 𝑌 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
9 dia2dimlem12.s 𝑆 = ( LSubSp ‘ 𝑌 )
10 dia2dimlem12.pl = ( LSSum ‘ 𝑌 )
11 dia2dimlem12.n 𝑁 = ( LSpan ‘ 𝑌 )
12 dia2dimlem12.i 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
13 dia2dimlem12.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
14 dia2dimlem12.u ( 𝜑 → ( 𝑈𝐴𝑈 𝑊 ) )
15 dia2dimlem12.v ( 𝜑 → ( 𝑉𝐴𝑉 𝑊 ) )
16 oveq2 ( 𝑈 = 𝑉 → ( 𝑈 𝑈 ) = ( 𝑈 𝑉 ) )
17 16 adantl ( ( 𝜑𝑈 = 𝑉 ) → ( 𝑈 𝑈 ) = ( 𝑈 𝑉 ) )
18 13 simpld ( 𝜑𝐾 ∈ HL )
19 14 simpld ( 𝜑𝑈𝐴 )
20 2 4 hlatjidm ( ( 𝐾 ∈ HL ∧ 𝑈𝐴 ) → ( 𝑈 𝑈 ) = 𝑈 )
21 18 19 20 syl2anc ( 𝜑 → ( 𝑈 𝑈 ) = 𝑈 )
22 21 adantr ( ( 𝜑𝑈 = 𝑉 ) → ( 𝑈 𝑈 ) = 𝑈 )
23 17 22 eqtr3d ( ( 𝜑𝑈 = 𝑉 ) → ( 𝑈 𝑉 ) = 𝑈 )
24 23 fveq2d ( ( 𝜑𝑈 = 𝑉 ) → ( 𝐼 ‘ ( 𝑈 𝑉 ) ) = ( 𝐼𝑈 ) )
25 ssid ( 𝐼𝑈 ) ⊆ ( 𝐼𝑈 )
26 24 25 eqsstrdi ( ( 𝜑𝑈 = 𝑉 ) → ( 𝐼 ‘ ( 𝑈 𝑉 ) ) ⊆ ( 𝐼𝑈 ) )
27 5 8 dvalvec ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑌 ∈ LVec )
28 lveclmod ( 𝑌 ∈ LVec → 𝑌 ∈ LMod )
29 13 27 28 3syl ( 𝜑𝑌 ∈ LMod )
30 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
31 30 4 atbase ( 𝑈𝐴𝑈 ∈ ( Base ‘ 𝐾 ) )
32 19 31 syl ( 𝜑𝑈 ∈ ( Base ‘ 𝐾 ) )
33 14 simprd ( 𝜑𝑈 𝑊 )
34 30 1 5 8 12 9 dialss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 𝑊 ) ) → ( 𝐼𝑈 ) ∈ 𝑆 )
35 13 32 33 34 syl12anc ( 𝜑 → ( 𝐼𝑈 ) ∈ 𝑆 )
36 9 lsssubg ( ( 𝑌 ∈ LMod ∧ ( 𝐼𝑈 ) ∈ 𝑆 ) → ( 𝐼𝑈 ) ∈ ( SubGrp ‘ 𝑌 ) )
37 29 35 36 syl2anc ( 𝜑 → ( 𝐼𝑈 ) ∈ ( SubGrp ‘ 𝑌 ) )
38 10 lsmidm ( ( 𝐼𝑈 ) ∈ ( SubGrp ‘ 𝑌 ) → ( ( 𝐼𝑈 ) ( 𝐼𝑈 ) ) = ( 𝐼𝑈 ) )
39 37 38 syl ( 𝜑 → ( ( 𝐼𝑈 ) ( 𝐼𝑈 ) ) = ( 𝐼𝑈 ) )
40 fveq2 ( 𝑈 = 𝑉 → ( 𝐼𝑈 ) = ( 𝐼𝑉 ) )
41 40 oveq2d ( 𝑈 = 𝑉 → ( ( 𝐼𝑈 ) ( 𝐼𝑈 ) ) = ( ( 𝐼𝑈 ) ( 𝐼𝑉 ) ) )
42 39 41 sylan9req ( ( 𝜑𝑈 = 𝑉 ) → ( 𝐼𝑈 ) = ( ( 𝐼𝑈 ) ( 𝐼𝑉 ) ) )
43 26 42 sseqtrd ( ( 𝜑𝑈 = 𝑉 ) → ( 𝐼 ‘ ( 𝑈 𝑉 ) ) ⊆ ( ( 𝐼𝑈 ) ( 𝐼𝑉 ) ) )
44 13 adantr ( ( 𝜑𝑈𝑉 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
45 14 adantr ( ( 𝜑𝑈𝑉 ) → ( 𝑈𝐴𝑈 𝑊 ) )
46 15 adantr ( ( 𝜑𝑈𝑉 ) → ( 𝑉𝐴𝑉 𝑊 ) )
47 simpr ( ( 𝜑𝑈𝑉 ) → 𝑈𝑉 )
48 1 2 3 4 5 6 7 8 9 10 11 12 44 45 46 47 dia2dimlem12 ( ( 𝜑𝑈𝑉 ) → ( 𝐼 ‘ ( 𝑈 𝑉 ) ) ⊆ ( ( 𝐼𝑈 ) ( 𝐼𝑉 ) ) )
49 43 48 pm2.61dane ( 𝜑 → ( 𝐼 ‘ ( 𝑈 𝑉 ) ) ⊆ ( ( 𝐼𝑈 ) ( 𝐼𝑉 ) ) )