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