Theorem mdetunilem9 18989

Description: Lemma for mdetuni 18991. (Contributed by SO, 15-Jul-2018.)

Hypotheses

Ref	Expression
mdetuni.a	|- A = ( N Mat R )
mdetuni.b	|- B = ( Base ` A )
mdetuni.k	|- K = ( Base ` R )
mdetuni.0g	|- .0. = ( 0g ` R )
mdetuni.1r	|- .1. = ( 1r ` R )
mdetuni.pg	|- .+ = ( +g ` R )
mdetuni.tg	|- .x. = ( .r ` R )
mdetuni.n	|- ( ph -> N e. Fin )
mdetuni.r	|- ( ph -> R e. Ring )
mdetuni.ff	|- ( ph -> D : B --> K )
mdetuni.al	|- ( ph -> A. x e. B A. y e. N A. z e. N ( ( y =/= z /\ A. w e. N ( y x w ) = ( z x w ) ) -> ( D ` x ) = .0. ) )
mdetuni.li	|- ( ph -> A. x e. B A. y e. B A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) ) )
mdetuni.sc	|- ( ph -> A. x e. B A. y e. K A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( y .x. ( D ` z ) ) ) )
mdetunilem9.id	|- ( ph -> ( D ` ( 1r ` A ) ) = .0. )
mdetunilem9.y	|- Y = { x | A. y e. B A. z e. ( N ^m N ) ( A. w e. x ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) }

Assertion

Ref	Expression
mdetunilem9	|- ( ph -> D = ( B X. { .0. } ) )

Distinct variable groups:   ph, x, y, z, w   x, B, y, z, w   x, K, y, z, w   x, N, y, z, w   x, D, y, z, w   x, .x. , y, z, w   x, .+ , y, z, w   x, .0. , y, z, w   x, .1. , y, z, w   x, R, y, z, w   x, A, y, z, w

Allowed substitution hints:   Y( x, y, z, w)

Proof of Theorem mdetunilem9

