# Metamath Proof Explorer

## Theorem tendolinv

Description: Left multiplicative inverse for endomorphism. (Contributed by NM, 10-Apr-2014) (Revised by Mario Carneiro, 23-Jun-2014)

Ref Expression
Hypotheses tendoinv.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
tendoinv.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
tendoinv.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
tendoinv.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
tendoinv.o ${⊢}{O}=\left({h}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
tendoinv.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
tendoinv.f ${⊢}{F}=\mathrm{Scalar}\left({U}\right)$
tendoinv.n ${⊢}{N}={inv}_{r}\left({F}\right)$
Assertion tendolinv ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {S}\ne {O}\right)\to {N}\left({S}\right)\circ {S}={\mathrm{I}↾}_{{T}}$

### Proof

Step Hyp Ref Expression
1 tendoinv.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 tendoinv.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
3 tendoinv.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
4 tendoinv.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
5 tendoinv.o ${⊢}{O}=\left({h}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
6 tendoinv.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
7 tendoinv.f ${⊢}{F}=\mathrm{Scalar}\left({U}\right)$
8 tendoinv.n ${⊢}{N}={inv}_{r}\left({F}\right)$
9 simp1 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {S}\ne {O}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
10 eqid ${⊢}\mathrm{EDRing}\left({K}\right)\left({W}\right)=\mathrm{EDRing}\left({K}\right)\left({W}\right)$
11 2 10 6 7 dvhsca ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {F}=\mathrm{EDRing}\left({K}\right)\left({W}\right)$
12 9 11 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {S}\ne {O}\right)\to {F}=\mathrm{EDRing}\left({K}\right)\left({W}\right)$
13 2 10 erngdv ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{EDRing}\left({K}\right)\left({W}\right)\in \mathrm{DivRing}$
14 9 13 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {S}\ne {O}\right)\to \mathrm{EDRing}\left({K}\right)\left({W}\right)\in \mathrm{DivRing}$
15 12 14 eqeltrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {S}\ne {O}\right)\to {F}\in \mathrm{DivRing}$
16 simp2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {S}\ne {O}\right)\to {S}\in {E}$
17 eqid ${⊢}{\mathrm{Base}}_{{F}}={\mathrm{Base}}_{{F}}$
18 2 4 6 7 17 dvhbase ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {\mathrm{Base}}_{{F}}={E}$
19 9 18 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {S}\ne {O}\right)\to {\mathrm{Base}}_{{F}}={E}$
20 16 19 eleqtrrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {S}\ne {O}\right)\to {S}\in {\mathrm{Base}}_{{F}}$
21 simp3 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {S}\ne {O}\right)\to {S}\ne {O}$
22 11 fveq2d ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {0}_{{F}}={0}_{\mathrm{EDRing}\left({K}\right)\left({W}\right)}$
23 eqid ${⊢}{0}_{\mathrm{EDRing}\left({K}\right)\left({W}\right)}={0}_{\mathrm{EDRing}\left({K}\right)\left({W}\right)}$
24 1 2 3 10 5 23 erng0g ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {0}_{\mathrm{EDRing}\left({K}\right)\left({W}\right)}={O}$
25 22 24 eqtrd ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {0}_{{F}}={O}$
26 9 25 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {S}\ne {O}\right)\to {0}_{{F}}={O}$
27 21 26 neeqtrrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {S}\ne {O}\right)\to {S}\ne {0}_{{F}}$
28 eqid ${⊢}{0}_{{F}}={0}_{{F}}$
29 eqid ${⊢}{\cdot }_{{F}}={\cdot }_{{F}}$
30 eqid ${⊢}{1}_{{F}}={1}_{{F}}$
31 17 28 29 30 8 drnginvrl ${⊢}\left({F}\in \mathrm{DivRing}\wedge {S}\in {\mathrm{Base}}_{{F}}\wedge {S}\ne {0}_{{F}}\right)\to {N}\left({S}\right){\cdot }_{{F}}{S}={1}_{{F}}$
32 15 20 27 31 syl3anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {S}\ne {O}\right)\to {N}\left({S}\right){\cdot }_{{F}}{S}={1}_{{F}}$
33 1 2 3 4 5 6 7 8 tendoinvcl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {S}\ne {O}\right)\to \left({N}\left({S}\right)\in {E}\wedge {N}\left({S}\right)\ne {O}\right)$
34 33 simpld ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {S}\ne {O}\right)\to {N}\left({S}\right)\in {E}$
35 2 3 4 6 7 29 dvhmulr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({N}\left({S}\right)\in {E}\wedge {S}\in {E}\right)\right)\to {N}\left({S}\right){\cdot }_{{F}}{S}={N}\left({S}\right)\circ {S}$
36 9 34 16 35 syl12anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {S}\ne {O}\right)\to {N}\left({S}\right){\cdot }_{{F}}{S}={N}\left({S}\right)\circ {S}$
37 11 fveq2d ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {1}_{{F}}={1}_{\mathrm{EDRing}\left({K}\right)\left({W}\right)}$
38 eqid ${⊢}{1}_{\mathrm{EDRing}\left({K}\right)\left({W}\right)}={1}_{\mathrm{EDRing}\left({K}\right)\left({W}\right)}$
39 2 3 10 38 erng1r ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {1}_{\mathrm{EDRing}\left({K}\right)\left({W}\right)}={\mathrm{I}↾}_{{T}}$
40 37 39 eqtrd ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {1}_{{F}}={\mathrm{I}↾}_{{T}}$
41 9 40 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {S}\ne {O}\right)\to {1}_{{F}}={\mathrm{I}↾}_{{T}}$
42 32 36 41 3eqtr3d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {S}\ne {O}\right)\to {N}\left({S}\right)\circ {S}={\mathrm{I}↾}_{{T}}$