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 )