erngdvlem1-rN

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

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		eqid	\|- ( Base ` D ) = ( Base ` D )
10	1 4 5 2 9	erngbase-rN	\|- ( ( K e. HL /\ W e. H ) -> ( Base ` D ) = E )
11	10	eqcomd	\|- ( ( K e. HL /\ W e. H ) -> E = ( Base ` D ) )
12		eqid	\|- ( +g ` D ) = ( +g ` D )
13	1 4 5 2 12	erngfplus-rN	\|- ( ( K e. HL /\ W e. H ) -> ( +g ` D ) = ( a e. E , b e. E \|-> ( f e. T \|-> ( ( a ` f ) o. ( b ` f ) ) ) ) )
14	6 13	eqtr4id	\|- ( ( K e. HL /\ W e. H ) -> P = ( +g ` D ) )
15	1 4 5 6	tendoplcl	\|- ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ t e. E ) -> ( s P t ) e. E )
16	1 4 5 6	tendoplass	\|- ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ u e. E ) ) -> ( ( s P t ) P u ) = ( s P ( t P u ) ) )
17	3 1 4 5 7	tendo0cl	\|- ( ( K e. HL /\ W e. H ) -> O e. E )
18	3 1 4 5 7 6	tendo0pl	\|- ( ( ( K e. HL /\ W e. H ) /\ s e. E ) -> ( O P s ) = s )
19	1 4 5 8	tendoicl	\|- ( ( ( K e. HL /\ W e. H ) /\ s e. E ) -> ( I ` s ) e. E )
20	1 4 5 8 3 6 7	tendoipl	\|- ( ( ( K e. HL /\ W e. H ) /\ s e. E ) -> ( ( I ` s ) P s ) = O )
21	11 14 15 16 17 18 19 20	isgrpd	\|- ( ( K e. HL /\ W e. H ) -> D e. Grp )

Metamath Proof Explorer