Metamath Proof Explorer

Theorem dib1dim

Description: Two expressions for the 1-dimensional subspaces of vector space H. (Contributed by NM, 24-Feb-2014) (Revised by Mario Carneiro, 24-Jun-2014)

Ref Expression
Hypotheses dib1dim.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
dib1dim.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dib1dim.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
dib1dim.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
dib1dim.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
dib1dim.o ${⊢}{O}=\left({h}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
dib1dim.i ${⊢}{I}=\mathrm{DIsoB}\left({K}\right)\left({W}\right)$
Assertion dib1dim ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to {I}\left({R}\left({F}\right)\right)=\left\{{g}\in \left({T}×{E}\right)|\exists {s}\in {E}\phantom{\rule{.4em}{0ex}}{g}=⟨{s}\left({F}\right),{O}⟩\right\}$

Proof

Step Hyp Ref Expression
1 dib1dim.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 dib1dim.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
3 dib1dim.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
4 dib1dim.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
5 dib1dim.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
6 dib1dim.o ${⊢}{O}=\left({h}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
7 dib1dim.i ${⊢}{I}=\mathrm{DIsoB}\left({K}\right)\left({W}\right)$
8 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)$
9 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}$
10 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
11 10 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}$
12 eqid ${⊢}\mathrm{DIsoA}\left({K}\right)\left({W}\right)=\mathrm{DIsoA}\left({K}\right)\left({W}\right)$
13 1 10 2 3 6 12 7 dibval2 ${⊢}\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{DIsoA}\left({K}\right)\left({W}\right)\left({R}\left({F}\right)\right)×\left\{{O}\right\}$
14 8 9 11 13 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{DIsoA}\left({K}\right)\left({W}\right)\left({R}\left({F}\right)\right)×\left\{{O}\right\}$
15 relxp ${⊢}\mathrm{Rel}\left(\mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({R}\left({F}\right)\right)×\left\{{O}\right\}\right)$
16 opelxp ${⊢}⟨{f},{t}⟩\in \left(\mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({R}\left({F}\right)\right)×\left\{{O}\right\}\right)↔\left({f}\in \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({R}\left({F}\right)\right)\wedge {t}\in \left\{{O}\right\}\right)$
17 2 3 4 5 12 dia1dim ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({R}\left({F}\right)\right)=\left\{{f}|\exists {s}\in {E}\phantom{\rule{.4em}{0ex}}{f}={s}\left({F}\right)\right\}$
18 17 abeq2d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to \left({f}\in \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({R}\left({F}\right)\right)↔\exists {s}\in {E}\phantom{\rule{.4em}{0ex}}{f}={s}\left({F}\right)\right)$
19 18 anbi1d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to \left(\left({f}\in \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({R}\left({F}\right)\right)\wedge {t}\in \left\{{O}\right\}\right)↔\left(\exists {s}\in {E}\phantom{\rule{.4em}{0ex}}{f}={s}\left({F}\right)\wedge {t}\in \left\{{O}\right\}\right)\right)$
20 2 3 5 tendocl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {s}\in {E}\wedge {F}\in {T}\right)\to {s}\left({F}\right)\in {T}$
21 20 3expa ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {s}\in {E}\right)\wedge {F}\in {T}\right)\to {s}\left({F}\right)\in {T}$
22 21 an32s ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\wedge {s}\in {E}\right)\to {s}\left({F}\right)\in {T}$
23 1 2 3 5 6 tendo0cl ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {O}\in {E}$
24 23 ad2antrr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\wedge {s}\in {E}\right)\to {O}\in {E}$
25 22 24 jca ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\wedge {s}\in {E}\right)\to \left({s}\left({F}\right)\in {T}\wedge {O}\in {E}\right)$
26 eleq1 ${⊢}{f}={s}\left({F}\right)\to \left({f}\in {T}↔{s}\left({F}\right)\in {T}\right)$
27 eleq1 ${⊢}{t}={O}\to \left({t}\in {E}↔{O}\in {E}\right)$
28 26 27 bi2anan9 ${⊢}\left({f}={s}\left({F}\right)\wedge {t}={O}\right)\to \left(\left({f}\in {T}\wedge {t}\in {E}\right)↔\left({s}\left({F}\right)\in {T}\wedge {O}\in {E}\right)\right)$
29 25 28 syl5ibrcom ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\wedge {s}\in {E}\right)\to \left(\left({f}={s}\left({F}\right)\wedge {t}={O}\right)\to \left({f}\in {T}\wedge {t}\in {E}\right)\right)$
30 29 rexlimdva ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to \left(\exists {s}\in {E}\phantom{\rule{.4em}{0ex}}\left({f}={s}\left({F}\right)\wedge {t}={O}\right)\to \left({f}\in {T}\wedge {t}\in {E}\right)\right)$
31 30 pm4.71rd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to \left(\exists {s}\in {E}\phantom{\rule{.4em}{0ex}}\left({f}={s}\left({F}\right)\wedge {t}={O}\right)↔\left(\left({f}\in {T}\wedge {t}\in {E}\right)\wedge \exists {s}\in {E}\phantom{\rule{.4em}{0ex}}\left({f}={s}\left({F}\right)\wedge {t}={O}\right)\right)\right)$
32 velsn ${⊢}{t}\in \left\{{O}\right\}↔{t}={O}$
33 32 anbi2i ${⊢}\left(\exists {s}\in {E}\phantom{\rule{.4em}{0ex}}{f}={s}\left({F}\right)\wedge {t}\in \left\{{O}\right\}\right)↔\left(\exists {s}\in {E}\phantom{\rule{.4em}{0ex}}{f}={s}\left({F}\right)\wedge {t}={O}\right)$
34 r19.41v ${⊢}\exists {s}\in {E}\phantom{\rule{.4em}{0ex}}\left({f}={s}\left({F}\right)\wedge {t}={O}\right)↔\left(\exists {s}\in {E}\phantom{\rule{.4em}{0ex}}{f}={s}\left({F}\right)\wedge {t}={O}\right)$
35 33 34 bitr4i ${⊢}\left(\exists {s}\in {E}\phantom{\rule{.4em}{0ex}}{f}={s}\left({F}\right)\wedge {t}\in \left\{{O}\right\}\right)↔\exists {s}\in {E}\phantom{\rule{.4em}{0ex}}\left({f}={s}\left({F}\right)\wedge {t}={O}\right)$
36 df-3an ${⊢}\left({f}\in {T}\wedge {t}\in {E}\wedge \exists {s}\in {E}\phantom{\rule{.4em}{0ex}}\left({f}={s}\left({F}\right)\wedge {t}={O}\right)\right)↔\left(\left({f}\in {T}\wedge {t}\in {E}\right)\wedge \exists {s}\in {E}\phantom{\rule{.4em}{0ex}}\left({f}={s}\left({F}\right)\wedge {t}={O}\right)\right)$
37 31 35 36 3bitr4g ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to \left(\left(\exists {s}\in {E}\phantom{\rule{.4em}{0ex}}{f}={s}\left({F}\right)\wedge {t}\in \left\{{O}\right\}\right)↔\left({f}\in {T}\wedge {t}\in {E}\wedge \exists {s}\in {E}\phantom{\rule{.4em}{0ex}}\left({f}={s}\left({F}\right)\wedge {t}={O}\right)\right)\right)$
38 19 37 bitrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to \left(\left({f}\in \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({R}\left({F}\right)\right)\wedge {t}\in \left\{{O}\right\}\right)↔\left({f}\in {T}\wedge {t}\in {E}\wedge \exists {s}\in {E}\phantom{\rule{.4em}{0ex}}\left({f}={s}\left({F}\right)\wedge {t}={O}\right)\right)\right)$
39 16 38 syl5bb ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to \left(⟨{f},{t}⟩\in \left(\mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({R}\left({F}\right)\right)×\left\{{O}\right\}\right)↔\left({f}\in {T}\wedge {t}\in {E}\wedge \exists {s}\in {E}\phantom{\rule{.4em}{0ex}}\left({f}={s}\left({F}\right)\wedge {t}={O}\right)\right)\right)$
40 15 39 opabbi2dv ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({R}\left({F}\right)\right)×\left\{{O}\right\}=\left\{⟨{f},{t}⟩|\left({f}\in {T}\wedge {t}\in {E}\wedge \exists {s}\in {E}\phantom{\rule{.4em}{0ex}}\left({f}={s}\left({F}\right)\wedge {t}={O}\right)\right)\right\}$
41 14 40 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)=\left\{⟨{f},{t}⟩|\left({f}\in {T}\wedge {t}\in {E}\wedge \exists {s}\in {E}\phantom{\rule{.4em}{0ex}}\left({f}={s}\left({F}\right)\wedge {t}={O}\right)\right)\right\}$
42 eqeq1 ${⊢}{g}=⟨{f},{t}⟩\to \left({g}=⟨{s}\left({F}\right),{O}⟩↔⟨{f},{t}⟩=⟨{s}\left({F}\right),{O}⟩\right)$
43 vex ${⊢}{f}\in \mathrm{V}$
44 vex ${⊢}{t}\in \mathrm{V}$
45 43 44 opth ${⊢}⟨{f},{t}⟩=⟨{s}\left({F}\right),{O}⟩↔\left({f}={s}\left({F}\right)\wedge {t}={O}\right)$
46 42 45 syl6bb ${⊢}{g}=⟨{f},{t}⟩\to \left({g}=⟨{s}\left({F}\right),{O}⟩↔\left({f}={s}\left({F}\right)\wedge {t}={O}\right)\right)$
47 46 rexbidv ${⊢}{g}=⟨{f},{t}⟩\to \left(\exists {s}\in {E}\phantom{\rule{.4em}{0ex}}{g}=⟨{s}\left({F}\right),{O}⟩↔\exists {s}\in {E}\phantom{\rule{.4em}{0ex}}\left({f}={s}\left({F}\right)\wedge {t}={O}\right)\right)$
48 47 rabxp ${⊢}\left\{{g}\in \left({T}×{E}\right)|\exists {s}\in {E}\phantom{\rule{.4em}{0ex}}{g}=⟨{s}\left({F}\right),{O}⟩\right\}=\left\{⟨{f},{t}⟩|\left({f}\in {T}\wedge {t}\in {E}\wedge \exists {s}\in {E}\phantom{\rule{.4em}{0ex}}\left({f}={s}\left({F}\right)\wedge {t}={O}\right)\right)\right\}$
49 41 48 syl6eqr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to {I}\left({R}\left({F}\right)\right)=\left\{{g}\in \left({T}×{E}\right)|\exists {s}\in {E}\phantom{\rule{.4em}{0ex}}{g}=⟨{s}\left({F}\right),{O}⟩\right\}$