Theorem erngdvlem2-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 ) ) )
Assertion	erngdvlem2-rN	|- ( ( K e. HL /\ W e. H ) -> D e. Abel )

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		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 2 3 4 5 6 7 8	erngdvlem1-rN	|- ( ( K e. HL /\ W e. H ) -> D e. Grp )
16	1 4 5 6	tendoplcom	|- ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ t e. E ) -> ( s P t ) = ( t P s ) )
17	11 14 15 16	isabld	|- ( ( K e. HL /\ W e. H ) -> D e. Abel )