Theorem erngdvlem1

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

	Ref	Expression
Hypotheses	ernggrp.h	|- H = ( LHyp ` K )
	ernggrp.d	|- D = ( ( EDRing ` K ) ` W )
	erngdv.b	|- B = ( Base ` K )
	erngdv.t	|- T = ( ( LTrn ` K ) ` W )
	erngdv.e	|- E = ( ( TEndo ` K ) ` W )
	erngdv.p	|- P = ( a e. E , b e. E |-> ( f e. T |-> ( ( a ` f ) o. ( b ` f ) ) ) )
	erngdv.o	|- .0. = ( f e. T |-> ( _I |` B ) )
	erngdv.i	|- I = ( a e. E |-> ( f e. T |-> `' ( a ` f ) ) )
Assertion	erngdvlem1	|- ( ( K e. HL /\ W e. H ) -> D e. Grp )

Proof

Step	Hyp	Ref	Expression
1		ernggrp.h	|- H = ( LHyp ` K )
2		ernggrp.d	|- D = ( ( EDRing ` K ) ` W )
3		erngdv.b	|- B = ( Base ` K )
4		erngdv.t	|- T = ( ( LTrn ` K ) ` W )
5		erngdv.e	|- E = ( ( TEndo ` K ) ` W )
6		erngdv.p	|- P = ( a e. E , b e. E |-> ( f e. T |-> ( ( a ` f ) o. ( b ` f ) ) ) )
7		erngdv.o	|- .0. = ( f e. T |-> ( _I |` B ) )
8		erngdv.i	|- I = ( a e. E |-> ( f e. T |-> `' ( a ` f ) ) )
9		eqid	|- ( Base ` D ) = ( Base ` D )
10	1 4 5 2 9	erngbase	|- ( ( 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	|- ( ( 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 ) -> .0. e. E )
18	3 1 4 5 7 6	tendo0pl	|- ( ( ( K e. HL /\ W e. H ) /\ s e. E ) -> ( .0. 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 ) = .0. )
21	11 14 15 16 17 18 19 20	isgrpd	|- ( ( K e. HL /\ W e. H ) -> D e. Grp )