Metamath Proof Explorer

Theorem tendorinv

Description: Right multiplicative inverse for endomorphism. (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 tendorinv ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → S ∘ N ⁡ S = I ↾ T

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 simp1 ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → K ∈ HL ∧ W ∈ H
10 eqid ⊢ EDRing ⁡ K ⁡ W = EDRing ⁡ K ⁡ W
11 2 10 6 7 dvhsca ⊢ K ∈ HL ∧ W ∈ H → F = EDRing ⁡ K ⁡ W
12 9 11 syl ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → F = EDRing ⁡ K ⁡ W
13 2 10 erngdv ⊢ K ∈ HL ∧ W ∈ H → EDRing ⁡ K ⁡ W ∈ DivRing
14 9 13 syl ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → EDRing ⁡ K ⁡ W ∈ DivRing
15 12 14 eqeltrd ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → F ∈ DivRing
16 simp2 ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → S ∈ E
17 eqid ⊢ Base F = Base F
18 2 4 6 7 17 dvhbase ⊢ K ∈ HL ∧ W ∈ H → Base F = E
19 9 18 syl ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → Base F = E
20 16 19 eleqtrrd ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → S ∈ Base F
21 simp3 ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → S ≠ O
22 11 fveq2d ⊢ K ∈ HL ∧ W ∈ H → 0 F = 0 EDRing ⁡ K ⁡ W
23 eqid ⊢ 0 EDRing ⁡ K ⁡ W = 0 EDRing ⁡ K ⁡ W
24 1 2 3 10 5 23 erng0g ⊢ K ∈ HL ∧ W ∈ H → 0 EDRing ⁡ K ⁡ W = O
25 22 24 eqtrd ⊢ K ∈ HL ∧ W ∈ H → 0 F = O
26 9 25 syl ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → 0 F = O
27 21 26 neeqtrrd ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → S ≠ 0 F
28 eqid ⊢ 0 F = 0 F
29 eqid ⊢ ⋅ F = ⋅ F
30 eqid ⊢ 1 F = 1 F
31 17 28 29 30 8 drnginvrr ⊢ F ∈ DivRing ∧ S ∈ Base F ∧ S ≠ 0 F → S ⋅ F N ⁡ S = 1 F
32 15 20 27 31 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → S ⋅ F N ⁡ S = 1 F
33 1 2 3 4 5 6 7 8 tendoinvcl ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → N ⁡ S ∈ E ∧ N ⁡ S ≠ O
34 33 simpld ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → N ⁡ S ∈ E
35 2 3 4 6 7 29 dvhmulr ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ N ⁡ S ∈ E → S ⋅ F N ⁡ S = S ∘ N ⁡ S
36 9 16 34 35 syl12anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → S ⋅ F N ⁡ S = S ∘ N ⁡ S
37 11 fveq2d ⊢ K ∈ HL ∧ W ∈ H → 1 F = 1 EDRing ⁡ K ⁡ W
38 eqid ⊢ 1 EDRing ⁡ K ⁡ W = 1 EDRing ⁡ K ⁡ W
39 2 3 10 38 erng1r ⊢ K ∈ HL ∧ W ∈ H → 1 EDRing ⁡ K ⁡ W = I ↾ T
40 37 39 eqtrd ⊢ K ∈ HL ∧ W ∈ H → 1 F = I ↾ T
41 9 40 syl ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → 1 F = I ↾ T
42 32 36 41 3eqtr3d ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ S ≠ O → S ∘ N ⁡ S = I ↾ T