Theorem erngdvlem3-rN 34285

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

Hypotheses

Ref	Expression
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

Ref	Expression
erngdvlem3-rN	|- ( ( K e. HL /\ W e. H ) -> D e. Ring )

Distinct variable groups:   B, f   a, b, E   f, a, K, b   f, H   T, a, b, f   W, a, b, f

Allowed substitution hints:   B( a, b)   D( f, a, b)   P( f, a, b)   E( f)   H( a, b)   I( f, a, b)   M( f, a, b)   O( f, a, b)

Proof of Theorem erngdvlem3-rN

Dummy variables t s u are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ernggrp.h-r	. . . 4 |- H = ( LHyp ` K )
2		ernggrplem.t-r	. . . 4 |- T = ( ( LTrn ` K ) ` W )
3		ernggrplem.e-r	. . . 4 |- E = ( ( TEndo ` K ) ` W )
4		ernggrp.d-r	. . . 4 |- D = ( ( EDRingR ` K ) ` W )
5		eqid 2429	. . . 4 |- ( Base ` D ) = ( Base ` D )
6	1, 2, 3, 4, 5	erngbase-rN 34096	. . 3 |- ( ( K e. HL /\ W e. H ) -> ( Base ` D ) = E )
7	6	eqcomd 2437	. 2 |- ( ( K e. HL /\ W e. H ) -> E = ( Base ` D ) )
8		eqid 2429	. . . 4 |- ( +g ` D ) = ( +g ` D )
9	1, 2, 3, 4, 8	erngfplus-rN 34097	. . 3 |- ( ( K e. HL /\ W e. H ) -> ( +g ` D ) = ( a e. E , b e. E |-> ( f e. T |-> ( ( a ` f ) o. ( b ` f ) ) ) ) )
10		ernggrplem.p-r	. . 3 |- P = ( a e. E , b e. E |-> ( f e. T |-> ( ( a ` f ) o. ( b ` f ) ) ) )
11	9, 10	syl6reqr 2489	. 2 |- ( ( K e. HL /\ W e. H ) -> P = ( +g ` D ) )
12		eqid 2429	. . . 4 |- ( .r ` D ) = ( .r ` D )
13	1, 2, 3, 4, 12	erngfmul-rN 34100	. . 3 |- ( ( K e. HL /\ W e. H ) -> ( .r ` D ) = ( a e. E , b e. E |-> ( b o. a ) ) )
14		erngrnglem.m-r	. . 3 |- M = ( a e. E , b e. E |-> ( b o. a ) )
15	13, 14	syl6reqr 2489	. 2 |- ( ( K e. HL /\ W e. H ) -> M = ( .r ` D ) )
16		ernggrplem.b-r	. . 3 |- B = ( Base ` K )
17		ernggrplem.o-r	. . 3 |- O = ( f e. T |-> ( _I |` B ) )
18		ernggrplem.i-r	. . 3 |- I = ( a e. E |-> ( f e. T |-> `' ( a ` f ) ) )
19	1, 4, 16, 2, 3, 10, 17, 18	erngdvlem1-rN 34283	. 2 |- ( ( K e. HL /\ W e. H ) -> D e. Grp )
20	15	oveqd 6322	. . . . 5 |- ( ( K e. HL /\ W e. H ) -> ( s M t ) = ( s ( .r ` D ) t ) )
21	20	3ad2ant1 1026	. . . 4 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ t e. E ) -> ( s M t ) = ( s ( .r ` D ) t ) )
22	1, 2, 3, 4, 12	erngmul-rN 34101	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E ) ) -> ( s ( .r ` D ) t ) = ( t o. s ) )
23	22	3impb 1201	. . . 4 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ t e. E ) -> ( s ( .r ` D ) t ) = ( t o. s ) )
24	21, 23	eqtrd 2470	. . 3 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ t e. E ) -> ( s M t ) = ( t o. s ) )
25	1, 3	tendococl 34059	. . . 4 |- ( ( ( K e. HL /\ W e. H ) /\ t e. E /\ s e. E ) -> ( t o. s ) e. E )
26	25	3com23 1211	. . 3 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ t e. E ) -> ( t o. s ) e. E )
27	24, 26	eqeltrd 2517	. 2 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ t e. E ) -> ( s M t ) e. E )
28	15	oveqdr 6329	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ u e. E ) ) -> ( t M u ) = ( t ( .r ` D ) u ) )
29	1, 2, 3, 4, 12	erngmul-rN 34101	. . . . . 6 |- ( ( ( K e. HL /\ W e. H ) /\ ( t e. E /\ u e. E ) ) -> ( t ( .r ` D ) u ) = ( u o. t ) )
30	29	3adantr1 1164	. . . . 5 |- ( ( ( 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 2470	. . . 4 |- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ u e. E ) ) -> ( t M u ) = ( u o. t ) )
32	31	coeq1d 5016	. . 3 |- ( ( ( 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	15	oveqd 6322	. . . . 5 |- ( ( K e. HL /\ W e. H ) -> ( s M ( t M u ) ) = ( s ( .r ` D ) ( t M u ) ) )
34	33	adantr 466	. . . 4 |- ( ( ( 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 458	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ u e. E ) ) -> ( K e. HL /\ W e. H ) )
36		simpr1 1011	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ u e. E ) ) -> s e. E )
37		simpr3 1013	. . . . . . 7 |- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ u e. E ) ) -> u e. E )
38		simpr2 1012	. . . . . . 7 |- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ u e. E ) ) -> t e. E )
39	1, 3	tendococl 34059	. . . . . . 7 |- ( ( ( K e. HL /\ W e. H ) /\ u e. E /\ t e. E ) -> ( u o. t ) e. E )
40	35, 37, 38, 39	syl3anc 1264	. . . . . 6 |- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ u e. E ) ) -> ( u o. t ) e. E )
41	31, 40	eqeltrd 2517	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ u e. E ) ) -> ( t M u ) e. E )
42	1, 2, 3, 4, 12	erngmul-rN 34101	. . . . 5 |- ( ( ( 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 1262	. . . 4 |- ( ( ( 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 2470	. . 3 |- ( ( ( 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	15	oveqd 6322	. . . . . 6 |- ( ( K e. HL /\ W e. H ) -> ( ( s M t ) M u ) = ( ( s M t ) ( .r ` D ) u ) )
46	45	adantr 466	. . . . 5 |- ( ( ( 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 1216	. . . . . 6 |- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ u e. E ) ) -> ( s M t ) e. E )
48	1, 2, 3, 4, 12	erngmul-rN 34101	. . . . . 6 |- ( ( ( 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 1262	. . . . 5 |- ( ( ( 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	15	oveqdr 6329	. . . . . . 7 |- ( ( ( 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 1166	. . . . . . 7 |- ( ( ( 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 2470	. . . . . 6 |- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ u e. E ) ) -> ( s M t ) = ( t o. s ) )
53	52	coeq2d 5017	. . . . 5 |- ( ( ( 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 2474	. . . 4 |- ( ( ( 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 5374	. . . 4 |- ( ( u o. t ) o. s ) = ( u o. ( t o. s ) )
56	54, 55	syl6eqr 2488	. . 3 |- ( ( ( 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 2481	. 2 |- ( ( ( 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, 2, 3, 10	tendodi2 34072	. . . 4 |- ( ( ( 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 1266	. . 3 |- ( ( ( 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	15	oveqd 6322	. . . . 5 |- ( ( K e. HL /\ W e. H ) -> ( s M ( t P u ) ) = ( s ( .r ` D ) ( t P u ) ) )
61	60	adantr 466	. . . 4 |- ( ( ( 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, 2, 3, 10	tendoplcl 34068	. . . . . 6 |- ( ( ( K e. HL /\ W e. H ) /\ t e. E /\ u e. E ) -> ( t P u ) e. E )
63	35, 38, 37, 62	syl3anc 1264	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ u e. E ) ) -> ( t P u ) e. E )
64	1, 2, 3, 4, 12	erngmul-rN 34101	. . . . 5 |- ( ( ( 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 1262	. . . 4 |- ( ( ( 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 2470	. . 3 |- ( ( ( 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	15	oveqdr 6329	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ u e. E ) ) -> ( s M u ) = ( s ( .r ` D ) u ) )
68	1, 2, 3, 4, 12	erngmul-rN 34101	. . . . . 6 |- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ u e. E ) ) -> ( s ( .r ` D ) u ) = ( u o. s ) )
69	68	3adantr2 1165	. . . . 5 |- ( ( ( 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 2470	. . . 4 |- ( ( ( 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 6323	. . 3 |- ( ( ( 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 2480	. 2 |- ( ( ( 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, 2, 3, 10	tendodi1 34071	. . . 4 |- ( ( ( 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 1266	. . 3 |- ( ( ( 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	15	adantr 466	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ u e. E ) ) -> M = ( .r ` D ) )
76	75	oveqd 6322	. . . 4 |- ( ( ( 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, 2, 3, 10	tendoplcl 34068	. . . . . 6 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ t e. E ) -> ( s P t ) e. E )
78	77	3adant3r3 1216	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ u e. E ) ) -> ( s P t ) e. E )
79	1, 2, 3, 4, 12	erngmul-rN 34101	. . . . 5 |- ( ( ( 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 1262	. . . 4 |- ( ( ( 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 2470	. . 3 |- ( ( ( 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 6323	. . 3 |- ( ( ( 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 2480	. 2 |- ( ( ( 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, 2, 3	tendoidcl 34056	. 2 |- ( ( K e. HL /\ W e. H ) -> ( _I |` T ) e. E )
85	15	oveqd 6322	. . . 4 |- ( ( K e. HL /\ W e. H ) -> ( ( _I |` T ) M s ) = ( ( _I |` T ) ( .r ` D ) s ) )
86	85	adantr 466	. . 3 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E ) -> ( ( _I |` T ) M s ) = ( ( _I |` T ) ( .r ` D ) s ) )
87		simpl 458	. . . 4 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E ) -> ( K e. HL /\ W e. H ) )
88	84	adantr 466	. . . 4 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E ) -> ( _I |` T ) e. E )
89		simpr 462	. . . 4 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E ) -> s e. E )
90	1, 2, 3, 4, 12	erngmul-rN 34101	. . . 4 |- ( ( ( 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 1262	. . 3 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E ) -> ( ( _I |` T ) ( .r ` D ) s ) = ( s o. ( _I |` T ) ) )
92	1, 2, 3	tendo1mulr 34058	. . 3 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E ) -> ( s o. ( _I |` T ) ) = s )
93	86, 91, 92	3eqtrd 2474	. 2 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E ) -> ( ( _I |` T ) M s ) = s )
94	15	oveqd 6322	. . . 4 |- ( ( K e. HL /\ W e. H ) -> ( s M ( _I |` T ) ) = ( s ( .r ` D ) ( _I |` T ) ) )
95	94	adantr 466	. . 3 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E ) -> ( s M ( _I |` T ) ) = ( s ( .r ` D ) ( _I |` T ) ) )
96	1, 2, 3, 4, 12	erngmul-rN 34101	. . . 4 |- ( ( ( 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 1262	. . 3 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E ) -> ( s ( .r ` D ) ( _I |` T ) ) = ( ( _I |` T ) o. s ) )
98	1, 2, 3	tendo1mul 34057	. . 3 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E ) -> ( ( _I |` T ) o. s ) = s )
99	95, 97, 98	3eqtrd 2474	. 2 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E ) -> ( s M ( _I |` T ) ) = s )
100	7, 11, 15, 19, 27, 57, 72, 83, 84, 93, 99	isringd 17754	1 |- ( ( K e. HL /\ W e. H ) -> D e. Ring )

Syntax hints:   -> wi 4   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1870   |-> cmpt 4484   _I cid 4764   `'ccnv 4853   |` cres 4856   o. ccom 4858   ` cfv 5601  (class class class)co 6305   |-> cmpt2 6307   Basecbs 15084   +g cplusg 15153   .rcmulr 15154   Ringcrg 17719   HLchlt 32636   LHypclh 33269   LTrncltrn 33386   TEndoctendo 34039   EDRingRcedring-rN 34041

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-rep 4538  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-cnex 9594  ax-resscn 9595  ax-1cn 9596  ax-icn 9597  ax-addcl 9598  ax-addrcl 9599  ax-mulcl 9600  ax-mulrcl 9601  ax-mulcom 9602  ax-addass 9603  ax-mulass 9604  ax-distr 9605  ax-i2m1 9606  ax-1ne0 9607  ax-1rid 9608  ax-rnegex 9609  ax-rrecex 9610  ax-cnre 9611  ax-pre-lttri 9612  ax-pre-lttrn 9613  ax-pre-ltadd 9614  ax-pre-mulgt0 9615  ax-riotaBAD 32245

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-reu 2789  df-rmo 2790  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-int 4259  df-iun 4304  df-iin 4305  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-1st 6807  df-2nd 6808  df-undef 7028  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-1o 7190  df-oadd 7194  df-er 7371  df-map 7482  df-en 7578  df-dom 7579  df-sdom 7580  df-fin 7581  df-pnf 9676  df-mnf 9677  df-xr 9678  df-ltxr 9679  df-le 9680  df-sub 9861  df-neg 9862  df-nn 10610  df-2 10668  df-3 10669  df-n0 10870  df-z 10938  df-uz 11160  df-fz 11783  df-struct 15086  df-ndx 15087  df-slot 15088  df-base 15089  df-sets 15090  df-plusg 15166  df-mulr 15167  df-0g 15303  df-preset 16128  df-poset 16146  df-plt 16159  df-lub 16175  df-glb 16176  df-join 16177  df-meet 16178  df-p0 16240  df-p1 16241  df-lat 16247  df-clat 16309  df-mgm 16443  df-sgrp 16482  df-mnd 16492  df-grp 16628  df-mgp 17663  df-ring 17721  df-oposet 32462  df-ol 32464  df-oml 32465  df-covers 32552  df-ats 32553  df-atl 32584  df-cvlat 32608  df-hlat 32637  df-llines 32783  df-lplanes 32784  df-lvols 32785  df-lines 32786  df-psubsp 32788  df-pmap 32789  df-padd 33081  df-lhyp 33273  df-laut 33274  df-ldil 33389  df-ltrn 33390  df-trl 33445  df-tendo 34042  df-edring-rN 34043

This theorem is referenced by:  erngdvlem4-rN  34286  erngring-rN  34287