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 ⊢ H = LHyp ⁡ K
dihprrn.u ⊢ U = DVecH ⁡ K ⁡ W
dihprrn.v ⊢ V = Base U
dihprrn.n ⊢ N = LSpan ⁡ U
dihprrn.i ⊢ I = DIsoH ⁡ K ⁡ W
dihprrn.k ⊢ φ → K ∈ HL ∧ W ∈ H
dihprrn.x ⊢ φ → X ∈ V
dihprrn.y ⊢ φ → Y ∈ V
Assertion dihprrn ⊢ φ → N ⁡ X Y ∈ ran ⁡ I

Proof

Step Hyp Ref Expression
1 dihprrn.h ⊢ H = LHyp ⁡ K
2 dihprrn.u ⊢ U = DVecH ⁡ K ⁡ W
3 dihprrn.v ⊢ V = Base U
4 dihprrn.n ⊢ N = LSpan ⁡ U
5 dihprrn.i ⊢ I = DIsoH ⁡ K ⁡ W
6 dihprrn.k ⊢ φ → K ∈ HL ∧ W ∈ H
7 dihprrn.x ⊢ φ → X ∈ V
8 dihprrn.y ⊢ φ → Y ∈ V
9 prcom ⊢ X Y = Y X
10 preq2 ⊢ X = 0 U → Y X = Y 0 U
11 9 10 eqtrid ⊢ X = 0 U → X Y = Y 0 U
12 11 fveq2d ⊢ X = 0 U → N ⁡ X Y = N ⁡ Y 0 U
13 eqid ⊢ 0 U = 0 U
14 1 2 6 dvhlmod ⊢ φ → U ∈ LMod
15 3 13 4 14 8 lsppr0 ⊢ φ → N ⁡ Y 0 U = N ⁡ Y
16 12 15 sylan9eqr ⊢ φ ∧ X = 0 U → N ⁡ X Y = N ⁡ Y
17 1 2 3 4 5 dihlsprn ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ V → N ⁡ Y ∈ ran ⁡ I
18 6 8 17 syl2anc ⊢ φ → N ⁡ Y ∈ ran ⁡ I
19 18 adantr ⊢ φ ∧ X = 0 U → N ⁡ Y ∈ ran ⁡ I
20 16 19 eqeltrd ⊢ φ ∧ X = 0 U → N ⁡ X Y ∈ ran ⁡ I
21 preq2 ⊢ Y = 0 U → X Y = X 0 U
22 21 fveq2d ⊢ Y = 0 U → N ⁡ X Y = N ⁡ X 0 U
23 3 13 4 14 7 lsppr0 ⊢ φ → N ⁡ X 0 U = N ⁡ X
24 22 23 sylan9eqr ⊢ φ ∧ Y = 0 U → N ⁡ X Y = N ⁡ X
25 1 2 3 4 5 dihlsprn ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ V → N ⁡ X ∈ ran ⁡ I
26 6 7 25 syl2anc ⊢ φ → N ⁡ X ∈ ran ⁡ I
27 26 adantr ⊢ φ ∧ Y = 0 U → N ⁡ X ∈ ran ⁡ I
28 24 27 eqeltrd ⊢ φ ∧ Y = 0 U → N ⁡ X Y ∈ ran ⁡ I
29 6 adantr ⊢ φ ∧ X ≠ 0 U ∧ Y ≠ 0 U → K ∈ HL ∧ W ∈ H
30 7 adantr ⊢ φ ∧ X ≠ 0 U ∧ Y ≠ 0 U → X ∈ V
31 8 adantr ⊢ φ ∧ X ≠ 0 U ∧ Y ≠ 0 U → Y ∈ V
32 simprl ⊢ φ ∧ X ≠ 0 U ∧ Y ≠ 0 U → X ≠ 0 U
33 simprr ⊢ φ ∧ X ≠ 0 U ∧ Y ≠ 0 U → Y ≠ 0 U
34 1 2 3 4 5 29 30 31 13 32 33 dihprrnlem2 ⊢ φ ∧ X ≠ 0 U ∧ Y ≠ 0 U → N ⁡ X Y ∈ ran ⁡ I
35 20 28 34 pm2.61da2ne ⊢ φ → N ⁡ X Y ∈ ran ⁡ I