# Metamath Proof Explorer

## Theorem dihpN

Description: The value of isomorphism H at the fiducial atom P is determined by the vector <. 0 , S >. (the zero translation ltrnid and a nonzero member of the endomorphism ring). In particular, S can be replaced with the ring unit  ( _I |T ) . (Contributed by NM, 26-Aug-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihp.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
dihp.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dihp.p ${⊢}{P}=\mathrm{oc}\left({K}\right)\left({W}\right)$
dihp.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
dihp.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
dihp.o ${⊢}{O}=\left({f}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
dihp.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
dihp.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dihp.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
dihp.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
dihp.s ${⊢}{\phi }\to \left({S}\in {E}\wedge {S}\ne {O}\right)$
Assertion dihpN ${⊢}{\phi }\to {I}\left({P}\right)={N}\left(\left\{⟨{\mathrm{I}↾}_{{B}},{S}⟩\right\}\right)$

### Proof

Step Hyp Ref Expression
1 dihp.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 dihp.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
3 dihp.p ${⊢}{P}=\mathrm{oc}\left({K}\right)\left({W}\right)$
4 dihp.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
5 dihp.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
6 dihp.o ${⊢}{O}=\left({f}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
7 dihp.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
8 dihp.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
9 dihp.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
10 dihp.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
11 dihp.s ${⊢}{\phi }\to \left({S}\in {E}\wedge {S}\ne {O}\right)$
12 eqid ${⊢}{0}_{{U}}={0}_{{U}}$
13 eqid ${⊢}\mathrm{LSAtoms}\left({U}\right)=\mathrm{LSAtoms}\left({U}\right)$
14 2 8 10 dvhlvec ${⊢}{\phi }\to {U}\in \mathrm{LVec}$
15 2 3 7 8 13 10 dihat ${⊢}{\phi }\to {I}\left({P}\right)\in \mathrm{LSAtoms}\left({U}\right)$
16 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
17 eqid ${⊢}\mathrm{Atoms}\left({K}\right)=\mathrm{Atoms}\left({K}\right)$
18 16 17 2 3 lhpocnel2 ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left({P}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{P}{\le }_{{K}}{W}\right)$
19 eqid ${⊢}\left(\iota {f}\in {T}|{f}\left({P}\right)={P}\right)=\left(\iota {f}\in {T}|{f}\left({P}\right)={P}\right)$
20 1 16 17 2 4 19 ltrniotaidvalN ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({P}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{P}{\le }_{{K}}{W}\right)\right)\to \left(\iota {f}\in {T}|{f}\left({P}\right)={P}\right)={\mathrm{I}↾}_{{B}}$
21 10 18 20 syl2anc2 ${⊢}{\phi }\to \left(\iota {f}\in {T}|{f}\left({P}\right)={P}\right)={\mathrm{I}↾}_{{B}}$
22 21 fveq2d ${⊢}{\phi }\to {S}\left(\left(\iota {f}\in {T}|{f}\left({P}\right)={P}\right)\right)={S}\left({\mathrm{I}↾}_{{B}}\right)$
23 11 simpld ${⊢}{\phi }\to {S}\in {E}$
24 1 2 5 tendoid ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\right)\to {S}\left({\mathrm{I}↾}_{{B}}\right)={\mathrm{I}↾}_{{B}}$
25 10 23 24 syl2anc ${⊢}{\phi }\to {S}\left({\mathrm{I}↾}_{{B}}\right)={\mathrm{I}↾}_{{B}}$
26 22 25 eqtr2d ${⊢}{\phi }\to {\mathrm{I}↾}_{{B}}={S}\left(\left(\iota {f}\in {T}|{f}\left({P}\right)={P}\right)\right)$
27 1 fvexi ${⊢}{B}\in \mathrm{V}$
28 resiexg ${⊢}{B}\in \mathrm{V}\to {\mathrm{I}↾}_{{B}}\in \mathrm{V}$
29 27 28 mp1i ${⊢}{\phi }\to {\mathrm{I}↾}_{{B}}\in \mathrm{V}$
30 eqeq1 ${⊢}{g}={\mathrm{I}↾}_{{B}}\to \left({g}={s}\left(\left(\iota {f}\in {T}|{f}\left({P}\right)={P}\right)\right)↔{\mathrm{I}↾}_{{B}}={s}\left(\left(\iota {f}\in {T}|{f}\left({P}\right)={P}\right)\right)\right)$
31 30 anbi1d ${⊢}{g}={\mathrm{I}↾}_{{B}}\to \left(\left({g}={s}\left(\left(\iota {f}\in {T}|{f}\left({P}\right)={P}\right)\right)\wedge {s}\in {E}\right)↔\left({\mathrm{I}↾}_{{B}}={s}\left(\left(\iota {f}\in {T}|{f}\left({P}\right)={P}\right)\right)\wedge {s}\in {E}\right)\right)$
32 fveq1 ${⊢}{s}={S}\to {s}\left(\left(\iota {f}\in {T}|{f}\left({P}\right)={P}\right)\right)={S}\left(\left(\iota {f}\in {T}|{f}\left({P}\right)={P}\right)\right)$
33 32 eqeq2d ${⊢}{s}={S}\to \left({\mathrm{I}↾}_{{B}}={s}\left(\left(\iota {f}\in {T}|{f}\left({P}\right)={P}\right)\right)↔{\mathrm{I}↾}_{{B}}={S}\left(\left(\iota {f}\in {T}|{f}\left({P}\right)={P}\right)\right)\right)$
34 eleq1 ${⊢}{s}={S}\to \left({s}\in {E}↔{S}\in {E}\right)$
35 33 34 anbi12d ${⊢}{s}={S}\to \left(\left({\mathrm{I}↾}_{{B}}={s}\left(\left(\iota {f}\in {T}|{f}\left({P}\right)={P}\right)\right)\wedge {s}\in {E}\right)↔\left({\mathrm{I}↾}_{{B}}={S}\left(\left(\iota {f}\in {T}|{f}\left({P}\right)={P}\right)\right)\wedge {S}\in {E}\right)\right)$
36 31 35 opelopabg ${⊢}\left({\mathrm{I}↾}_{{B}}\in \mathrm{V}\wedge {S}\in {E}\right)\to \left(⟨{\mathrm{I}↾}_{{B}},{S}⟩\in \left\{⟨{g},{s}⟩|\left({g}={s}\left(\left(\iota {f}\in {T}|{f}\left({P}\right)={P}\right)\right)\wedge {s}\in {E}\right)\right\}↔\left({\mathrm{I}↾}_{{B}}={S}\left(\left(\iota {f}\in {T}|{f}\left({P}\right)={P}\right)\right)\wedge {S}\in {E}\right)\right)$
37 29 23 36 syl2anc ${⊢}{\phi }\to \left(⟨{\mathrm{I}↾}_{{B}},{S}⟩\in \left\{⟨{g},{s}⟩|\left({g}={s}\left(\left(\iota {f}\in {T}|{f}\left({P}\right)={P}\right)\right)\wedge {s}\in {E}\right)\right\}↔\left({\mathrm{I}↾}_{{B}}={S}\left(\left(\iota {f}\in {T}|{f}\left({P}\right)={P}\right)\right)\wedge {S}\in {E}\right)\right)$
38 26 23 37 mpbir2and ${⊢}{\phi }\to ⟨{\mathrm{I}↾}_{{B}},{S}⟩\in \left\{⟨{g},{s}⟩|\left({g}={s}\left(\left(\iota {f}\in {T}|{f}\left({P}\right)={P}\right)\right)\wedge {s}\in {E}\right)\right\}$
39 eqid ${⊢}\mathrm{DIsoC}\left({K}\right)\left({W}\right)=\mathrm{DIsoC}\left({K}\right)\left({W}\right)$
40 16 17 2 39 7 dihvalcqat ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({P}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{P}{\le }_{{K}}{W}\right)\right)\to {I}\left({P}\right)=\mathrm{DIsoC}\left({K}\right)\left({W}\right)\left({P}\right)$
41 10 18 40 syl2anc2 ${⊢}{\phi }\to {I}\left({P}\right)=\mathrm{DIsoC}\left({K}\right)\left({W}\right)\left({P}\right)$
42 16 17 2 3 4 5 39 dicval ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({P}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{P}{\le }_{{K}}{W}\right)\right)\to \mathrm{DIsoC}\left({K}\right)\left({W}\right)\left({P}\right)=\left\{⟨{g},{s}⟩|\left({g}={s}\left(\left(\iota {f}\in {T}|{f}\left({P}\right)={P}\right)\right)\wedge {s}\in {E}\right)\right\}$
43 10 18 42 syl2anc2 ${⊢}{\phi }\to \mathrm{DIsoC}\left({K}\right)\left({W}\right)\left({P}\right)=\left\{⟨{g},{s}⟩|\left({g}={s}\left(\left(\iota {f}\in {T}|{f}\left({P}\right)={P}\right)\right)\wedge {s}\in {E}\right)\right\}$
44 41 43 eqtr2d ${⊢}{\phi }\to \left\{⟨{g},{s}⟩|\left({g}={s}\left(\left(\iota {f}\in {T}|{f}\left({P}\right)={P}\right)\right)\wedge {s}\in {E}\right)\right\}={I}\left({P}\right)$
45 38 44 eleqtrd ${⊢}{\phi }\to ⟨{\mathrm{I}↾}_{{B}},{S}⟩\in {I}\left({P}\right)$
46 11 simprd ${⊢}{\phi }\to {S}\ne {O}$
47 1 2 4 8 12 6 dvh0g ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {0}_{{U}}=⟨{\mathrm{I}↾}_{{B}},{O}⟩$
48 10 47 syl ${⊢}{\phi }\to {0}_{{U}}=⟨{\mathrm{I}↾}_{{B}},{O}⟩$
49 48 eqeq2d ${⊢}{\phi }\to \left(⟨{\mathrm{I}↾}_{{B}},{S}⟩={0}_{{U}}↔⟨{\mathrm{I}↾}_{{B}},{S}⟩=⟨{\mathrm{I}↾}_{{B}},{O}⟩\right)$
50 27 28 ax-mp ${⊢}{\mathrm{I}↾}_{{B}}\in \mathrm{V}$
51 4 fvexi ${⊢}{T}\in \mathrm{V}$
52 51 mptex ${⊢}\left({f}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)\in \mathrm{V}$
53 6 52 eqeltri ${⊢}{O}\in \mathrm{V}$
54 50 53 opth2 ${⊢}⟨{\mathrm{I}↾}_{{B}},{S}⟩=⟨{\mathrm{I}↾}_{{B}},{O}⟩↔\left({\mathrm{I}↾}_{{B}}={\mathrm{I}↾}_{{B}}\wedge {S}={O}\right)$
55 54 simprbi ${⊢}⟨{\mathrm{I}↾}_{{B}},{S}⟩=⟨{\mathrm{I}↾}_{{B}},{O}⟩\to {S}={O}$
56 49 55 syl6bi ${⊢}{\phi }\to \left(⟨{\mathrm{I}↾}_{{B}},{S}⟩={0}_{{U}}\to {S}={O}\right)$
57 56 necon3d ${⊢}{\phi }\to \left({S}\ne {O}\to ⟨{\mathrm{I}↾}_{{B}},{S}⟩\ne {0}_{{U}}\right)$
58 46 57 mpd ${⊢}{\phi }\to ⟨{\mathrm{I}↾}_{{B}},{S}⟩\ne {0}_{{U}}$
59 12 9 13 14 15 45 58 lsatel ${⊢}{\phi }\to {I}\left({P}\right)={N}\left(\left\{⟨{\mathrm{I}↾}_{{B}},{S}⟩\right\}\right)$