Theorem mdetunilem9 19569

Description: Lemma for mdetuni 19571. (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 3899	. . . 4 |- A. w e. (/) ( a ` w ) = if ( w e. ( _I |` N ) , .1. , .0. )
2		simpr 462	. . . . 5 |- ( ( ph /\ a e. B ) -> a e. B )
3		f1oi 5857	. . . . . . . 8 |- ( _I |` N ) : N -1-1-onto-> N
4		f1of 5822	. . . . . . . 8 |- ( ( _I |` N ) : N -1-1-onto-> N -> ( _I |` N ) : N --> N )
5	3, 4	mp1i 13	. . . . . . 7 |- ( ph -> ( _I |` N ) : N --> N )
6		mdetuni.n	. . . . . . . 8 |- ( ph -> N e. Fin )
7	6, 6	elmapd 7485	. . . . . . 7 |- ( ph -> ( ( _I |` N ) e. ( N ^m N ) <-> ( _I |` N ) : N --> N ) )
8	5, 7	mpbird 235	. . . . . 6 |- ( ph -> ( _I |` N ) e. ( N ^m N ) )
9	8	adantr 466	. . . . 5 |- ( ( ph /\ a e. B ) -> ( _I |` N ) e. ( N ^m N ) )
10		simplrl 768	. . . . . . . . . . . . 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 )
11		mdetuni.a	. . . . . . . . . . . . . . . . 17 |- A = ( N Mat R )
12		mdetuni.k	. . . . . . . . . . . . . . . . 17 |- K = ( Base ` R )
13		mdetuni.b	. . . . . . . . . . . . . . . . 17 |- B = ( Base ` A )
14	11, 12, 13	matbas2i 19371	. . . . . . . . . . . . . . . 16 |- ( y e. B -> y e. ( K ^m ( N X. N ) ) )
15		elmapi 7492	. . . . . . . . . . . . . . . 16 |- ( y e. ( K ^m ( N X. N ) ) -> y : ( N X. N ) --> K )
16	14, 15	syl 17	. . . . . . . . . . . . . . 15 |- ( y e. B -> y : ( N X. N ) --> K )
17	16	feqmptd 5925	. . . . . . . . . . . . . 14 |- ( y e. B -> y = ( w e. ( N X. N ) |-> ( y ` w ) ) )
18	17	fveq2d 5876	. . . . . . . . . . . . 13 |- ( y e. B -> ( D ` y ) = ( D ` ( w e. ( N X. N ) |-> ( y ` w ) ) ) )
19	10, 18	syl 17	. . . . . . . . . . . 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 ) ) ) )
20		eqid 2420	. . . . . . . . . . . . . 14 |- ( N X. N ) = ( N X. N )
21		mpteq12 4496	. . . . . . . . . . . . . . 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. ) ) )
22	21	fveq2d 5876	. . . . . . . . . . . . . 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. ) ) ) )
23	20, 22	mpan 674	. . . . . . . . . . . . 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. ) ) ) )
24	23	adantl 467	. . . . . . . . . . . 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. ) ) ) )
25		eleq1 2492	. . . . . . . . . . . . . . . . 17 |- ( a = z -> ( a e. ( N ^m N ) <-> z e. ( N ^m N ) ) )
26	25	anbi2d 708	. . . . . . . . . . . . . . . 16 |- ( a = z -> ( ( ph /\ a e. ( N ^m N ) ) <-> ( ph /\ z e. ( N ^m N ) ) ) )
27		elequ2 1872	. . . . . . . . . . . . . . . . . . . 20 |- ( a = z -> ( w e. a <-> w e. z ) )
28	27	ifbid 3928	. . . . . . . . . . . . . . . . . . 19 |- ( a = z -> if ( w e. a , .1. , .0. ) = if ( w e. z , .1. , .0. ) )
29	28	mpteq2dv 4504	. . . . . . . . . . . . . . . . . 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. ) ) )
30	29	fveq2d 5876	. . . . . . . . . . . . . . . . 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. ) ) ) )
31	30	eqeq1d 2422	. . . . . . . . . . . . . . . 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. ) )
32	26, 31	imbi12d 321	. . . . . . . . . . . . . . 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. ) ) )
33		eleq1 2492	. . . . . . . . . . . . . . . . . . . 20 |- ( w = <. b , c >. -> ( w e. a <-> <. b , c >. e. a ) )
34	33	ifbid 3928	. . . . . . . . . . . . . . . . . . 19 |- ( w = <. b , c >. -> if ( w e. a , .1. , .0. ) = if ( <. b , c >. e. a , .1. , .0. ) )
35	34	mpt2mpt 6393	. . . . . . . . . . . . . . . . . 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. ) )
36		elmapi 7492	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( a e. ( N ^m N ) -> a : N --> N )
37	36	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ a e. ( N ^m N ) ) -> a : N --> N )
38		ffn 5737	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( a : N --> N -> a Fn N )
39	37, 38	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ a e. ( N ^m N ) ) -> a Fn N )
40	39	3ad2ant1 1026	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ a e. ( N ^m N ) ) /\ b e. N /\ c e. N ) -> a Fn N )
41		simp2 1006	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ a e. ( N ^m N ) ) /\ b e. N /\ c e. N ) -> b e. N )
42		fnopfvb 5913	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( a Fn N /\ b e. N ) -> ( ( a ` b ) = c <-> <. b , c >. e. a ) )
43	40, 41, 42	syl2anc 665	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ a e. ( N ^m N ) ) /\ b e. N /\ c e. N ) -> ( ( a ` b ) = c <-> <. b , c >. e. a ) )
44	43	bicomd 204	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ a e. ( N ^m N ) ) /\ b e. N /\ c e. N ) -> ( <. b , c >. e. a <-> ( a ` b ) = c ) )
45	44	ifbid 3928	. . . . . . . . . . . . . . . . . . 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. ) )
46	45	mpt2eq3dva 6360	. . . . . . . . . . . . . . . . . 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. ) ) )
47	35, 46	syl5eq 2473	. . . . . . . . . . . . . . . . 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. ) ) )
48	47	fveq2d 5876	. . . . . . . . . . . . . . . 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. ) ) ) )
49		mdetuni.0g	. . . . . . . . . . . . . . . . . 18 |- .0. = ( 0g ` R )
50		mdetuni.1r	. . . . . . . . . . . . . . . . . 18 |- .1. = ( 1r ` R )
51		mdetuni.pg	. . . . . . . . . . . . . . . . . 18 |- .+ = ( +g ` R )
52		mdetuni.tg	. . . . . . . . . . . . . . . . . 18 |- .x. = ( .r ` R )
53		mdetuni.r	. . . . . . . . . . . . . . . . . 18 |- ( ph -> R e. Ring )
54		mdetuni.ff	. . . . . . . . . . . . . . . . . 18 |- ( ph -> D : B --> K )
55		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. ) )
56		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 ) ) ) )
57		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 ) ) ) )
58		mdetunilem9.id	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( D ` ( 1r ` A ) ) = .0. )
59	11, 13, 12, 49, 50, 51, 52, 6, 53, 54, 55, 56, 57, 58	mdetunilem8 19568	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ a : N --> N ) -> ( D ` ( b e. N , c e. N |-> if ( ( a ` b ) = c , .1. , .0. ) ) ) = .0. )
60	36, 59	sylan2 476	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ a e. ( N ^m N ) ) -> ( D ` ( b e. N , c e. N |-> if ( ( a ` b ) = c , .1. , .0. ) ) ) = .0. )
61	48, 60	eqtrd 2461	. . . . . . . . . . . . . . 15 |- ( ( ph /\ a e. ( N ^m N ) ) -> ( D ` ( w e. ( N X. N ) |-> if ( w e. a , .1. , .0. ) ) ) = .0. )
62	32, 61	chvarv 2067	. . . . . . . . . . . . . 14 |- ( ( ph /\ z e. ( N ^m N ) ) -> ( D ` ( w e. ( N X. N ) |-> if ( w e. z , .1. , .0. ) ) ) = .0. )
63	62	adantrl 720	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. B /\ z e. ( N ^m N ) ) ) -> ( D ` ( w e. ( N X. N ) |-> if ( w e. z , .1. , .0. ) ) ) = .0. )
64	63	adantr 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 ) |-> if ( w e. z , .1. , .0. ) ) ) = .0. )
65	19, 24, 64	3eqtrd 2465	. . . . . . . . . . 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. )
66	65	ex 435	. . . . . . . . . 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. ) )
67	66	ralrimivva 2844	. . . . . . . . 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. ) )
68		xpfi 7839	. . . . . . . . . . 11 |- ( ( N e. Fin /\ N e. Fin ) -> ( N X. N ) e. Fin )
69	6, 6, 68	syl2anc 665	. . . . . . . . . 10 |- ( ph -> ( N X. N ) e. Fin )
70		raleq 3023	. . . . . . . . . . . . 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. ) ) )
71	70	imbi1d 318	. . . . . . . . . . . 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. ) ) )
72	71	2ralbidv 2867	. . . . . . . . . . 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. ) ) )
73		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. ) }
74	72, 73	elab2g 3217	. . . . . . . . . 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. ) ) )
75	69, 74	syl 17	. . . . . . . . 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. ) ) )
76	67, 75	mpbird 235	. . . . . . . 8 |- ( ph -> ( N X. N ) e. Y )
77		ssid 3480	. . . . . . . . 9 |- ( N X. N ) C_ ( N X. N )
78	69	3ad2ant1 1026	. . . . . . . . . . 11 |- ( ( ph /\ ( N X. N ) C_ ( N X. N ) /\ -. (/) e. Y ) -> ( N X. N ) e. Fin )
79		sseq1 3482	. . . . . . . . . . . . . 14 |- ( a = (/) -> ( a C_ ( N X. N ) <-> (/) C_ ( N X. N ) ) )
80	79	3anbi2d 1340	. . . . . . . . . . . . 13 |- ( a = (/) -> ( ( ph /\ a C_ ( N X. N ) /\ -. (/) e. Y ) <-> ( ph /\ (/) C_ ( N X. N ) /\ -. (/) e. Y ) ) )
81		eleq1 2492	. . . . . . . . . . . . . 14 |- ( a = (/) -> ( a e. Y <-> (/) e. Y ) )
82	81	notbid 295	. . . . . . . . . . . . 13 |- ( a = (/) -> ( -. a e. Y <-> -. (/) e. Y ) )
83	80, 82	imbi12d 321	. . . . . . . . . . . 12 |- ( a = (/) -> ( ( ( ph /\ a C_ ( N X. N ) /\ -. (/) e. Y ) -> -. a e. Y ) <-> ( ( ph /\ (/) C_ ( N X. N ) /\ -. (/) e. Y ) -> -. (/) e. Y ) ) )
84		sseq1 3482	. . . . . . . . . . . . . 14 |- ( a = b -> ( a C_ ( N X. N ) <-> b C_ ( N X. N ) ) )
85	84	3anbi2d 1340	. . . . . . . . . . . . 13 |- ( a = b -> ( ( ph /\ a C_ ( N X. N ) /\ -. (/) e. Y ) <-> ( ph /\ b C_ ( N X. N ) /\ -. (/) e. Y ) ) )
86		eleq1 2492	. . . . . . . . . . . . . 14 |- ( a = b -> ( a e. Y <-> b e. Y ) )
87	86	notbid 295	. . . . . . . . . . . . 13 |- ( a = b -> ( -. a e. Y <-> -. b e. Y ) )
88	85, 87	imbi12d 321	. . . . . . . . . . . 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 ) ) )
89		sseq1 3482	. . . . . . . . . . . . . 14 |- ( a = ( b u. { c } ) -> ( a C_ ( N X. N ) <-> ( b u. { c } ) C_ ( N X. N ) ) )
90	89	3anbi2d 1340	. . . . . . . . . . . . 13 |- ( a = ( b u. { c } ) -> ( ( ph /\ a C_ ( N X. N ) /\ -. (/) e. Y ) <-> ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ -. (/) e. Y ) ) )
91		eleq1 2492	. . . . . . . . . . . . . 14 |- ( a = ( b u. { c } ) -> ( a e. Y <-> ( b u. { c } ) e. Y ) )
92	91	notbid 295	. . . . . . . . . . . . 13 |- ( a = ( b u. { c } ) -> ( -. a e. Y <-> -. ( b u. { c } ) e. Y ) )
93	90, 92	imbi12d 321	. . . . . . . . . . . 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 ) ) )
94		sseq1 3482	. . . . . . . . . . . . . 14 |- ( a = ( N X. N ) -> ( a C_ ( N X. N ) <-> ( N X. N ) C_ ( N X. N ) ) )
95	94	3anbi2d 1340	. . . . . . . . . . . . 13 |- ( a = ( N X. N ) -> ( ( ph /\ a C_ ( N X. N ) /\ -. (/) e. Y ) <-> ( ph /\ ( N X. N ) C_ ( N X. N ) /\ -. (/) e. Y ) ) )
96		eleq1 2492	. . . . . . . . . . . . . 14 |- ( a = ( N X. N ) -> ( a e. Y <-> ( N X. N ) e. Y ) )
97	96	notbid 295	. . . . . . . . . . . . 13 |- ( a = ( N X. N ) -> ( -. a e. Y <-> -. ( N X. N ) e. Y ) )
98	95, 97	imbi12d 321	. . . . . . . . . . . 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 ) ) )
99		simp3 1007	. . . . . . . . . . . 12 |- ( ( ph /\ (/) C_ ( N X. N ) /\ -. (/) e. Y ) -> -. (/) e. Y )
100		ssun1 3626	. . . . . . . . . . . . . . . 16 |- b C_ ( b u. { c } )
101		sstr2 3468	. . . . . . . . . . . . . . . 16 |- ( b C_ ( b u. { c } ) -> ( ( b u. { c } ) C_ ( N X. N ) -> b C_ ( N X. N ) ) )
102	100, 101	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( ( b u. { c } ) C_ ( N X. N ) -> b C_ ( N X. N ) )
103	102	3anim2i 1192	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ -. (/) e. Y ) -> ( ph /\ b C_ ( N X. N ) /\ -. (/) e. Y ) )
104	103	imim1i 60	. . . . . . . . . . . . 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 ) )
105		simpl1 1008	. . . . . . . . . . . . . . . . . . . . . . . 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 )
106		simpl2 1009	. . . . . . . . . . . . . . . . . . . . . . . 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 ) )
107		simprll 770	. . . . . . . . . . . . . . . . . . . . . . . 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 )
108	11, 12, 13	matbas2i 19371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( a e. B -> a e. ( K ^m ( N X. N ) ) )
109		elmapi 7492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( a e. ( K ^m ( N X. N ) ) -> a : ( N X. N ) --> K )
110	108, 109	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( a e. B -> a : ( N X. N ) --> K )
111	110	3ad2ant3 1028	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> a : ( N X. N ) --> K )
112	111	feqmptd 5925	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> a = ( e e. ( N X. N ) |-> ( a ` e ) ) )
113	112	reseq1d 5115	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
114	53	3ad2ant1 1026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> R e. Ring )
115		ringgrp 17713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( R e. Ring -> R e. Grp )
116	114, 115	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> R e. Grp )
117	116	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> R e. Grp )
118	111	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> a : ( N X. N ) --> K )
119		simp2 1006	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( b u. { c } ) C_ ( N X. N ) )
120	119	unssbd 3641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> { c } C_ ( N X. N ) )
121		vex 3081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- c e. _V
122	121	snss 4118	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( c e. ( N X. N ) <-> { c } C_ ( N X. N ) )
123	120, 122	sylibr 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> c e. ( N X. N ) )
124		xp1st 6828	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( c e. ( N X. N ) -> ( 1st ` c ) e. N )
125	123, 124	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( 1st ` c ) e. N )
126	125	snssd 4139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> { ( 1st ` c ) } C_ N )
127		xpss1 4954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( { ( 1st ` c ) } C_ N -> ( { ( 1st ` c ) } X. N ) C_ ( N X. N ) )
128	126, 127	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( { ( 1st ` c ) } X. N ) C_ ( N X. N ) )
129	128	sselda 3461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> e e. ( N X. N ) )
130	118, 129	ffvelrnd 6029	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> ( a ` e ) e. K )
131	12, 50	ringidcl 17729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( R e. Ring -> .1. e. K )
132	114, 131	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> .1. e. K )
133	12, 49	ring0cl 17730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( R e. Ring -> .0. e. K )
134	114, 133	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> .0. e. K )
135	132, 134	ifcld 3949	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> if ( e e. d , .1. , .0. ) e. K )
136	135	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
137		eqid 2420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( -g ` R ) = ( -g ` R )
138	12, 51, 137	grpnpcan 16690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
139	117, 130, 136, 138	syl3anc 1264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
140	139	eqcomd 2428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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. ) ) )
141	140	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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. ) ) )
142		iftrue 3912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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. ) ) )
143		iftrue 3912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( e = c -> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) = if ( e e. d , .1. , .0. ) )
144	142, 143	oveq12d 6314	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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. ) ) )
145	144	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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. ) ) )
146	141, 145	eqtr4d 2464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
147	12, 51, 49	grplid 16640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( R e. Grp /\ ( a ` e ) e. K ) -> ( .0. .+ ( a ` e ) ) = ( a ` e ) )
148	117, 130, 147	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> ( .0. .+ ( a ` e ) ) = ( a ` e ) )
149	148	eqcomd 2428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> ( a ` e ) = ( .0. .+ ( a ` e ) ) )
150	149	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
151		iffalse 3915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( -. e = c -> if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) = .0. )
152		iffalse 3915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( -. e = c -> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) = ( a ` e ) )
153	151, 152	oveq12d 6314	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
154	153	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
155	150, 154	eqtr4d 2464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
156	146, 155	pm2.61dan 798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
157	156	mpteq2dva 4503	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
158		snfi 7648	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- { ( 1st ` c ) } e. Fin
159	6	3ad2ant1 1026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> N e. Fin )
160		xpfi 7839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( { ( 1st ` c ) } e. Fin /\ N e. Fin ) -> ( { ( 1st ` c ) } X. N ) e. Fin )
161	158, 159, 160	sylancr 667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( { ( 1st ` c ) } X. N ) e. Fin )
162		ovex 6324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) e. _V
163		fvex 5882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( 0g ` R ) e. _V
164	49, 163	eqeltri 2504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- .0. e. _V
165	162, 164	ifex 3974	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) e. _V
166	165	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 )
167		fvex 5882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( 1r ` R ) e. _V
168	50, 167	eqeltri 2504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- .1. e. _V
169	168, 164	ifex 3974	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- if ( e e. d , .1. , .0. ) e. _V
170		fvex 5882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( a ` e ) e. _V
171	169, 170	ifex 3974	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) e. _V
172	171	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 )
173		xp1st 6828	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( e e. ( { ( 1st ` c ) } X. N ) -> ( 1st ` e ) e. { ( 1st ` c ) } )
174		elsni 4018	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( 1st ` e ) e. { ( 1st ` c ) } -> ( 1st ` e ) = ( 1st ` c ) )
175		iftrue 3912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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. ) )
176	173, 174, 175	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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. ) )
177	176	mpteq2ia 4499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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. ) )
178	177	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. ) ) )
179		eqidd 2421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
180	161, 166, 172, 178, 179	offval2 6553	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
181	157, 180	eqtr4d 2464	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
182	128	resmptd 5167	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
183	128	resmptd 5167	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
184	128	resmptd 5167	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
185	183, 184	oveq12d 6314	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
186	181, 182, 185	3eqtr4d 2471	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
187	113, 186	eqtrd 2461	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
188	112	reseq1d 5115	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
189		xp1st 6828	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( e e. ( ( N \ { ( 1st ` c ) } ) X. N ) -> ( 1st ` e ) e. ( N \ { ( 1st ` c ) } ) )
190		eldifsni 4120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( 1st ` e ) e. ( N \ { ( 1st ` c ) } ) -> ( 1st ` e ) =/= ( 1st ` c ) )
191	189, 190	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( e e. ( ( N \ { ( 1st ` c ) } ) X. N ) -> ( 1st ` e ) =/= ( 1st ` c ) )
192	191	neneqd 2623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( e e. ( ( N \ { ( 1st ` c ) } ) X. N ) -> -. ( 1st ` e ) = ( 1st ` c ) )
193	192	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( ( N \ { ( 1st ` c ) } ) X. N ) ) -> -. ( 1st ` e ) = ( 1st ` c ) )
194	193	iffalsed 3917	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
195	194	mpteq2dva 4503	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
196		difss 3589	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( N \ { ( 1st ` c ) } ) C_ N
197		xpss1 4954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( N \ { ( 1st ` c ) } ) C_ N -> ( ( N \ { ( 1st ` c ) } ) X. N ) C_ ( N X. N ) )
198	196, 197	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( N \ { ( 1st ` c ) } ) X. N ) C_ ( N X. N )
199		resmpt 5165	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
200	198, 199	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
201		resmpt 5165	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
202	198, 201	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
203	195, 200, 202	3eqtr4rd 2472	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
204	188, 203	eqtrd 2461	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
205		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( e = c -> ( 1st ` e ) = ( 1st ` c ) )
206	193, 205	nsyl 124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( ( N \ { ( 1st ` c ) } ) X. N ) ) -> -. e = c )
207	206	iffalsed 3917	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
208	207	mpteq2dva 4503	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
209		resmpt 5165	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
210	198, 209	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
211	208, 210, 202	3eqtr4rd 2472	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
212	188, 211	eqtrd 2461	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
213	135	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
214	111	ffvelrnda 6028	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( N X. N ) ) -> ( a ` e ) e. K )
215	213, 214	ifcld 3949	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
216		eqid 2420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
217	215, 216	fmptd 6052	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
218		fvex 5882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( Base ` R ) e. _V
219	12, 218	eqeltri 2504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- K e. _V
220	68	anidms 649	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( N e. Fin -> ( N X. N ) e. Fin )
221	159, 220	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( N X. N ) e. Fin )
222		elmapg 7484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
223	219, 221, 222	sylancr 667	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
224	217, 223	mpbird 235	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
225	11, 12	matbas2 19370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( N e. Fin /\ R e. Ring ) -> ( K ^m ( N X. N ) ) = ( Base ` A ) )
226	159, 114, 225	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( K ^m ( N X. N ) ) = ( Base ` A ) )
227	226, 13	syl6eqr 2479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( K ^m ( N X. N ) ) = B )
228	224, 227	eleqtrd 2510	. . . . . . . . . . . . . . . . . . . . . . . . . 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 )
229		simp3 1007	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> a e. B )
230	116	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( N X. N ) ) -> R e. Grp )
231	12, 137	grpsubcl 16678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
232	230, 214, 213, 231	syl3anc 1264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
233	134	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( N X. N ) ) -> .0. e. K )
234	232, 233	ifcld 3949	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
235	234, 214	ifcld 3949	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
236		eqid 2420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
237	235, 236	fmptd 6052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
238		elmapg 7484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
239	219, 221, 238	sylancr 667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
240	237, 239	mpbird 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
241	240, 227	eleqtrd 2510	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
242	56	3ad2ant1 1026	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
243		reseq1 5110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( x = a -> ( x |` ( { w } X. N ) ) = ( a |` ( { w } X. N ) ) )
244	243	eqeq1d 2422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
245		reseq1 5110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( x = a -> ( x |` ( ( N \ { w } ) X. N ) ) = ( a |` ( ( N \ { w } ) X. N ) ) )
246	245	eqeq1d 2422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( x = a -> ( ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) <-> ( a |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) ) )
247	245	eqeq1d 2422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( x = a -> ( ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) <-> ( a |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) )
248	244, 246, 247	3anbi123d 1335	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
249		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( x = a -> ( D ` x ) = ( D ` a ) )
250	249	eqeq1d 2422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( x = a -> ( ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) <-> ( D ` a ) = ( ( D ` y ) .+ ( D ` z ) ) ) )
251	248, 250	imbi12d 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
252	251	2ralbidv 2867	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
253		reseq1 5110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
254	253	oveq1d 6311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
255	254	eqeq2d 2434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
256		reseq1 5110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
257	256	eqeq2d 2434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
258	255, 257	3anbi12d 1336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
259		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
260	259	oveq1d 6311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
261	260	eqeq2d 2434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( y = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , ( (