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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
tendoinv.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
tendoinv.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tendoinv.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
tendoinv.o ⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
tendoinv.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
tendoinv.f ⊢ 𝐹 = ( Scalar ‘ 𝑈 )
tendoinv.n ⊢ 𝑁 = ( invr ‘ 𝐹 )
Assertion tendorinv ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) → ( 𝑆 ∘ ( 𝑁 ‘ 𝑆 ) ) = ( I ↾ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 tendoinv.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 tendoinv.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 tendoinv.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 tendoinv.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
5 tendoinv.o ⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
6 tendoinv.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
7 tendoinv.f ⊢ 𝐹 = ( Scalar ‘ 𝑈 )
8 tendoinv.n ⊢ 𝑁 = ( invr ‘ 𝐹 )
9 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10 eqid ⊢ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
11 2 10 6 7 dvhsca ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐹 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) )
12 9 11 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) → 𝐹 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) )
13 2 10 erngdv ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ∈ DivRing )
14 9 13 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) → ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ∈ DivRing )
15 12 14 eqeltrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) → 𝐹 ∈ DivRing )
16 simp2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) → 𝑆 ∈ 𝐸 )
17 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
18 2 4 6 7 17 dvhbase ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝐹 ) = 𝐸 )
19 9 18 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) → ( Base ‘ 𝐹 ) = 𝐸 )
20 16 19 eleqtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) → 𝑆 ∈ ( Base ‘ 𝐹 ) )
21 simp3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) → 𝑆 ≠ 𝑂 )
22 11 fveq2d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 0g ‘ 𝐹 ) = ( 0g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) )
23 eqid ⊢ ( 0g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 0g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) )
24 1 2 3 10 5 23 erng0g ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 0g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑂 )
25 22 24 eqtrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 0g ‘ 𝐹 ) = 𝑂 )
26 9 25 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) → ( 0g ‘ 𝐹 ) = 𝑂 )
27 21 26 neeqtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) → 𝑆 ≠ ( 0g ‘ 𝐹 ) )
28 eqid ⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 )
29 eqid ⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
30 eqid ⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 )
31 17 28 29 30 8 drnginvrr ⊢ ( ( 𝐹 ∈ DivRing ∧ 𝑆 ∈ ( Base ‘ 𝐹 ) ∧ 𝑆 ≠ ( 0g ‘ 𝐹 ) ) → ( 𝑆 ( .r ‘ 𝐹 ) ( 𝑁 ‘ 𝑆 ) ) = ( 1r ‘ 𝐹 ) )
32 15 20 27 31 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) → ( 𝑆 ( .r ‘ 𝐹 ) ( 𝑁 ‘ 𝑆 ) ) = ( 1r ‘ 𝐹 ) )
33 1 2 3 4 5 6 7 8 tendoinvcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) → ( ( 𝑁 ‘ 𝑆 ) ∈ 𝐸 ∧ ( 𝑁 ‘ 𝑆 ) ≠ 𝑂 ) )
34 33 simpld ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) → ( 𝑁 ‘ 𝑆 ) ∈ 𝐸 )
35 2 3 4 6 7 29 dvhmulr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ ( 𝑁 ‘ 𝑆 ) ∈ 𝐸 ) ) → ( 𝑆 ( .r ‘ 𝐹 ) ( 𝑁 ‘ 𝑆 ) ) = ( 𝑆 ∘ ( 𝑁 ‘ 𝑆 ) ) )
36 9 16 34 35 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) → ( 𝑆 ( .r ‘ 𝐹 ) ( 𝑁 ‘ 𝑆 ) ) = ( 𝑆 ∘ ( 𝑁 ‘ 𝑆 ) ) )
37 11 fveq2d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 1r ‘ 𝐹 ) = ( 1r ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) )
38 eqid ⊢ ( 1r ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 1r ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) )
39 2 3 10 38 erng1r ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 1r ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) = ( I ↾ 𝑇 ) )
40 37 39 eqtrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 1r ‘ 𝐹 ) = ( I ↾ 𝑇 ) )
41 9 40 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) → ( 1r ‘ 𝐹 ) = ( I ↾ 𝑇 ) )
42 32 36 41 3eqtr3d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) → ( 𝑆 ∘ ( 𝑁 ‘ 𝑆 ) ) = ( I ↾ 𝑇 ) )