Metamath Proof Explorer

Theorem dihprrn

Description: The span of a vector pair belongs to the range of isomorphism H i.e. is a closed subspace. (Contributed by NM, 29-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 dihprrn.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dihprrn.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 dihprrn.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 dihprrn.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
5 dihprrn.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
6 dihprrn.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 dihprrn.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
8 dihprrn.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
9 prcom ⊢ { 𝑋 , 𝑌 } = { 𝑌 , 𝑋 }
10 preq2 ⊢ ( 𝑋 = ( 0g ‘ 𝑈 ) → { 𝑌 , 𝑋 } = { 𝑌 , ( 0g ‘ 𝑈 ) } )
11 9 10 eqtrid ⊢ ( 𝑋 = ( 0g ‘ 𝑈 ) → { 𝑋 , 𝑌 } = { 𝑌 , ( 0g ‘ 𝑈 ) } )
12 11 fveq2d ⊢ ( 𝑋 = ( 0g ‘ 𝑈 ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( 𝑁 ‘ { 𝑌 , ( 0g ‘ 𝑈 ) } ) )
13 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
14 1 2 6 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
15 3 13 4 14 8 lsppr0 ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 , ( 0g ‘ 𝑈 ) } ) = ( 𝑁 ‘ { 𝑌 } ) )
16 12 15 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( 𝑁 ‘ { 𝑌 } ) )
17 1 2 3 4 5 dihlsprn ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ran 𝐼 )
18 6 8 17 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ran 𝐼 )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ran 𝐼 )
20 16 19 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ran 𝐼 )
21 preq2 ⊢ ( 𝑌 = ( 0g ‘ 𝑈 ) → { 𝑋 , 𝑌 } = { 𝑋 , ( 0g ‘ 𝑈 ) } )
22 21 fveq2d ⊢ ( 𝑌 = ( 0g ‘ 𝑈 ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( 𝑁 ‘ { 𝑋 , ( 0g ‘ 𝑈 ) } ) )
23 3 13 4 14 7 lsppr0 ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , ( 0g ‘ 𝑈 ) } ) = ( 𝑁 ‘ { 𝑋 } ) )
24 22 23 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( 𝑁 ‘ { 𝑋 } ) )
25 1 2 3 4 5 dihlsprn ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ran 𝐼 )
26 6 7 25 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ran 𝐼 )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ran 𝐼 )
28 24 27 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ran 𝐼 )
29 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
30 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ) ) → 𝑋 ∈ 𝑉 )
31 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ) ) → 𝑌 ∈ 𝑉 )
32 simprl ⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ) ) → 𝑋 ≠ ( 0g ‘ 𝑈 ) )
33 simprr ⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ) ) → 𝑌 ≠ ( 0g ‘ 𝑈 ) )
34 1 2 3 4 5 29 30 31 13 32 33 dihprrnlem2 ⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ) ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ran 𝐼 )
35 20 28 34 pm2.61da2ne ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ran 𝐼 )