Metamath Proof Explorer

Theorem erngdvlem3

Description: Lemma for eringring . (Contributed by NM, 6-Aug-2013)

Ref Expression
Hypotheses ernggrp.h ⊢ H = LHyp ⁡ K
ernggrp.d ⊢ D = EDRing ⁡ K ⁡ W
erngdv.b ⊢ B = Base K
erngdv.t ⊢ T = LTrn ⁡ K ⁡ W
erngdv.e ⊢ E = TEndo ⁡ K ⁡ W
erngdv.p ⊢ P = a ∈ E , b ∈ E ⟼ f ∈ T ⟼ a ⁡ f ∘ b ⁡ f
erngdv.o ⊢ 0 ˙ = f ∈ T ⟼ I ↾ B
erngdv.i ⊢ I = a ∈ E ⟼ f ∈ T ⟼ a ⁡ f -1
erngrnglem.m ⊢ + ˙ = a ∈ E , b ∈ E ⟼ a ∘ b
Assertion erngdvlem3 ⊢ K ∈ HL ∧ W ∈ H → D ∈ Ring

Proof

Step Hyp Ref Expression
1 ernggrp.h ⊢ H = LHyp ⁡ K
2 ernggrp.d ⊢ D = EDRing ⁡ K ⁡ W
3 erngdv.b ⊢ B = Base K
4 erngdv.t ⊢ T = LTrn ⁡ K ⁡ W
5 erngdv.e ⊢ E = TEndo ⁡ K ⁡ W
6 erngdv.p ⊢ P = a ∈ E , b ∈ E ⟼ f ∈ T ⟼ a ⁡ f ∘ b ⁡ f
7 erngdv.o ⊢ 0 ˙ = f ∈ T ⟼ I ↾ B
8 erngdv.i ⊢ I = a ∈ E ⟼ f ∈ T ⟼ a ⁡ f -1
9 erngrnglem.m ⊢ + ˙ = a ∈ E , b ∈ E ⟼ a ∘ b
10 eqid ⊢ Base D = Base D
11 1 4 5 2 10 erngbase ⊢ K ∈ HL ∧ W ∈ H → Base D = E
12 11 eqcomd ⊢ K ∈ HL ∧ W ∈ H → E = Base D
13 eqid ⊢ + D = + D
14 1 4 5 2 13 erngfplus ⊢ K ∈ HL ∧ W ∈ H → + D = a ∈ E , b ∈ E ⟼ f ∈ T ⟼ a ⁡ f ∘ b ⁡ f
15 6 14 eqtr4id ⊢ K ∈ HL ∧ W ∈ H → P = + D
16 eqid ⊢ ⋅ D = ⋅ D
17 1 4 5 2 16 erngfmul ⊢ K ∈ HL ∧ W ∈ H → ⋅ D = a ∈ E , b ∈ E ⟼ a ∘ b
18 9 17 eqtr4id ⊢ K ∈ HL ∧ W ∈ H → + ˙ = ⋅ D
19 1 2 3 4 5 6 7 8 erngdvlem1 ⊢ K ∈ HL ∧ W ∈ H → D ∈ Grp
20 18 oveqd ⊢ K ∈ HL ∧ W ∈ H → s + ˙ t = s ⋅ D t
21 20 3ad2ant1 ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E → s + ˙ t = s ⋅ D t
22 1 4 5 2 16 erngmul ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E → s ⋅ D t = s ∘ t
23 22 3impb ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E → s ⋅ D t = s ∘ t
24 21 23 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E → s + ˙ t = s ∘ t
25 1 5 tendococl ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E → s ∘ t ∈ E
26 24 25 eqeltrd ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E → s + ˙ t ∈ E
27 coass ⊢ s ∘ t ∘ u = s ∘ t ∘ u
28 18 oveqd ⊢ K ∈ HL ∧ W ∈ H → s + ˙ t + ˙ u = s + ˙ t ⋅ D u
29 28 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s + ˙ t + ˙ u = s + ˙ t ⋅ D u
30 simpl ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → K ∈ HL ∧ W ∈ H
31 26 3adant3r3 ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s + ˙ t ∈ E
32 simpr3 ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → u ∈ E
33 1 4 5 2 16 erngmul ⊢ K ∈ HL ∧ W ∈ H ∧ s + ˙ t ∈ E ∧ u ∈ E → s + ˙ t ⋅ D u = s + ˙ t ∘ u
34 30 31 32 33 syl12anc ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s + ˙ t ⋅ D u = s + ˙ t ∘ u
35 18 oveqdr ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s + ˙ t = s ⋅ D t
36 22 3adantr3 ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s ⋅ D t = s ∘ t
37 35 36 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s + ˙ t = s ∘ t
38 37 coeq1d ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s + ˙ t ∘ u = s ∘ t ∘ u
39 29 34 38 3eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s + ˙ t + ˙ u = s ∘ t ∘ u
40 18 oveqd ⊢ K ∈ HL ∧ W ∈ H → s + ˙ t + ˙ u = s ⋅ D t + ˙ u
41 40 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s + ˙ t + ˙ u = s ⋅ D t + ˙ u
42 simpr1 ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s ∈ E
43 18 oveqdr ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → t + ˙ u = t ⋅ D u
44 1 4 5 2 16 erngmul ⊢ K ∈ HL ∧ W ∈ H ∧ t ∈ E ∧ u ∈ E → t ⋅ D u = t ∘ u
45 44 3adantr1 ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → t ⋅ D u = t ∘ u
46 43 45 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → t + ˙ u = t ∘ u
47 1 5 tendococl ⊢ K ∈ HL ∧ W ∈ H ∧ t ∈ E ∧ u ∈ E → t ∘ u ∈ E
48 47 3adant3r1 ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → t ∘ u ∈ E
49 46 48 eqeltrd ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → t + ˙ u ∈ E
50 1 4 5 2 16 erngmul ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t + ˙ u ∈ E → s ⋅ D t + ˙ u = s ∘ t + ˙ u
51 30 42 49 50 syl12anc ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s ⋅ D t + ˙ u = s ∘ t + ˙ u
52 46 coeq2d ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s ∘ t + ˙ u = s ∘ t ∘ u
53 41 51 52 3eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s + ˙ t + ˙ u = s ∘ t ∘ u
54 27 39 53 3eqtr4a ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s + ˙ t + ˙ u = s + ˙ t + ˙ u
55 1 4 5 6 tendodi1 ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s ∘ t P u = s ∘ t P s ∘ u
56 18 oveqd ⊢ K ∈ HL ∧ W ∈ H → s + ˙ t P u = s ⋅ D t P u
57 56 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s + ˙ t P u = s ⋅ D t P u
58 1 4 5 6 tendoplcl ⊢ K ∈ HL ∧ W ∈ H ∧ t ∈ E ∧ u ∈ E → t P u ∈ E
59 58 3adant3r1 ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → t P u ∈ E
60 1 4 5 2 16 erngmul ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t P u ∈ E → s ⋅ D t P u = s ∘ t P u
61 30 42 59 60 syl12anc ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s ⋅ D t P u = s ∘ t P u
62 57 61 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s + ˙ t P u = s ∘ t P u
63 18 oveqdr ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s + ˙ u = s ⋅ D u
64 1 4 5 2 16 erngmul ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ u ∈ E → s ⋅ D u = s ∘ u
65 64 3adantr2 ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s ⋅ D u = s ∘ u
66 63 65 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s + ˙ u = s ∘ u
67 37 66 oveq12d ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s + ˙ t P s + ˙ u = s ∘ t P s ∘ u
68 55 62 67 3eqtr4d ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s + ˙ t P u = s + ˙ t P s + ˙ u
69 1 4 5 6 tendodi2 ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s P t ∘ u = s ∘ u P t ∘ u
70 18 oveqd ⊢ K ∈ HL ∧ W ∈ H → s P t + ˙ u = s P t ⋅ D u
71 70 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s P t + ˙ u = s P t ⋅ D u
72 1 4 5 6 tendoplcl ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E → s P t ∈ E
73 72 3adant3r3 ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s P t ∈ E
74 1 4 5 2 16 erngmul ⊢ K ∈ HL ∧ W ∈ H ∧ s P t ∈ E ∧ u ∈ E → s P t ⋅ D u = s P t ∘ u
75 30 73 32 74 syl12anc ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s P t ⋅ D u = s P t ∘ u
76 71 75 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s P t + ˙ u = s P t ∘ u
77 66 46 oveq12d ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s + ˙ u P t + ˙ u = s ∘ u P t ∘ u
78 69 76 77 3eqtr4d ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E ∧ u ∈ E → s P t + ˙ u = s + ˙ u P t + ˙ u
79 1 4 5 tendoidcl ⊢ K ∈ HL ∧ W ∈ H → I ↾ T ∈ E
80 18 oveqd ⊢ K ∈ HL ∧ W ∈ H → I ↾ T + ˙ s = I ↾ T ⋅ D s
81 80 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E → I ↾ T + ˙ s = I ↾ T ⋅ D s
82 simpl ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E → K ∈ HL ∧ W ∈ H
83 79 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E → I ↾ T ∈ E
84 simpr ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E → s ∈ E
85 1 4 5 2 16 erngmul ⊢ K ∈ HL ∧ W ∈ H ∧ I ↾ T ∈ E ∧ s ∈ E → I ↾ T ⋅ D s = I ↾ T ∘ s
86 82 83 84 85 syl12anc ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E → I ↾ T ⋅ D s = I ↾ T ∘ s
87 1 4 5 tendo1mul ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E → I ↾ T ∘ s = s
88 81 86 87 3eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E → I ↾ T + ˙ s = s
89 18 oveqd ⊢ K ∈ HL ∧ W ∈ H → s + ˙ I ↾ T = s ⋅ D I ↾ T
90 89 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E → s + ˙ I ↾ T = s ⋅ D I ↾ T
91 1 4 5 2 16 erngmul ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ I ↾ T ∈ E → s ⋅ D I ↾ T = s ∘ I ↾ T
92 82 84 83 91 syl12anc ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E → s ⋅ D I ↾ T = s ∘ I ↾ T
93 1 4 5 tendo1mulr ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E → s ∘ I ↾ T = s
94 90 92 93 3eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E → s + ˙ I ↾ T = s
95 12 15 18 19 26 54 68 78 79 88 94 isringd ⊢ K ∈ HL ∧ W ∈ H → D ∈ Ring