Theorem mdetunilem9 18882

Description: Lemma for mdetuni 18884. (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 3925	. . . 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 5842	. . . . . . . 8 |- ( _I |` N ) : N -1-1-onto-> N
4		f1of 5807	. . . . . . . 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 7423	. . . . . . . 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 18684	. . . . . . . . . . . . . . . 16 |- ( y e. B -> y e. ( K ^m ( N X. N ) ) )
16		elmapi 7430	. . . . . . . . . . . . . . . 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 5911	. . . . . . . . . . . . . 14 |- ( y e. B -> y = ( w e. ( N X. N ) |-> ( y ` w ) ) )
19	18	fveq2d 5861	. . . . . . . . . . . . 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 2460	. . . . . . . . . . . . . 14 |- ( N X. N ) = ( N X. N )
22		mpteq12 4519	. . . . . . . . . . . . . . 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 5861	. . . . . . . . . . . . . 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 2532	. . . . . . . . . . . . . . . . 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 1767	. . . . . . . . . . . . . . . . . . . 20 |- ( a = z -> ( w e. a <-> w e. z ) )
29	28	ifbid 3954	. . . . . . . . . . . . . . . . . . 19 |- ( a = z -> if ( w e. a , .1. , .0. ) = if ( w e. z , .1. , .0. ) )
30	29	mpteq2dv 4527	. . . . . . . . . . . . . . . . . 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 5861	. . . . . . . . . . . . . . . . 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 2462	. . . . . . . . . . . . . . . 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 2532	. . . . . . . . . . . . . . . . . . . 20 |- ( w = <. b , c >. -> ( w e. a <-> <. b , c >. e. a ) )
35	34	ifbid 3954	. . . . . . . . . . . . . . . . . . 19 |- ( w = <. b , c >. -> if ( w e. a , .1. , .0. ) = if ( <. b , c >. e. a , .1. , .0. ) )
36	35	mpt2mpt 6369	. . . . . . . . . . . . . . . . . 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 7430	. . . . . . . . . . . . . . . . . . . . . . . . 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 5722	. . . . . . . . . . . . . . . . . . . . . . . 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 1012	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ a e. ( N ^m N ) ) /\ b e. N /\ c e. N ) -> a Fn N )
42		simp2 992	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ a e. ( N ^m N ) ) /\ b e. N /\ c e. N ) -> b e. N )
43		fnopfvb 5900	. . . . . . . . . . . . . . . . . . . . . 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 3954	. . . . . . . . . . . . . . . . . . 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 6336	. . . . . . . . . . . . . . . . . 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 2513	. . . . . . . . . . . . . . . . 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 5861	. . . . . . . . . . . . . . . 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 18881	. . . . . . . . . . . . . . . . 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 2501	. . . . . . . . . . . . . . 15 |- ( ( ph /\ a e. ( N ^m N ) ) -> ( D ` ( w e. ( N X. N ) |-> if ( w e. a , .1. , .0. ) ) ) = .0. )
63	33, 62	chvarv 1976	. . . . . . . . . . . . . 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 2505	. . . . . . . . . . 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 2878	. . . . . . . . 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 7780	. . . . . . . . . . 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 3051	. . . . . . . . . . . . 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 2901	. . . . . . . . . . 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 3245	. . . . . . . . . 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 3516	. . . . . . . . 9 |- ( N X. N ) C_ ( N X. N )
79	70	3ad2ant1 1012	. . . . . . . . . . 11 |- ( ( ph /\ ( N X. N ) C_ ( N X. N ) /\ -. (/) e. Y ) -> ( N X. N ) e. Fin )
80		sseq1 3518	. . . . . . . . . . . . . 14 |- ( a = (/) -> ( a C_ ( N X. N ) <-> (/) C_ ( N X. N ) ) )
81	80	3anbi2d 1299	. . . . . . . . . . . . 13 |- ( a = (/) -> ( ( ph /\ a C_ ( N X. N ) /\ -. (/) e. Y ) <-> ( ph /\ (/) C_ ( N X. N ) /\ -. (/) e. Y ) ) )
82		eleq1 2532	. . . . . . . . . . . . . 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 3518	. . . . . . . . . . . . . 14 |- ( a = b -> ( a C_ ( N X. N ) <-> b C_ ( N X. N ) ) )
86	85	3anbi2d 1299	. . . . . . . . . . . . 13 |- ( a = b -> ( ( ph /\ a C_ ( N X. N ) /\ -. (/) e. Y ) <-> ( ph /\ b C_ ( N X. N ) /\ -. (/) e. Y ) ) )
87		eleq1 2532	. . . . . . . . . . . . . 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 3518	. . . . . . . . . . . . . 14 |- ( a = ( b u. { c } ) -> ( a C_ ( N X. N ) <-> ( b u. { c } ) C_ ( N X. N ) ) )
91	90	3anbi2d 1299	. . . . . . . . . . . . 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 2532	. . . . . . . . . . . . . 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 3518	. . . . . . . . . . . . . 14 |- ( a = ( N X. N ) -> ( a C_ ( N X. N ) <-> ( N X. N ) C_ ( N X. N ) ) )
96	95	3anbi2d 1299	. . . . . . . . . . . . 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 2532	. . . . . . . . . . . . . 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 993	. . . . . . . . . . . 12 |- ( ( ph /\ (/) C_ ( N X. N ) /\ -. (/) e. Y ) -> -. (/) e. Y )
101		id 22	. . . . . . . . . . . . . . 15 |- ( ph -> ph )
102		ssun1 3660	. . . . . . . . . . . . . . . 16 |- b C_ ( b u. { c } )
103		sstr2 3504	. . . . . . . . . . . . . . . 16 |- ( b C_ ( b u. { c } ) -> ( ( b u. { c } ) C_ ( N X. N ) -> b C_ ( N X. N ) ) )
104	102, 103	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( ( b u. { c } ) C_ ( N X. N ) -> b C_ ( N X. N ) )
105		id 22	. . . . . . . . . . . . . . 15 |- ( -. (/) e. Y -> -. (/) e. Y )
106	101, 104, 105	3anim123i 1176	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ -. (/) e. Y ) -> ( ph /\ b C_ ( N X. N ) /\ -. (/) e. Y ) )
107	106	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 ) )
108		simpl1 994	. . . . . . . . . . . . . . . . . . . . . . . 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 )
109		simpl2 995	. . . . . . . . . . . . . . . . . . . . . . . 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 ) )
110		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 )
111	12, 13, 14	matbas2i 18684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( a e. B -> a e. ( K ^m ( N X. N ) ) )
112		elmapi 7430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( a e. ( K ^m ( N X. N ) ) -> a : ( N X. N ) --> K )
113	111, 112	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( a e. B -> a : ( N X. N ) --> K )
114	113	3ad2ant3 1014	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> a : ( N X. N ) --> K )
115	114	feqmptd 5911	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> a = ( e e. ( N X. N ) |-> ( a ` e ) ) )
116	115	reseq1d 5263	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
117	54	3ad2ant1 1012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> R e. Ring )
118		rnggrp 16984	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( R e. Ring -> R e. Grp )
119	117, 118	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> R e. Grp )
120	119	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> R e. Grp )
121	114	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 )
122		simp2 992	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( b u. { c } ) C_ ( N X. N ) )
123	122	unssbd 3675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> { c } C_ ( N X. N ) )
124		vex 3109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- c e. _V
125	124	snss 4144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( c e. ( N X. N ) <-> { c } C_ ( N X. N ) )
126	123, 125	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> c e. ( N X. N ) )
127		xp1st 6804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( c e. ( N X. N ) -> ( 1st ` c ) e. N )
128	126, 127	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( 1st ` c ) e. N )
129	128	snssd 4165	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> { ( 1st ` c ) } C_ N )
130		xpss1 5102	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( { ( 1st ` c ) } C_ N -> ( { ( 1st ` c ) } X. N ) C_ ( N X. N ) )
131	129, 130	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( { ( 1st ` c ) } X. N ) C_ ( N X. N ) )
132	131	sselda 3497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> e e. ( N X. N ) )
133	121, 132	ffvelrnd 6013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> ( a ` e ) e. K )
134	13, 51	rngidcl 16999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( R e. Ring -> .1. e. K )
135	117, 134	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> .1. e. K )
136	13, 50	rng0cl 17000	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( R e. Ring -> .0. e. K )
137	117, 136	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> .0. e. K )
138	135, 137	ifcld 3975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> if ( e e. d , .1. , .0. ) e. K )
139	138	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 )
140		eqid 2460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( -g ` R ) = ( -g ` R )
141	13, 52, 140	grpnpcan 15924	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
142	120, 133, 139, 141	syl3anc 1223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
143	142	eqcomd 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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. ) ) )
144	143	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. ) ) )
145		iftrue 3938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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. ) ) )
146		iftrue 3938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( e = c -> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) = if ( e e. d , .1. , .0. ) )
147	145, 146	oveq12d 6293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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. ) ) )
148	147	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. ) ) )
149	144, 148	eqtr4d 2504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
150	13, 52, 50	grplid 15874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( R e. Grp /\ ( a ` e ) e. K ) -> ( .0. .+ ( a ` e ) ) = ( a ` e ) )
151	120, 133, 150	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 ) )
152	151	eqcomd 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> ( a ` e ) = ( .0. .+ ( a ` e ) ) )
153	152	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 ) ) )
154		iffalse 3941	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( -. e = c -> if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) = .0. )
155		iffalse 3941	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( -. e = c -> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) = ( a ` e ) )
156	154, 155	oveq12d 6293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
157	156	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 ) ) )
158	153, 157	eqtr4d 2504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
159	149, 158	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 ) ) ) )
160	159	mpteq2dva 4526	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
161		snfi 7586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- { ( 1st ` c ) } e. Fin
162	6	3ad2ant1 1012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> N e. Fin )
163		xpfi 7780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( { ( 1st ` c ) } e. Fin /\ N e. Fin ) -> ( { ( 1st ` c ) } X. N ) e. Fin )
164	161, 162, 163	sylancr 663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( { ( 1st ` c ) } X. N ) e. Fin )
165		ovex 6300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) e. _V
166		fvex 5867	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( 0g ` R ) e. _V
167	50, 166	eqeltri 2544	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- .0. e. _V
168	165, 167	ifex 4001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) e. _V
169	168	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 )
170		fvex 5867	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( 1r ` R ) e. _V
171	51, 170	eqeltri 2544	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- .1. e. _V
172	171, 167	ifex 4001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- if ( e e. d , .1. , .0. ) e. _V
173		fvex 5867	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( a ` e ) e. _V
174	172, 173	ifex 4001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) e. _V
175	174	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 )
176		xp1st 6804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( e e. ( { ( 1st ` c ) } X. N ) -> ( 1st ` e ) e. { ( 1st ` c ) } )
177		elsni 4045	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( 1st ` e ) e. { ( 1st ` c ) } -> ( 1st ` e ) = ( 1st ` c ) )
178		iftrue 3938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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. ) )
179	176, 177, 178	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. ) )
180	179	mpteq2ia 4522	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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. ) )
181	180	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. ) ) )
182		eqidd 2461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
183	164, 169, 175, 181, 182	offval2 6531	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
184	160, 183	eqtr4d 2504	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
185		resmpt 5314	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( { ( 1st ` c ) } X. N ) C_ ( N X. N ) -> ( ( e e. ( N X. N ) |-> ( a ` e ) ) |` ( { ( 1st ` c ) } X. N ) ) = ( e e. ( { ( 1st ` c ) } X. N ) |-> ( a ` e ) ) )
186	131, 185	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
187		resmpt 5314	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( { ( 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 ) ) ) |` ( { ( 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 ) ) ) )
188	131, 187	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
189		resmpt 5314	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( { ( 1st ` c ) } X. N ) C_ ( N X. N ) -> ( ( 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 ) ) ) )
190	131, 189	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
191	188, 190	oveq12d 6293	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
192	184, 186, 191	3eqtr4d 2511	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
193	116, 192	eqtrd 2501	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
194	115	reseq1d 5263	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
195		xp1st 6804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( e e. ( ( N \ { ( 1st ` c ) } ) X. N ) -> ( 1st ` e ) e. ( N \ { ( 1st ` c ) } ) )
196		eldifsni 4146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( 1st ` e ) e. ( N \ { ( 1st ` c ) } ) -> ( 1st ` e ) =/= ( 1st ` c ) )
197	195, 196	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( e e. ( ( N \ { ( 1st ` c ) } ) X. N ) -> ( 1st ` e ) =/= ( 1st ` c ) )
198	197	neneqd 2662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( e e. ( ( N \ { ( 1st ` c ) } ) X. N ) -> -. ( 1st ` e ) = ( 1st ` c ) )
199	198	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 ) )
200		iffalse 3941	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( -. ( 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 ) ) = ( a ` e ) )
201	199, 200	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
202	201	mpteq2dva 4526	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
203		difss 3624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( N \ { ( 1st ` c ) } ) C_ N
204		xpss1 5102	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( N \ { ( 1st ` c ) } ) C_ N -> ( ( N \ { ( 1st ` c ) } ) X. N ) C_ ( N X. N ) )
205	203, 204	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( N \ { ( 1st ` c ) } ) X. N ) C_ ( N X. N )
206		resmpt 5314	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
207	205, 206	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 ) ) ) )
208		resmpt 5314	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
209	205, 208	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 ) ) )
210	202, 207, 209	3eqtr4rd 2512	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
211	194, 210	eqtrd 2501	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
212		fveq2 5857	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( e = c -> ( 1st ` e ) = ( 1st ` c ) )
213	199, 212	nsyl 121	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( ( N \ { ( 1st ` c ) } ) X. N ) ) -> -. e = c )
214	213, 155	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
215	214	mpteq2dva 4526	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
216		resmpt 5314	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
217	205, 216	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 ) ) ) )
218	215, 217, 209	3eqtr4rd 2512	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
219	194, 218	eqtrd 2501	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
220	138	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 )
221	114	ffvelrnda 6012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( N X. N ) ) -> ( a ` e ) e. K )
222	220, 221	ifcld 3975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
223		eqid 2460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
224	222, 223	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 )
225		fvex 5867	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( Base ` R ) e. _V
226	13, 225	eqeltri 2544	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- K e. _V
227	69	anidms 645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( N e. Fin -> ( N X. N ) e. Fin )
228	162, 227	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( N X. N ) e. Fin )
229		elmapg 7423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
230	226, 228, 229	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 ) )
231	224, 230	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 ) ) )
232	12, 13	matbas2 18683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( N e. Fin /\ R e. Ring ) -> ( K ^m ( N X. N ) ) = ( Base ` A ) )
233	162, 117, 232	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( K ^m ( N X. N ) ) = ( Base ` A ) )
234	233, 14	syl6eqr 2519	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( K ^m ( N X. N ) ) = B )
235	231, 234	eleqtrd 2550	. . . . . . . . . . . . . . . . . . . . . . . . . 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 )
236		simp3 993	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> a e. B )
237	119	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( N X. N ) ) -> R e. Grp )
238	13, 140	grpsubcl 15912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
239	237, 221, 220, 238	syl3anc 1223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
240	137	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( N X. N ) ) -> .0. e. K )
241	239, 240	ifcld 3975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
242	241, 221	ifcld 3975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
243		eqid 2460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
244	242, 243	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 )
245		elmapg 7423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
246	226, 228, 245	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 ) )
247	244, 246	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 ) ) )
248	247, 234	eleqtrd 2550	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
249	57	3ad2ant1 1012	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
250		reseq1 5258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( x = a -> ( x |` ( { w } X. N ) ) = ( a |` ( { w } X. N ) ) )
251	250	eqeq1d 2462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
252		reseq1 5258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( x = a -> ( x |` ( ( N \ { w } ) X. N ) ) = ( a |` ( ( N \ { w } ) X. N ) ) )
253	252	eqeq1d 2462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( x = a -> ( ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) <-> ( a |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) ) )
254	252	eqeq1d 2462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( x = a -> ( ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) <-> ( a |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) )
255	251, 253, 254	3anbi123d 1294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
256		fveq2 5857	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( x = a -> ( D ` x ) = ( D ` a ) )
257	256	eqeq1d 2462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( x = a -> ( ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) <-> ( D ` a ) = ( ( D ` y ) .+ ( D ` z ) ) ) )
258	255, 257	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 ) ) ) ) )
259	258	2ralbidv 2901	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
260		reseq1 5258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
261	260	oveq1d 6290	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
262	261	eqeq2d 2474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
263		reseq1 5258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
264	263	eqeq2d 2474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
265	262, 264	3anbi12d 1295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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