This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem erngdvlem3-rN

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

Ref Expression
Hypotheses ernggrp.h-r 
|- H = ( LHyp ` K )
ernggrp.d-r 
|- D = ( ( EDRingR ` K ) ` W )
ernggrplem.b-r 
|- B = ( Base ` K )
ernggrplem.t-r 
|- T = ( ( LTrn ` K ) ` W )
ernggrplem.e-r 
|- E = ( ( TEndo ` K ) ` W )
ernggrplem.p-r 
|- P = ( a e. E , b e. E |-> ( f e. T |-> ( ( a ` f ) o. ( b ` f ) ) ) )
ernggrplem.o-r 
|- O = ( f e. T |-> ( _I |` B ) )
ernggrplem.i-r 
|- I = ( a e. E |-> ( f e. T |-> `' ( a ` f ) ) )
erngrnglem.m-r 
|- M = ( a e. E , b e. E |-> ( b o. a ) )
Assertion erngdvlem3-rN 
|- ( ( K e. HL /\ W e. H ) -> D e. Ring )

Proof

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