Theorem erngdvlem3-rN 36195

Description: Lemma for eringring 36189. (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 2467	. . . 4 |- ( Base ` D ) = ( Base ` D )
6	1, 2, 3, 4, 5	erngbase-rN 36006	. . 3 |- ( ( K e. HL /\ W e. H ) -> ( Base ` D ) = E )
7	6	eqcomd 2475	. 2 |- ( ( K e. HL /\ W e. H ) -> E = ( Base ` D ) )
8		eqid 2467	. . . 4 |- ( +g ` D ) = ( +g ` D )
9	1, 2, 3, 4, 8	erngfplus-rN 36007	. . 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 2527	. 2 |- ( ( K e. HL /\ W e. H ) -> P = ( +g ` D ) )
12		eqid 2467	. . . 4 |- ( .r ` D ) = ( .r ` D )
13	1, 2, 3, 4, 12	erngfmul-rN 36010	. . 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 2527	. 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 36193	. 2 |- ( ( K e. HL /\ W e. H ) -> D e. Grp )
20	15	oveqd 6312	. . . . 5 |- ( ( K e. HL /\ W e. H ) -> ( s M t ) = ( s ( .r ` D ) t ) )
21	20	3ad2ant1 1017	. . . 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 36011	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E ) ) -> ( s ( .r ` D ) t ) = ( t o. s ) )
23	22	3impb 1192	. . . 4 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ t e. E ) -> ( s ( .r ` D ) t ) = ( t o. s ) )
24	21, 23	eqtrd 2508	. . 3 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ t e. E ) -> ( s M t ) = ( t o. s ) )
25	1, 3	tendococl 35969	. . . 4 |- ( ( ( K e. HL /\ W e. H ) /\ t e. E /\ s e. E ) -> ( t o. s ) e. E )
26	25	3com23 1202	. . 3 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ t e. E ) -> ( t o. s ) e. E )
27	24, 26	eqeltrd 2555	. 2 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ t e. E ) -> ( s M t ) e. E )
28	15	proplem3 14963	. . . . 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 36011	. . . . . 6 |- ( ( ( K e. HL /\ W e. H ) /\ ( t e. E /\ u e. E ) ) -> ( t ( .r ` D ) u ) = ( u o. t ) )
30	29	3adantr1 1155	. . . . 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 2508	. . . 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 5170	. . 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 6312	. . . . 5 |- ( ( K e. HL /\ W e. H ) -> ( s M ( t M u ) ) = ( s ( .r ` D ) ( t M u ) ) )
34	33	adantr 465	. . . 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 457	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ u e. E ) ) -> ( K e. HL /\ W e. H ) )
36		simpr1 1002	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ u e. E ) ) -> s e. E )
37		simpr3 1004	. . . . . . 7 |- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ u e. E ) ) -> u e. E )
38		simpr2 1003	. . . . . . 7 |- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ u e. E ) ) -> t e. E )
39	1, 3	tendococl 35969	. . . . . . 7 |- ( ( ( K e. HL /\ W e. H ) /\ u e. E /\ t e. E ) -> ( u o. t ) e. E )
40	35, 37, 38, 39	syl3anc 1228	. . . . . 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 2555	. . . . 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 36011	. . . . 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 1226	. . . 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 2508	. . 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 6312	. . . . . 6 |- ( ( K e. HL /\ W e. H ) -> ( ( s M t ) M u ) = ( ( s M t ) ( .r ` D ) u ) )
46	45	adantr 465	. . . . 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 1207	. . . . . 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 36011	. . . . . 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 1226	. . . . 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	proplem3 14963	. . . . . . 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 1157	. . . . . . 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 2508	. . . . . 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 5171	. . . . 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 2512	. . . 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 5532	. . . 4 |- ( ( u o. t ) o. s ) = ( u o. ( t o. s ) )
56	54, 55	syl6eqr 2526	. . 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 2519	. 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 35982	. . . 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 1230	. . 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 6312	. . . . 5 |- ( ( K e. HL /\ W e. H ) -> ( s M ( t P u ) ) = ( s ( .r ` D ) ( t P u ) ) )
61	60	adantr 465	. . . 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 35978	. . . . . 6 |- ( ( ( K e. HL /\ W e. H ) /\ t e. E /\ u e. E ) -> ( t P u ) e. E )
63	35, 38, 37, 62	syl3anc 1228	. . . . 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 36011	. . . . 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 1226	. . . 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 2508	. . 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	proplem3 14963	. . . . 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 36011	. . . . . 6 |- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ u e. E ) ) -> ( s ( .r ` D ) u ) = ( u o. s ) )
69	68	3adantr2 1156	. . . . 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 2508	. . . 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 6313	. . 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 2518	. 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 35981	. . . 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 1230	. . 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 465	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ u e. E ) ) -> M = ( .r ` D ) )
76	75	oveqd 6312	. . . 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 35978	. . . . . 6 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ t e. E ) -> ( s P t ) e. E )
78	77	3adant3r3 1207	. . . . 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 36011	. . . . 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 1226	. . . 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 2508	. . 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 6313	. . 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 2518	. 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 35966	. 2 |- ( ( K e. HL /\ W e. H ) -> ( _I |` T ) e. E )
85	15	oveqd 6312	. . . 4 |- ( ( K e. HL /\ W e. H ) -> ( ( _I |` T ) M s ) = ( ( _I |` T ) ( .r ` D ) s ) )
86	85	adantr 465	. . 3 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E ) -> ( ( _I |` T ) M s ) = ( ( _I |` T ) ( .r ` D ) s ) )
87		simpl 457	. . . 4 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E ) -> ( K e. HL /\ W e. H ) )
88	84	adantr 465	. . . 4 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E ) -> ( _I |` T ) e. E )
89		simpr 461	. . . 4 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E ) -> s e. E )
90	1, 2, 3, 4, 12	erngmul-rN 36011	. . . 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 1226	. . 3 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E ) -> ( ( _I |` T ) ( .r ` D ) s ) = ( s o. ( _I |` T ) ) )
92	1, 2, 3	tendo1mulr 35968	. . 3 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E ) -> ( s o. ( _I |` T ) ) = s )
93	86, 91, 92	3eqtrd 2512	. 2 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E ) -> ( ( _I |` T ) M s ) = s )
94	15	oveqd 6312	. . . 4 |- ( ( K e. HL /\ W e. H ) -> ( s M ( _I |` T ) ) = ( s ( .r ` D ) ( _I |` T ) ) )
95	94	adantr 465	. . 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 36011	. . . 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 1226	. . 3 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E ) -> ( s ( .r ` D ) ( _I |` T ) ) = ( ( _I |` T ) o. s ) )
98	1, 2, 3	tendo1mul 35967	. . 3 |- ( ( ( K e. HL /\ W e. H ) /\ s e. E ) -> ( ( _I |` T ) o. s ) = s )
99	95, 97, 98	3eqtrd 2512	. 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 17105	1 |- ( ( K e. HL /\ W e. H ) -> D e. Ring )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 973   = wceq 1379   e. wcel 1767   |-> cmpt 4511   _I cid 4796   `'ccnv 5004   |` cres 5007   o. ccom 5009   ` cfv 5594  (class class class)co 6295   |-> cmpt2 6297   Basecbs 14507   +g cplusg 14572   .rcmulr 14573   Ringcrg 17070   HLchlt 34548   LHypclh 35181   LTrncltrn 35298   TEndoctendo 35949   EDRingRcedring-rN 35951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-cnex 9560  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577  ax-pre-lttri 9578  ax-pre-lttrn 9579  ax-pre-ltadd 9580  ax-pre-mulgt0 9581  ax-riotaBAD 34157

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-int 4289  df-iun 4333  df-iin 4334  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6696  df-1st 6795  df-2nd 6796  df-undef 7014  df-recs 7054  df-rdg 7088  df-1o 7142  df-oadd 7146  df-er 7323  df-map 7434  df-en 7529  df-dom 7530  df-sdom 7531  df-fin 7532  df-pnf 9642  df-mnf 9643  df-xr 9644  df-ltxr 9645  df-le 9646  df-sub 9819  df-neg 9820  df-nn 10549  df-2 10606  df-3 10607  df-n0 10808  df-z 10877  df-uz 11095  df-fz 11685  df-struct 14509  df-ndx 14510  df-slot 14511  df-base 14512  df-sets 14513  df-plusg 14585  df-mulr 14586  df-0g 14714  df-poset 15450  df-plt 15462  df-lub 15478  df-glb 15479  df-join 15480  df-meet 15481  df-p0 15543  df-p1 15544  df-lat 15550  df-clat 15612  df-mgm 15746  df-sgrp 15785  df-mnd 15795  df-grp 15929  df-mgp 17014  df-ring 17072  df-oposet 34374  df-ol 34376  df-oml 34377  df-covers 34464  df-ats 34465  df-atl 34496  df-cvlat 34520  df-hlat 34549  df-llines 34695  df-lplanes 34696  df-lvols 34697  df-lines 34698  df-psubsp 34700  df-pmap 34701  df-padd 34993  df-lhyp 35185  df-laut 35186  df-ldil 35301  df-ltrn 35302  df-trl 35356  df-tendo 35952  df-edring-rN 35953

This theorem is referenced by:  erngdvlem4-rN  36196  erngring-rN  36197