Metamath Proof Explorer

Theorem dih1dimb

Description: Two expressions for a 1-dimensional subspace of vector space H (when F is a nonzero vector i.e. non-identity translation). (Contributed by NM, 27-Apr-2014)

Ref Expression
Hypotheses dih1dimb.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
dih1dimb.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dih1dimb.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
dih1dimb.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
dih1dimb.o ${⊢}{O}=\left({h}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
dih1dimb.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dih1dimb.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
dih1dimb.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
Assertion dih1dimb ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to {I}\left({R}\left({F}\right)\right)={N}\left(\left\{⟨{F},{O}⟩\right\}\right)$

Proof

Step Hyp Ref Expression
1 dih1dimb.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 dih1dimb.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
3 dih1dimb.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
4 dih1dimb.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
5 dih1dimb.o ${⊢}{O}=\left({h}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
6 dih1dimb.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
7 dih1dimb.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
8 dih1dimb.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
9 simpl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
10 1 2 3 4 trlcl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to {R}\left({F}\right)\in {B}$
11 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
12 11 2 3 4 trlle ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to {R}\left({F}\right){\le }_{{K}}{W}$
13 eqid ${⊢}\mathrm{DIsoB}\left({K}\right)\left({W}\right)=\mathrm{DIsoB}\left({K}\right)\left({W}\right)$
14 1 11 2 7 13 dihvalb ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({R}\left({F}\right)\in {B}\wedge {R}\left({F}\right){\le }_{{K}}{W}\right)\right)\to {I}\left({R}\left({F}\right)\right)=\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({R}\left({F}\right)\right)$
15 9 10 12 14 syl12anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to {I}\left({R}\left({F}\right)\right)=\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({R}\left({F}\right)\right)$
16 1 2 3 4 5 6 13 8 dib1dim2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to \mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({R}\left({F}\right)\right)={N}\left(\left\{⟨{F},{O}⟩\right\}\right)$
17 15 16 eqtrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to {I}\left({R}\left({F}\right)\right)={N}\left(\left\{⟨{F},{O}⟩\right\}\right)$