Metamath Proof Explorer

Theorem dihlsprn

Description: The span of a vector belongs to the range of isomorphism H. (Contributed by NM, 27-Apr-2014)

Ref Expression
Hypotheses dihlsprn.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihlsprn.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihlsprn.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dihlsprn.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
dihlsprn.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
Assertion dihlsprn ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ran 𝐼 )

Proof

Step Hyp Ref Expression
1 dihlsprn.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dihlsprn.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 dihlsprn.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 dihlsprn.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
5 dihlsprn.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
6 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → 𝑋 = ( 0g ‘ 𝑈 ) )
7 6 sneqd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → { 𝑋 } = { ( 0g ‘ 𝑈 ) } )
8 7 fveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) )
9 simpll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10 1 2 9 dvhlmod ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → 𝑈 ∈ LMod )
11 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
12 11 4 lspsn0 ⊢ ( 𝑈 ∈ LMod → ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) = { ( 0g ‘ 𝑈 ) } )
13 10 12 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) = { ( 0g ‘ 𝑈 ) } )
14 8 13 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑋 } ) = { ( 0g ‘ 𝑈 ) } )
15 1 5 2 11 dih0rn ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → { ( 0g ‘ 𝑈 ) } ∈ ran 𝐼 )
16 15 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → { ( 0g ‘ 𝑈 ) } ∈ ran 𝐼 )
17 14 16 eqeltrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ran 𝐼 )
18 simpll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
19 1 2 18 dvhlmod ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) → 𝑈 ∈ LMod )
20 simplr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) → 𝑋 ∈ 𝑉 )
21 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) → 𝑋 ≠ ( 0g ‘ 𝑈 ) )
22 eqid ⊢ ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
23 3 4 11 22 lsatlspsn2 ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSAtoms ‘ 𝑈 ) )
24 19 20 21 23 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSAtoms ‘ 𝑈 ) )
25 1 2 5 22 dih1dimat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSAtoms ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ran 𝐼 )
26 18 24 25 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ran 𝐼 )
27 17 26 pm2.61dane ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ran 𝐼 )