Metamath Proof Explorer


Theorem hgmaprnlem2N

Description: Lemma for hgmaprnN . Part 15 of Baer p. 50 line 20. We only require a subset relation, rather than equality, so that the case of zero z is taken care of automatically. (Contributed by NM, 7-Jun-2015) (New usage is discouraged.)

Ref Expression
Hypotheses hgmaprnlem1.h 𝐻 = ( LHyp ‘ 𝐾 )
hgmaprnlem1.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hgmaprnlem1.v 𝑉 = ( Base ‘ 𝑈 )
hgmaprnlem1.r 𝑅 = ( Scalar ‘ 𝑈 )
hgmaprnlem1.b 𝐵 = ( Base ‘ 𝑅 )
hgmaprnlem1.t · = ( ·𝑠𝑈 )
hgmaprnlem1.o 0 = ( 0g𝑈 )
hgmaprnlem1.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
hgmaprnlem1.d 𝐷 = ( Base ‘ 𝐶 )
hgmaprnlem1.p 𝑃 = ( Scalar ‘ 𝐶 )
hgmaprnlem1.a 𝐴 = ( Base ‘ 𝑃 )
hgmaprnlem1.e = ( ·𝑠𝐶 )
hgmaprnlem1.q 𝑄 = ( 0g𝐶 )
hgmaprnlem1.s 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hgmaprnlem1.g 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
hgmaprnlem1.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
hgmaprnlem1.z ( 𝜑𝑧𝐴 )
hgmaprnlem1.t2 ( 𝜑𝑡 ∈ ( 𝑉 ∖ { 0 } ) )
hgmaprnlem1.s2 ( 𝜑𝑠𝑉 )
hgmaprnlem1.sz ( 𝜑 → ( 𝑆𝑠 ) = ( 𝑧 ( 𝑆𝑡 ) ) )
hgmaprnlem1.m 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
hgmaprnlem1.n 𝑁 = ( LSpan ‘ 𝑈 )
hgmaprnlem1.l 𝐿 = ( LSpan ‘ 𝐶 )
Assertion hgmaprnlem2N ( 𝜑 → ( 𝑁 ‘ { 𝑠 } ) ⊆ ( 𝑁 ‘ { 𝑡 } ) )

Proof

Step Hyp Ref Expression
1 hgmaprnlem1.h 𝐻 = ( LHyp ‘ 𝐾 )
2 hgmaprnlem1.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hgmaprnlem1.v 𝑉 = ( Base ‘ 𝑈 )
4 hgmaprnlem1.r 𝑅 = ( Scalar ‘ 𝑈 )
5 hgmaprnlem1.b 𝐵 = ( Base ‘ 𝑅 )
6 hgmaprnlem1.t · = ( ·𝑠𝑈 )
7 hgmaprnlem1.o 0 = ( 0g𝑈 )
8 hgmaprnlem1.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
9 hgmaprnlem1.d 𝐷 = ( Base ‘ 𝐶 )
10 hgmaprnlem1.p 𝑃 = ( Scalar ‘ 𝐶 )
11 hgmaprnlem1.a 𝐴 = ( Base ‘ 𝑃 )
12 hgmaprnlem1.e = ( ·𝑠𝐶 )
13 hgmaprnlem1.q 𝑄 = ( 0g𝐶 )
14 hgmaprnlem1.s 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
15 hgmaprnlem1.g 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
16 hgmaprnlem1.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
17 hgmaprnlem1.z ( 𝜑𝑧𝐴 )
18 hgmaprnlem1.t2 ( 𝜑𝑡 ∈ ( 𝑉 ∖ { 0 } ) )
19 hgmaprnlem1.s2 ( 𝜑𝑠𝑉 )
20 hgmaprnlem1.sz ( 𝜑 → ( 𝑆𝑠 ) = ( 𝑧 ( 𝑆𝑡 ) ) )
21 hgmaprnlem1.m 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
22 hgmaprnlem1.n 𝑁 = ( LSpan ‘ 𝑈 )
23 hgmaprnlem1.l 𝐿 = ( LSpan ‘ 𝐶 )
24 1 8 16 lcdlmod ( 𝜑𝐶 ∈ LMod )
25 18 eldifad ( 𝜑𝑡𝑉 )
26 1 2 3 8 9 14 16 25 hdmapcl ( 𝜑 → ( 𝑆𝑡 ) ∈ 𝐷 )
27 10 11 9 12 23 lspsnvsi ( ( 𝐶 ∈ LMod ∧ 𝑧𝐴 ∧ ( 𝑆𝑡 ) ∈ 𝐷 ) → ( 𝐿 ‘ { ( 𝑧 ( 𝑆𝑡 ) ) } ) ⊆ ( 𝐿 ‘ { ( 𝑆𝑡 ) } ) )
28 24 17 26 27 syl3anc ( 𝜑 → ( 𝐿 ‘ { ( 𝑧 ( 𝑆𝑡 ) ) } ) ⊆ ( 𝐿 ‘ { ( 𝑆𝑡 ) } ) )
29 1 2 3 22 8 23 21 14 16 19 hdmap10 ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑠 } ) ) = ( 𝐿 ‘ { ( 𝑆𝑠 ) } ) )
30 20 sneqd ( 𝜑 → { ( 𝑆𝑠 ) } = { ( 𝑧 ( 𝑆𝑡 ) ) } )
31 30 fveq2d ( 𝜑 → ( 𝐿 ‘ { ( 𝑆𝑠 ) } ) = ( 𝐿 ‘ { ( 𝑧 ( 𝑆𝑡 ) ) } ) )
32 29 31 eqtrd ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑠 } ) ) = ( 𝐿 ‘ { ( 𝑧 ( 𝑆𝑡 ) ) } ) )
33 1 2 3 22 8 23 21 14 16 25 hdmap10 ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑡 } ) ) = ( 𝐿 ‘ { ( 𝑆𝑡 ) } ) )
34 28 32 33 3sstr4d ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑠 } ) ) ⊆ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑡 } ) ) )
35 eqid ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
36 1 2 16 dvhlmod ( 𝜑𝑈 ∈ LMod )
37 3 35 22 lspsncl ( ( 𝑈 ∈ LMod ∧ 𝑠𝑉 ) → ( 𝑁 ‘ { 𝑠 } ) ∈ ( LSubSp ‘ 𝑈 ) )
38 36 19 37 syl2anc ( 𝜑 → ( 𝑁 ‘ { 𝑠 } ) ∈ ( LSubSp ‘ 𝑈 ) )
39 3 35 22 lspsncl ( ( 𝑈 ∈ LMod ∧ 𝑡𝑉 ) → ( 𝑁 ‘ { 𝑡 } ) ∈ ( LSubSp ‘ 𝑈 ) )
40 36 25 39 syl2anc ( 𝜑 → ( 𝑁 ‘ { 𝑡 } ) ∈ ( LSubSp ‘ 𝑈 ) )
41 1 2 35 21 16 38 40 mapdord ( 𝜑 → ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑠 } ) ) ⊆ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑡 } ) ) ↔ ( 𝑁 ‘ { 𝑠 } ) ⊆ ( 𝑁 ‘ { 𝑡 } ) ) )
42 34 41 mpbid ( 𝜑 → ( 𝑁 ‘ { 𝑠 } ) ⊆ ( 𝑁 ‘ { 𝑡 } ) )