# Metamath Proof Explorer

## Theorem tendoinvcl

Description: Closure of multiplicative inverse for endomorphism. We use the scalar inverse of the vector space since it is much simpler than the direct inverse of cdleml8 . (Contributed by NM, 10-Apr-2014) (Revised by Mario Carneiro, 23-Jun-2014)

Ref Expression
Hypotheses tendoinv.b $⊢ B = Base K$
tendoinv.h $⊢ H = LHyp ⁡ K$
tendoinv.t $⊢ T = LTrn ⁡ K ⁡ W$
tendoinv.e $⊢ E = TEndo ⁡ K ⁡ W$
tendoinv.o $⊢ O = h ∈ T ⟼ I ↾ B$
tendoinv.u $⊢ U = DVecH ⁡ K ⁡ W$
tendoinv.f $⊢ F = Scalar ⁡ U$
tendoinv.n $⊢ N = inv r ⁡ F$
Assertion tendoinvcl $⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → N ⁡ S ∈ E ∧ N ⁡ S ≠ O$

### Proof

Step Hyp Ref Expression
1 tendoinv.b $⊢ B = Base K$
2 tendoinv.h $⊢ H = LHyp ⁡ K$
3 tendoinv.t $⊢ T = LTrn ⁡ K ⁡ W$
4 tendoinv.e $⊢ E = TEndo ⁡ K ⁡ W$
5 tendoinv.o $⊢ O = h ∈ T ⟼ I ↾ B$
6 tendoinv.u $⊢ U = DVecH ⁡ K ⁡ W$
7 tendoinv.f $⊢ F = Scalar ⁡ U$
8 tendoinv.n $⊢ N = inv r ⁡ F$
9 eqid $⊢ EDRing ⁡ K ⁡ W = EDRing ⁡ K ⁡ W$
10 2 9 6 7 dvhsca $⊢ K ∈ HL ∧ W ∈ H → F = EDRing ⁡ K ⁡ W$
11 2 9 erngdv $⊢ K ∈ HL ∧ W ∈ H → EDRing ⁡ K ⁡ W ∈ DivRing$
12 10 11 eqeltrd $⊢ K ∈ HL ∧ W ∈ H → F ∈ DivRing$
13 12 3ad2ant1 $⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → F ∈ DivRing$
14 simp2 $⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → S ∈ E$
15 eqid $⊢ Base F = Base F$
16 2 4 6 7 15 dvhbase $⊢ K ∈ HL ∧ W ∈ H → Base F = E$
17 16 3ad2ant1 $⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → Base F = E$
18 14 17 eleqtrrd $⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → S ∈ Base F$
19 simp3 $⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → S ≠ O$
20 10 fveq2d $⊢ K ∈ HL ∧ W ∈ H → 0 F = 0 EDRing ⁡ K ⁡ W$
21 eqid $⊢ 0 EDRing ⁡ K ⁡ W = 0 EDRing ⁡ K ⁡ W$
22 1 2 3 9 5 21 erng0g $⊢ K ∈ HL ∧ W ∈ H → 0 EDRing ⁡ K ⁡ W = O$
23 20 22 eqtrd $⊢ K ∈ HL ∧ W ∈ H → 0 F = O$
24 23 3ad2ant1 $⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → 0 F = O$
25 19 24 neeqtrrd $⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → S ≠ 0 F$
26 eqid $⊢ 0 F = 0 F$
27 15 26 8 drnginvrcl $⊢ F ∈ DivRing ∧ S ∈ Base F ∧ S ≠ 0 F → N ⁡ S ∈ Base F$
28 13 18 25 27 syl3anc $⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → N ⁡ S ∈ Base F$
29 28 17 eleqtrd $⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → N ⁡ S ∈ E$
30 15 26 8 drnginvrn0 $⊢ F ∈ DivRing ∧ S ∈ Base F ∧ S ≠ 0 F → N ⁡ S ≠ 0 F$
31 13 18 25 30 syl3anc $⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → N ⁡ S ≠ 0 F$
32 31 24 neeqtrd $⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → N ⁡ S ≠ O$
33 29 32 jca $⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → N ⁡ S ∈ E ∧ N ⁡ S ≠ O$