Dummy variables a b c d e are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ral0 3915	. . . 4 |- A. w e. (/) ( a ` w ) = if ( w e. ( _I |` N ) , .1. , .0. )
2		simpr 461	. . . . 5 |- ( ( ph /\ a e. B ) -> a e. B )
3		f1oi 5837	. . . . . . . 8 |- ( _I |` N ) : N -1-1-onto-> N
4		f1of 5802	. . . . . . . 8 |- ( ( _I |` N ) : N -1-1-onto-> N -> ( _I |` N ) : N --> N )
5	3, 4	mp1i 12	. . . . . . 7 |- ( ph -> ( _I |` N ) : N --> N )
6		mdetuni.n	. . . . . . . 8 |- ( ph -> N e. Fin )
7		elmapg 7431	. . . . . . . 8 |- ( ( N e. Fin /\ N e. Fin ) -> ( ( _I |` N ) e. ( N ^m N ) <-> ( _I |` N ) : N --> N ) )
8	6, 6, 7	syl2anc 661	. . . . . . 7 |- ( ph -> ( ( _I |` N ) e. ( N ^m N ) <-> ( _I |` N ) : N --> N ) )
9	5, 8	mpbird 232	. . . . . 6 |- ( ph -> ( _I |` N ) e. ( N ^m N ) )
10	9	adantr 465	. . . . 5 |- ( ( ph /\ a e. B ) -> ( _I |` N ) e. ( N ^m N ) )
11		simplrl 759	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( y e. B /\ z e. ( N ^m N ) ) ) /\ A. w e. ( N X. N ) ( y ` w ) = if ( w e. z , .1. , .0. ) ) -> y e. B )
12		mdetuni.a	. . . . . . . . . . . . . . . . 17 |- A = ( N Mat R )
13		mdetuni.k	. . . . . . . . . . . . . . . . 17 |- K = ( Base ` R )
14		mdetuni.b	. . . . . . . . . . . . . . . . 17 |- B = ( Base ` A )
15	12, 13, 14	matbas2i 18791	. . . . . . . . . . . . . . . 16 |- ( y e. B -> y e. ( K ^m ( N X. N ) ) )
16		elmapi 7438	. . . . . . . . . . . . . . . 16 |- ( y e. ( K ^m ( N X. N ) ) -> y : ( N X. N ) --> K )
17	15, 16	syl 16	. . . . . . . . . . . . . . 15 |- ( y e. B -> y : ( N X. N ) --> K )
18	17	feqmptd 5907	. . . . . . . . . . . . . 14 |- ( y e. B -> y = ( w e. ( N X. N ) |-> ( y ` w ) ) )
19	18	fveq2d 5856	. . . . . . . . . . . . 13 |- ( y e. B -> ( D ` y ) = ( D ` ( w e. ( N X. N ) |-> ( y ` w ) ) ) )
20	11, 19	syl 16	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( y e. B /\ z e. ( N ^m N ) ) ) /\ A. w e. ( N X. N ) ( y ` w ) = if ( w e. z , .1. , .0. ) ) -> ( D ` y ) = ( D ` ( w e. ( N X. N ) |-> ( y ` w ) ) ) )
21		eqid 2441	. . . . . . . . . . . . . 14 |- ( N X. N ) = ( N X. N )
22		mpteq12 4512	. . . . . . . . . . . . . . 15 |- ( ( ( N X. N ) = ( N X. N ) /\ A. w e. ( N X. N ) ( y ` w ) = if ( w e. z , .1. , .0. ) ) -> ( w e. ( N X. N ) |-> ( y ` w ) ) = ( w e. ( N X. N ) |-> if ( w e. z , .1. , .0. ) ) )
23	22	fveq2d 5856	. . . . . . . . . . . . . 14 |- ( ( ( N X. N ) = ( N X. N ) /\ A. w e. ( N X. N ) ( y ` w ) = if ( w e. z , .1. , .0. ) ) -> ( D ` ( w e. ( N X. N ) |-> ( y ` w ) ) ) = ( D ` ( w e. ( N X. N ) |-> if ( w e. z , .1. , .0. ) ) ) )
24	21, 23	mpan 670	. . . . . . . . . . . . 13 |- ( A. w e. ( N X. N ) ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` ( w e. ( N X. N ) |-> ( y ` w ) ) ) = ( D ` ( w e. ( N X. N ) |-> if ( w e. z , .1. , .0. ) ) ) )
25	24	adantl 466	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( y e. B /\ z e. ( N ^m N ) ) ) /\ A. w e. ( N X. N ) ( y ` w ) = if ( w e. z , .1. , .0. ) ) -> ( D ` ( w e. ( N X. N ) |-> ( y ` w ) ) ) = ( D ` ( w e. ( N X. N ) |-> if ( w e. z , .1. , .0. ) ) ) )
26		eleq1 2513	. . . . . . . . . . . . . . . . 17 |- ( a = z -> ( a e. ( N ^m N ) <-> z e. ( N ^m N ) ) )
27	26	anbi2d 703	. . . . . . . . . . . . . . . 16 |- ( a = z -> ( ( ph /\ a e. ( N ^m N ) ) <-> ( ph /\ z e. ( N ^m N ) ) ) )
28		elequ2 1807	. . . . . . . . . . . . . . . . . . . 20 |- ( a = z -> ( w e. a <-> w e. z ) )
29	28	ifbid 3944	. . . . . . . . . . . . . . . . . . 19 |- ( a = z -> if ( w e. a , .1. , .0. ) = if ( w e. z , .1. , .0. ) )
30	29	mpteq2dv 4520	. . . . . . . . . . . . . . . . . 18 |- ( a = z -> ( w e. ( N X. N ) |-> if ( w e. a , .1. , .0. ) ) = ( w e. ( N X. N ) |-> if ( w e. z , .1. , .0. ) ) )
31	30	fveq2d 5856	. . . . . . . . . . . . . . . . 17 |- ( a = z -> ( D ` ( w e. ( N X. N ) |-> if ( w e. a , .1. , .0. ) ) ) = ( D ` ( w e. ( N X. N ) |-> if ( w e. z , .1. , .0. ) ) ) )
32	31	eqeq1d 2443	. . . . . . . . . . . . . . . 16 |- ( a = z -> ( ( D ` ( w e. ( N X. N ) |-> if ( w e. a , .1. , .0. ) ) ) = .0. <-> ( D ` ( w e. ( N X. N ) |-> if ( w e. z , .1. , .0. ) ) ) = .0. ) )
33	27, 32	imbi12d 320	. . . . . . . . . . . . . . 15 |- ( a = z -> ( ( ( ph /\ a e. ( N ^m N ) ) -> ( D ` ( w e. ( N X. N ) |-> if ( w e. a , .1. , .0. ) ) ) = .0. ) <-> ( ( ph /\ z e. ( N ^m N ) ) -> ( D ` ( w e. ( N X. N ) |-> if ( w e. z , .1. , .0. ) ) ) = .0. ) ) )
34		eleq1 2513	. . . . . . . . . . . . . . . . . . . 20 |- ( w = <. b , c >. -> ( w e. a <-> <. b , c >. e. a ) )
35	34	ifbid 3944	. . . . . . . . . . . . . . . . . . 19 |- ( w = <. b , c >. -> if ( w e. a , .1. , .0. ) = if ( <. b , c >. e. a , .1. , .0. ) )
36	35	mpt2mpt 6375	. . . . . . . . . . . . . . . . . 18 |- ( w e. ( N X. N ) |-> if ( w e. a , .1. , .0. ) ) = ( b e. N , c e. N |-> if ( <. b , c >. e. a , .1. , .0. ) )
37		elmapi 7438	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( a e. ( N ^m N ) -> a : N --> N )
38	37	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ a e. ( N ^m N ) ) -> a : N --> N )
39		ffn 5717	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( a : N --> N -> a Fn N )
40	38, 39	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ a e. ( N ^m N ) ) -> a Fn N )
41	40	3ad2ant1 1016	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ a e. ( N ^m N ) ) /\ b e. N /\ c e. N ) -> a Fn N )
42		simp2 996	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ a e. ( N ^m N ) ) /\ b e. N /\ c e. N ) -> b e. N )
43		fnopfvb 5895	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( a Fn N /\ b e. N ) -> ( ( a ` b ) = c <-> <. b , c >. e. a ) )
44	41, 42, 43	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ a e. ( N ^m N ) ) /\ b e. N /\ c e. N ) -> ( ( a ` b ) = c <-> <. b , c >. e. a ) )
45	44	bicomd 201	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ a e. ( N ^m N ) ) /\ b e. N /\ c e. N ) -> ( <. b , c >. e. a <-> ( a ` b ) = c ) )
46	45	ifbid 3944	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ a e. ( N ^m N ) ) /\ b e. N /\ c e. N ) -> if ( <. b , c >. e. a , .1. , .0. ) = if ( ( a ` b ) = c , .1. , .0. ) )
47	46	mpt2eq3dva 6342	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ a e. ( N ^m N ) ) -> ( b e. N , c e. N |-> if ( <. b , c >. e. a , .1. , .0. ) ) = ( b e. N , c e. N |-> if ( ( a ` b ) = c , .1. , .0. ) ) )
48	36, 47	syl5eq 2494	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ a e. ( N ^m N ) ) -> ( w e. ( N X. N ) |-> if ( w e. a , .1. , .0. ) ) = ( b e. N , c e. N |-> if ( ( a ` b ) = c , .1. , .0. ) ) )
49	48	fveq2d 5856	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ a e. ( N ^m N ) ) -> ( D ` ( w e. ( N X. N ) |-> if ( w e. a , .1. , .0. ) ) ) = ( D ` ( b e. N , c e. N |-> if ( ( a ` b ) = c , .1. , .0. ) ) ) )
50		mdetuni.0g	. . . . . . . . . . . . . . . . . 18 |- .0. = ( 0g ` R )
51		mdetuni.1r	. . . . . . . . . . . . . . . . . 18 |- .1. = ( 1r ` R )
52		mdetuni.pg	. . . . . . . . . . . . . . . . . 18 |- .+ = ( +g ` R )
53		mdetuni.tg	. . . . . . . . . . . . . . . . . 18 |- .x. = ( .r ` R )
54		mdetuni.r	. . . . . . . . . . . . . . . . . 18 |- ( ph -> R e. Ring )
55		mdetuni.ff	. . . . . . . . . . . . . . . . . 18 |- ( ph -> D : B --> K )
56		mdetuni.al	. . . . . . . . . . . . . . . . . 18 |- ( ph -> A. x e. B A. y e. N A. z e. N ( ( y =/= z /\ A. w e. N ( y x w ) = ( z x w ) ) -> ( D ` x ) = .0. ) )
57		mdetuni.li	. . . . . . . . . . . . . . . . . 18 |- ( ph -> A. x e. B A. y e. B A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) ) )
58		mdetuni.sc	. . . . . . . . . . . . . . . . . 18 |- ( ph -> A. x e. B A. y e. K A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( y .x. ( D ` z ) ) ) )
59		mdetunilem9.id	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( D ` ( 1r ` A ) ) = .0. )
60	12, 14, 13, 50, 51, 52, 53, 6, 54, 55, 56, 57, 58, 59	mdetunilem8 18988	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ a : N --> N ) -> ( D ` ( b e. N , c e. N |-> if ( ( a ` b ) = c , .1. , .0. ) ) ) = .0. )
61	37, 60	sylan2 474	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ a e. ( N ^m N ) ) -> ( D ` ( b e. N , c e. N |-> if ( ( a ` b ) = c , .1. , .0. ) ) ) = .0. )
62	49, 61	eqtrd 2482	. . . . . . . . . . . . . . 15 |- ( ( ph /\ a e. ( N ^m N ) ) -> ( D ` ( w e. ( N X. N ) |-> if ( w e. a , .1. , .0. ) ) ) = .0. )
63	33, 62	chvarv 1998	. . . . . . . . . . . . . 14 |- ( ( ph /\ z e. ( N ^m N ) ) -> ( D ` ( w e. ( N X. N ) |-> if ( w e. z , .1. , .0. ) ) ) = .0. )
64	63	adantrl 715	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. B /\ z e. ( N ^m N ) ) ) -> ( D ` ( w e. ( N X. N ) |-> if ( w e. z , .1. , .0. ) ) ) = .0. )
65	64	adantr 465	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( y e. B /\ z e. ( N ^m N ) ) ) /\ A. w e. ( N X. N ) ( y ` w ) = if ( w e. z , .1. , .0. ) ) -> ( D ` ( w e. ( N X. N ) |-> if ( w e. z , .1. , .0. ) ) ) = .0. )
66	20, 25, 65	3eqtrd 2486	. . . . . . . . . . 11 |- ( ( ( ph /\ ( y e. B /\ z e. ( N ^m N ) ) ) /\ A. w e. ( N X. N ) ( y ` w ) = if ( w e. z , .1. , .0. ) ) -> ( D ` y ) = .0. )
67	66	ex 434	. . . . . . . . . 10 |- ( ( ph /\ ( y e. B /\ z e. ( N ^m N ) ) ) -> ( A. w e. ( N X. N ) ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) )
68	67	ralrimivva 2862	. . . . . . . . 9 |- ( ph -> A. y e. B A. z e. ( N ^m N ) ( A. w e. ( N X. N ) ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) )
69		xpfi 7789	. . . . . . . . . . 11 |- ( ( N e. Fin /\ N e. Fin ) -> ( N X. N ) e. Fin )
70	6, 6, 69	syl2anc 661	. . . . . . . . . 10 |- ( ph -> ( N X. N ) e. Fin )
71		raleq 3038	. . . . . . . . . . . . 13 |- ( x = ( N X. N ) -> ( A. w e. x ( y ` w ) = if ( w e. z , .1. , .0. ) <-> A. w e. ( N X. N ) ( y ` w ) = if ( w e. z , .1. , .0. ) ) )
72	71	imbi1d 317	. . . . . . . . . . . 12 |- ( x = ( N X. N ) -> ( ( A. w e. x ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) <-> ( A. w e. ( N X. N ) ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) ) )
73	72	2ralbidv 2885	. . . . . . . . . . 11 |- ( x = ( N X. N ) -> ( A. y e. B A. z e. ( N ^m N ) ( A. w e. x ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) <-> A. y e. B A. z e. ( N ^m N ) ( A. w e. ( N X. N ) ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) ) )
74		mdetunilem9.y	. . . . . . . . . . 11 |- Y = { x | A. y e. B A. z e. ( N ^m N ) ( A. w e. x ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) }
75	73, 74	elab2g 3232	. . . . . . . . . 10 |- ( ( N X. N ) e. Fin -> ( ( N X. N ) e. Y <-> A. y e. B A. z e. ( N ^m N ) ( A. w e. ( N X. N ) ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) ) )
76	70, 75	syl 16	. . . . . . . . 9 |- ( ph -> ( ( N X. N ) e. Y <-> A. y e. B A. z e. ( N ^m N ) ( A. w e. ( N X. N ) ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) ) )
77	68, 76	mpbird 232	. . . . . . . 8 |- ( ph -> ( N X. N ) e. Y )
78		ssid 3505	. . . . . . . . 9 |- ( N X. N ) C_ ( N X. N )
79	70	3ad2ant1 1016	. . . . . . . . . . 11 |- ( ( ph /\ ( N X. N ) C_ ( N X. N ) /\ -. (/) e. Y ) -> ( N X. N ) e. Fin )
80		sseq1 3507	. . . . . . . . . . . . . 14 |- ( a = (/) -> ( a C_ ( N X. N ) <-> (/) C_ ( N X. N ) ) )
81	80	3anbi2d 1303	. . . . . . . . . . . . 13 |- ( a = (/) -> ( ( ph /\ a C_ ( N X. N ) /\ -. (/) e. Y ) <-> ( ph /\ (/) C_ ( N X. N ) /\ -. (/) e. Y ) ) )
82		eleq1 2513	. . . . . . . . . . . . . 14 |- ( a = (/) -> ( a e. Y <-> (/) e. Y ) )
83	82	notbid 294	. . . . . . . . . . . . 13 |- ( a = (/) -> ( -. a e. Y <-> -. (/) e. Y ) )
84	81, 83	imbi12d 320	. . . . . . . . . . . 12 |- ( a = (/) -> ( ( ( ph /\ a C_ ( N X. N ) /\ -. (/) e. Y ) -> -. a e. Y ) <-> ( ( ph /\ (/) C_ ( N X. N ) /\ -. (/) e. Y ) -> -. (/) e. Y ) ) )
85		sseq1 3507	. . . . . . . . . . . . . 14 |- ( a = b -> ( a C_ ( N X. N ) <-> b C_ ( N X. N ) ) )
86	85	3anbi2d 1303	. . . . . . . . . . . . 13 |- ( a = b -> ( ( ph /\ a C_ ( N X. N ) /\ -. (/) e. Y ) <-> ( ph /\ b C_ ( N X. N ) /\ -. (/) e. Y ) ) )
87		eleq1 2513	. . . . . . . . . . . . . 14 |- ( a = b -> ( a e. Y <-> b e. Y ) )
88	87	notbid 294	. . . . . . . . . . . . 13 |- ( a = b -> ( -. a e. Y <-> -. b e. Y ) )
89	86, 88	imbi12d 320	. . . . . . . . . . . 12 |- ( a = b -> ( ( ( ph /\ a C_ ( N X. N ) /\ -. (/) e. Y ) -> -. a e. Y ) <-> ( ( ph /\ b C_ ( N X. N ) /\ -. (/) e. Y ) -> -. b e. Y ) ) )
90		sseq1 3507	. . . . . . . . . . . . . 14 |- ( a = ( b u. { c } ) -> ( a C_ ( N X. N ) <-> ( b u. { c } ) C_ ( N X. N ) ) )
91	90	3anbi2d 1303	. . . . . . . . . . . . 13 |- ( a = ( b u. { c } ) -> ( ( ph /\ a C_ ( N X. N ) /\ -. (/) e. Y ) <-> ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ -. (/) e. Y ) ) )
92		eleq1 2513	. . . . . . . . . . . . . 14 |- ( a = ( b u. { c } ) -> ( a e. Y <-> ( b u. { c } ) e. Y ) )
93	92	notbid 294	. . . . . . . . . . . . 13 |- ( a = ( b u. { c } ) -> ( -. a e. Y <-> -. ( b u. { c } ) e. Y ) )
94	91, 93	imbi12d 320	. . . . . . . . . . . 12 |- ( a = ( b u. { c } ) -> ( ( ( ph /\ a C_ ( N X. N ) /\ -. (/) e. Y ) -> -. a e. Y ) <-> ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ -. (/) e. Y ) -> -. ( b u. { c } ) e. Y ) ) )
95		sseq1 3507	. . . . . . . . . . . . . 14 |- ( a = ( N X. N ) -> ( a C_ ( N X. N ) <-> ( N X. N ) C_ ( N X. N ) ) )
96	95	3anbi2d 1303	. . . . . . . . . . . . 13 |- ( a = ( N X. N ) -> ( ( ph /\ a C_ ( N X. N ) /\ -. (/) e. Y ) <-> ( ph /\ ( N X. N ) C_ ( N X. N ) /\ -. (/) e. Y ) ) )
97		eleq1 2513	. . . . . . . . . . . . . 14 |- ( a = ( N X. N ) -> ( a e. Y <-> ( N X. N ) e. Y ) )
98	97	notbid 294	. . . . . . . . . . . . 13 |- ( a = ( N X. N ) -> ( -. a e. Y <-> -. ( N X. N ) e. Y ) )
99	96, 98	imbi12d 320	. . . . . . . . . . . 12 |- ( a = ( N X. N ) -> ( ( ( ph /\ a C_ ( N X. N ) /\ -. (/) e. Y ) -> -. a e. Y ) <-> ( ( ph /\ ( N X. N ) C_ ( N X. N ) /\ -. (/) e. Y ) -> -. ( N X. N ) e. Y ) ) )
100		simp3 997	. . . . . . . . . . . 12 |- ( ( ph /\ (/) C_ ( N X. N ) /\ -. (/) e. Y ) -> -. (/) e. Y )
101		ssun1 3649	. . . . . . . . . . . . . . . 16 |- b C_ ( b u. { c } )
102		sstr2 3493	. . . . . . . . . . . . . . . 16 |- ( b C_ ( b u. { c } ) -> ( ( b u. { c } ) C_ ( N X. N ) -> b C_ ( N X. N ) ) )
103	101, 102	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( ( b u. { c } ) C_ ( N X. N ) -> b C_ ( N X. N ) )
104	103	3anim2i 1182	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ -. (/) e. Y ) -> ( ph /\ b C_ ( N X. N ) /\ -. (/) e. Y ) )
105	104	imim1i 58	. . . . . . . . . . . . 13 |- ( ( ( ph /\ b C_ ( N X. N ) /\ -. (/) e. Y ) -> -. b e. Y ) -> ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ -. (/) e. Y ) -> -. b e. Y ) )
106		simpl1 998	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ ( b u. { c } ) e. Y ) /\ ( ( a e. B /\ d e. ( N ^m N ) ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> ph )
107		simpl2 999	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ ( b u. { c } ) e. Y ) /\ ( ( a e. B /\ d e. ( N ^m N ) ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> ( b u. { c } ) C_ ( N X. N ) )
108		simprll 761	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ ( b u. { c } ) e. Y ) /\ ( ( a e. B /\ d e. ( N ^m N ) ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> a e. B )
109	12, 13, 14	matbas2i 18791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( a e. B -> a e. ( K ^m ( N X. N ) ) )
110		elmapi 7438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( a e. ( K ^m ( N X. N ) ) -> a : ( N X. N ) --> K )
111	109, 110	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( a e. B -> a : ( N X. N ) --> K )
112	111	3ad2ant3 1018	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> a : ( N X. N ) --> K )
113	112	feqmptd 5907	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> a = ( e e. ( N X. N ) |-> ( a ` e ) ) )
114	113	reseq1d 5258	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( a |` ( { ( 1st ` c ) } X. N ) ) = ( ( e e. ( N X. N ) |-> ( a ` e ) ) |` ( { ( 1st ` c ) } X. N ) ) )
115	54	3ad2ant1 1016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> R e. Ring )
116		ringgrp 17071	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( R e. Ring -> R e. Grp )
117	115, 116	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> R e. Grp )
118	117	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> R e. Grp )
119	112	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> a : ( N X. N ) --> K )
120		simp2 996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( b u. { c } ) C_ ( N X. N ) )
121	120	unssbd 3664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> { c } C_ ( N X. N ) )
122		vex 3096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- c e. _V
123	122	snss 4135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( c e. ( N X. N ) <-> { c } C_ ( N X. N ) )
124	121, 123	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> c e. ( N X. N ) )
125		xp1st 6811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( c e. ( N X. N ) -> ( 1st ` c ) e. N )
126	124, 125	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( 1st ` c ) e. N )
127	126	snssd 4156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> { ( 1st ` c ) } C_ N )
128		xpss1 5097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( { ( 1st ` c ) } C_ N -> ( { ( 1st ` c ) } X. N ) C_ ( N X. N ) )
129	127, 128	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( { ( 1st ` c ) } X. N ) C_ ( N X. N ) )
130	129	sselda 3486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> e e. ( N X. N ) )
131	119, 130	ffvelrnd 6013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> ( a ` e ) e. K )
132	13, 51	ringidcl 17087	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( R e. Ring -> .1. e. K )
133	115, 132	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> .1. e. K )
134	13, 50	ring0cl 17088	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( R e. Ring -> .0. e. K )
135	115, 134	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> .0. e. K )
136	133, 135	ifcld 3965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> if ( e e. d , .1. , .0. ) e. K )
137	136	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> if ( e e. d , .1. , .0. ) e. K )
138		eqid 2441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( -g ` R ) = ( -g ` R )
139	13, 52, 138	grpnpcan 15999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( R e. Grp /\ ( a ` e ) e. K /\ if ( e e. d , .1. , .0. ) e. K ) -> ( ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) .+ if ( e e. d , .1. , .0. ) ) = ( a ` e ) )
140	118, 131, 137, 139	syl3anc 1227	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> ( ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) .+ if ( e e. d , .1. , .0. ) ) = ( a ` e ) )
141	140	eqcomd 2449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> ( a ` e ) = ( ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) .+ if ( e e. d , .1. , .0. ) ) )
142	141	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) /\ e = c ) -> ( a ` e ) = ( ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) .+ if ( e e. d , .1. , .0. ) ) )
143		iftrue 3928	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( e = c -> if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) = ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) )
144		iftrue 3928	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( e = c -> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) = if ( e e. d , .1. , .0. ) )
145	143, 144	oveq12d 6295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( e = c -> ( if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) .+ if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) = ( ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) .+ if ( e e. d , .1. , .0. ) ) )
146	145	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) /\ e = c ) -> ( if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) .+ if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) = ( ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) .+ if ( e e. d , .1. , .0. ) ) )
147	142, 146	eqtr4d 2485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) /\ e = c ) -> ( a ` e ) = ( if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) .+ if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) )
148	13, 52, 50	grplid 15949	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( R e. Grp /\ ( a ` e ) e. K ) -> ( .0. .+ ( a ` e ) ) = ( a ` e ) )
149	118, 131, 148	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> ( .0. .+ ( a ` e ) ) = ( a ` e ) )
150	149	eqcomd 2449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> ( a ` e ) = ( .0. .+ ( a ` e ) ) )
151	150	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) /\ -. e = c ) -> ( a ` e ) = ( .0. .+ ( a ` e ) ) )
152		iffalse 3931	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( -. e = c -> if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) = .0. )
153		iffalse 3931	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( -. e = c -> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) = ( a ` e ) )
154	152, 153	oveq12d 6295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( -. e = c -> ( if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) .+ if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) = ( .0. .+ ( a ` e ) ) )
155	154	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) /\ -. e = c ) -> ( if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) .+ if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) = ( .0. .+ ( a ` e ) ) )
156	151, 155	eqtr4d 2485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) /\ -. e = c ) -> ( a ` e ) = ( if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) .+ if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) )
157	147, 156	pm2.61dan 789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> ( a ` e ) = ( if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) .+ if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) )
158	157	mpteq2dva 4519	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( e e. ( { ( 1st ` c ) } X. N ) |-> ( a ` e ) ) = ( e e. ( { ( 1st ` c ) } X. N ) |-> ( if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) .+ if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) )
159		snfi 7594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- { ( 1st ` c ) } e. Fin
160	6	3ad2ant1 1016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> N e. Fin )
161		xpfi 7789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( { ( 1st ` c ) } e. Fin /\ N e. Fin ) -> ( { ( 1st ` c ) } X. N ) e. Fin )
162	159, 160, 161	sylancr 663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( { ( 1st ` c ) } X. N ) e. Fin )
163		ovex 6305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) e. _V
164		fvex 5862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( 0g ` R ) e. _V
165	50, 164	eqeltri 2525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- .0. e. _V
166	163, 165	ifex 3991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) e. _V
167	166	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) e. _V )
168		fvex 5862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( 1r ` R ) e. _V
169	51, 168	eqeltri 2525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- .1. e. _V
170	169, 165	ifex 3991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- if ( e e. d , .1. , .0. ) e. _V
171		fvex 5862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( a ` e ) e. _V
172	170, 171	ifex 3991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) e. _V
173	172	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) e. _V )
174		xp1st 6811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( e e. ( { ( 1st ` c ) } X. N ) -> ( 1st ` e ) e. { ( 1st ` c ) } )
175		elsni 4035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( 1st ` e ) e. { ( 1st ` c ) } -> ( 1st ` e ) = ( 1st ` c ) )
176		iftrue 3928	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( 1st ` e ) = ( 1st ` c ) -> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) = if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) )
177	174, 175, 176	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( e e. ( { ( 1st ` c ) } X. N ) -> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) = if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) )
178	177	mpteq2ia 4515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( e e. ( { ( 1st ` c ) } X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) = ( e e. ( { ( 1st ` c ) } X. N ) |-> if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) )
179	178	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( e e. ( { ( 1st ` c ) } X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) = ( e e. ( { ( 1st ` c ) } X. N ) |-> if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) ) )
180		eqidd 2442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( e e. ( { ( 1st ` c ) } X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) = ( e e. ( { ( 1st ` c ) } X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) )
181	162, 167, 173, 179, 180	offval2 6537	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( e e. ( { ( 1st ` c ) } X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) oF .+ ( e e. ( { ( 1st ` c ) } X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) = ( e e. ( { ( 1st ` c ) } X. N ) |-> ( if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) .+ if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) )
182	158, 181	eqtr4d 2485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( e e. ( { ( 1st ` c ) } X. N ) |-> ( a ` e ) ) = ( ( e e. ( { ( 1st ` c ) } X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) oF .+ ( e e. ( { ( 1st ` c ) } X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) )
183	129	resmptd 5311	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( e e. ( N X. N ) |-> ( a ` e ) ) |` ( { ( 1st ` c ) } X. N ) ) = ( e e. ( { ( 1st ` c ) } X. N ) |-> ( a ` e ) ) )
184	129	resmptd 5311	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) |` ( { ( 1st ` c ) } X. N ) ) = ( e e. ( { ( 1st ` c ) } X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) )
185	129	resmptd 5311	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( { ( 1st ` c ) } X. N ) ) = ( e e. ( { ( 1st ` c ) } X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) )
186	184, 185	oveq12d 6295	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) |` ( { ( 1st ` c ) } X. N ) ) oF .+ ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( { ( 1st ` c ) } X. N ) ) ) = ( ( e e. ( { ( 1st ` c ) } X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) oF .+ ( e e. ( { ( 1st ` c ) } X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) )
187	182, 183, 186	3eqtr4d 2492	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( e e. ( N X. N ) |-> ( a ` e ) ) |` ( { ( 1st ` c ) } X. N ) ) = ( ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) |` ( { ( 1st ` c ) } X. N ) ) oF .+ ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( { ( 1st ` c ) } X. N ) ) ) )
188	114, 187	eqtrd 2482	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( a |` ( { ( 1st ` c ) } X. N ) ) = ( ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) |` ( { ( 1st ` c ) } X. N ) ) oF .+ ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( { ( 1st ` c ) } X. N ) ) ) )
189	113	reseq1d 5258	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( a |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) = ( ( e e. ( N X. N ) |-> ( a ` e ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) )
190		xp1st 6811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( e e. ( ( N \ { ( 1st ` c ) } ) X. N ) -> ( 1st ` e ) e. ( N \ { ( 1st ` c ) } ) )
191		eldifsni 4137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( 1st ` e ) e. ( N \ { ( 1st ` c ) } ) -> ( 1st ` e ) =/= ( 1st ` c ) )
192	190, 191	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( e e. ( ( N \ { ( 1st ` c ) } ) X. N ) -> ( 1st ` e ) =/= ( 1st ` c ) )
193	192	neneqd 2643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( e e. ( ( N \ { ( 1st ` c ) } ) X. N ) -> -. ( 1st ` e ) = ( 1st ` c ) )
194	193	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( ( N \ { ( 1st ` c ) } ) X. N ) ) -> -. ( 1st ` e ) = ( 1st ` c ) )
195	194	iffalsed 3933	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( ( N \ { ( 1st ` c ) } ) X. N ) ) -> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) = ( a ` e ) )
196	195	mpteq2dva 4519	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( e e. ( ( N \ { ( 1st ` c ) } ) X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) = ( e e. ( ( N \ { ( 1st ` c ) } ) X. N ) |-> ( a ` e ) ) )
197		difss 3613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( N \ { ( 1st ` c ) } ) C_ N
198		xpss1 5097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( N \ { ( 1st ` c ) } ) C_ N -> ( ( N \ { ( 1st ` c ) } ) X. N ) C_ ( N X. N ) )
199	197, 198	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( N \ { ( 1st ` c ) } ) X. N ) C_ ( N X. N )
200		resmpt 5309	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( N \ { ( 1st ` c ) } ) X. N ) C_ ( N X. N ) -> ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) = ( e e. ( ( N \ { ( 1st ` c ) } ) X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) )
201	199, 200	mp1i 12	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) = ( e e. ( ( N \ { ( 1st ` c ) } ) X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) )
202		resmpt 5309	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( N \ { ( 1st ` c ) } ) X. N ) C_ ( N X. N ) -> ( ( e e. ( N X. N ) |-> ( a ` e ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) = ( e e. ( ( N \ { ( 1st ` c ) } ) X. N ) |-> ( a ` e ) ) )
203	199, 202	mp1i 12	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( e e. ( N X. N ) |-> ( a ` e ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) = ( e e. ( ( N \ { ( 1st ` c ) } ) X. N ) |-> ( a ` e ) ) )
204	196, 201, 203	3eqtr4rd 2493	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( e e. ( N X. N ) |-> ( a ` e ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) = ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) )
205	189, 204	eqtrd 2482	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( a |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) = ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) )
206		fveq2 5852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( e = c -> ( 1st ` e ) = ( 1st ` c ) )
207	194, 206	nsyl 121	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( ( N \ { ( 1st ` c ) } ) X. N ) ) -> -. e = c )
208	207	iffalsed 3933	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( ( N \ { ( 1st ` c ) } ) X. N ) ) -> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) = ( a ` e ) )
209	208	mpteq2dva 4519	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( e e. ( ( N \ { ( 1st ` c ) } ) X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) = ( e e. ( ( N \ { ( 1st ` c ) } ) X. N ) |-> ( a ` e ) ) )
210		resmpt 5309	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( N \ { ( 1st ` c ) } ) X. N ) C_ ( N X. N ) -> ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) = ( e e. ( ( N \ { ( 1st ` c ) } ) X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) )
211	199, 210	mp1i 12	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) = ( e e. ( ( N \ { ( 1st ` c ) } ) X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) )
212	209, 211, 203	3eqtr4rd 2493	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( e e. ( N X. N ) |-> ( a ` e ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) = ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) )
213	189, 212	eqtrd 2482	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( a |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) = ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) )
214	136	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( N X. N ) ) -> if ( e e. d , .1. , .0. ) e. K )
215	112	ffvelrnda 6012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( N X. N ) ) -> ( a ` e ) e. K )
216	214, 215	ifcld 3965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( N X. N ) ) -> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) e. K )
217		eqid 2441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) = ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) )
218	216, 217	fmptd 6036	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) : ( N X. N ) --> K )
219		fvex 5862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( Base ` R ) e. _V
220	13, 219	eqeltri 2525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- K e. _V
221	69	anidms 645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( N e. Fin -> ( N X. N ) e. Fin )
222	160, 221	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( N X. N ) e. Fin )
223		elmapg 7431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( K e. _V /\ ( N X. N ) e. Fin ) -> ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) e. ( K ^m ( N X. N ) ) <-> ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) : ( N X. N ) --> K ) )
224	220, 222, 223	sylancr 663	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) e. ( K ^m ( N X. N ) ) <-> ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) : ( N X. N ) --> K ) )
225	218, 224	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) e. ( K ^m ( N X. N ) ) )
226	12, 13	matbas2 18790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( N e. Fin /\ R e. Ring ) -> ( K ^m ( N X. N ) ) = ( Base ` A ) )
227	160, 115, 226	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( K ^m ( N X. N ) ) = ( Base ` A ) )
228	227, 14	syl6eqr 2500	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( K ^m ( N X. N ) ) = B )
229	225, 228	eleqtrd 2531	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) e. B )
230		simp3 997	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> a e. B )
231	117	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( N X. N ) ) -> R e. Grp )
232	13, 138	grpsubcl 15987	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( R e. Grp /\ ( a ` e ) e. K /\ if ( e e. d , .1. , .0. ) e. K ) -> ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) e. K )
233	231, 215, 214, 232	syl3anc 1227	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( N X. N ) ) -> ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) e. K )
234	135	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( N X. N ) ) -> .0. e. K )
235	233, 234	ifcld 3965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( N X. N ) ) -> if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) e. K )
236	235, 215	ifcld 3965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( N X. N ) ) -> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) e. K )
237		eqid 2441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) )
238	236, 237	fmptd 6036	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) : ( N X. N ) --> K )
239		elmapg 7431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( K e. _V /\ ( N X. N ) e. Fin ) -> ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) e. ( K ^m ( N X. N ) ) <-> ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) : ( N X. N ) --> K ) )
240	220, 222, 239	sylancr 663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) e. ( K ^m ( N X. N ) ) <-> ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) : ( N X. N ) --> K ) )
241	238, 240	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) e. ( K ^m ( N X. N ) ) )
242	241, 228	eleqtrd 2531	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) e. B )
243	57	3ad2ant1 1016	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> A. x e. B A. y e. B A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) ) )
244		reseq1 5253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( x = a -> ( x |` ( { w } X. N ) ) = ( a |` ( { w } X. N ) ) )
245	244	eqeq1d 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( x = a -> ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) <-> ( a |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) ) )
246		reseq1 5253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( x = a -> ( x |` ( ( N \ { w } ) X. N ) ) = ( a |` ( ( N \ { w } ) X. N ) ) )
247	246	eqeq1d 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( x = a -> ( ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) <-> ( a |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) ) )
248	246	eqeq1d 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( x = a -> ( ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) <-> ( a |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) )
249	245, 247, 248	3anbi123d 1298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( x = a -> ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) <-> ( ( a |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( a |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( a |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) ) )
250		fveq2 5852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( x = a -> ( D ` x ) = ( D ` a ) )
251	250	eqeq1d 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( x = a -> ( ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) <-> ( D ` a ) = ( ( D ` y ) .+ ( D ` z ) ) ) )
252	249, 251	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x = a -> ( ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) ) <-> ( ( ( a |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( a |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( a |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` a ) = ( ( D ` y ) .+ ( D ` z ) ) ) ) )
253	252	2ralbidv 2885	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x = a -> ( A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) ) <-> A. z e. B A. w e. N ( ( ( a |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( a |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( a |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` a ) = ( ( D ` y ) .+ ( D ` z ) ) ) ) )
254		reseq1 5253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( y = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) -> ( y |` ( { w } X. N ) ) = ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) |` ( { w } X. N ) ) )
255	254	oveq1d 6292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( y = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) -> ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) = ( ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) )
256	255	eqeq2d 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( y = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) -> ( ( a |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) <-> ( a |` ( { w } X. N ) ) = ( ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) ) )
257		reseq1 5253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( y = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) -> ( y |` ( ( N \ { w } ) X. N ) ) = ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) |` ( ( N \ { w } ) X. N ) ) )
258	257	eqeq2d 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( y = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) -> ( ( a |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) <-> ( a |` ( ( N \ { w } ) X. N ) ) = ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) |` ( ( N \ { w } ) X. N ) ) ) )
259	256, 258	3anbi12d 1299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( y = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) -> ( ( ( a |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( a |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( a |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) <-> ( ( a |` ( { w } X. N ) ) = ( ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( a |` ( ( N \ { w } ) X. N ) ) = ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) |` ( ( N \ { w } ) X. N ) ) /\ ( a |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) ) )
260		fveq2 5852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( y = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) -> ( D ` y ) = ( D ` ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) ) )
261	260	oveq1d 6292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( y = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) -> ( ( D ` y ) .+ ( D ` z ) ) = ( ( D ` ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) , ( a ` e ) ) ) ) .+ ( D ` z ) )