Theorem mdetunilem9

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

	Ref	Expression
Hypotheses	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	mdetunilem9	|- ( ph -> D = ( B X. { .0. } ) )

Proof

Step	Hyp	Ref	Expression
1		mdetuni.a	|- A = ( N Mat R )
2		mdetuni.b	|- B = ( Base ` A )
3		mdetuni.k	|- K = ( Base ` R )
4		mdetuni.0g	|- .0. = ( 0g ` R )
5		mdetuni.1r	|- .1. = ( 1r ` R )
6		mdetuni.pg	|- .+ = ( +g ` R )
7		mdetuni.tg	|- .x. = ( .r ` R )
8		mdetuni.n	|- ( ph -> N e. Fin )
9		mdetuni.r	|- ( ph -> R e. Ring )
10		mdetuni.ff	|- ( ph -> D : B --> K )
11		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. ) )
12		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 ) ) ) )
13		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 ) ) ) )
14		mdetunilem9.id	|- ( ph -> ( D ` ( 1r ` A ) ) = .0. )
15		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. ) }
16		ral0	|- A. w e. (/) ( a ` w ) = if ( w e. ( _I |` N ) , .1. , .0. )
17		simpr	|- ( ( ph /\ a e. B ) -> a e. B )
18		f1oi	|- ( _I |` N ) : N -1-1-onto-> N
19		f1of	|- ( ( _I |` N ) : N -1-1-onto-> N -> ( _I |` N ) : N --> N )
20	18 19	mp1i	|- ( ph -> ( _I |` N ) : N --> N )
21	8 8	elmapd	|- ( ph -> ( ( _I |` N ) e. ( N ^m N ) <-> ( _I |` N ) : N --> N ) )
22	20 21	mpbird	|- ( ph -> ( _I |` N ) e. ( N ^m N ) )
23	22	adantr	|- ( ( ph /\ a e. B ) -> ( _I |` N ) e. ( N ^m N ) )
24		simplrl	|- ( ( ( 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 )
25	1 3 2	matbas2i	|- ( y e. B -> y e. ( K ^m ( N X. N ) ) )
26		elmapi	|- ( y e. ( K ^m ( N X. N ) ) -> y : ( N X. N ) --> K )
27	25 26	syl	|- ( y e. B -> y : ( N X. N ) --> K )
28	27	feqmptd	|- ( y e. B -> y = ( w e. ( N X. N ) |-> ( y ` w ) ) )
29	28	fveq2d	|- ( y e. B -> ( D ` y ) = ( D ` ( w e. ( N X. N ) |-> ( y ` w ) ) ) )
30	24 29	syl	|- ( ( ( 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 ) ) ) )
31		eqid	|- ( N X. N ) = ( N X. N )
32		mpteq12	|- ( ( ( 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. ) ) )
33	32	fveq2d	|- ( ( ( 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. ) ) ) )
34	31 33	mpan	|- ( 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. ) ) ) )
35	34	adantl	|- ( ( ( 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. ) ) ) )
36		eleq1	|- ( a = z -> ( a e. ( N ^m N ) <-> z e. ( N ^m N ) ) )
37	36	anbi2d	|- ( a = z -> ( ( ph /\ a e. ( N ^m N ) ) <-> ( ph /\ z e. ( N ^m N ) ) ) )
38		elequ2	|- ( a = z -> ( w e. a <-> w e. z ) )
39	38	ifbid	|- ( a = z -> if ( w e. a , .1. , .0. ) = if ( w e. z , .1. , .0. ) )
40	39	mpteq2dv	|- ( a = z -> ( w e. ( N X. N ) |-> if ( w e. a , .1. , .0. ) ) = ( w e. ( N X. N ) |-> if ( w e. z , .1. , .0. ) ) )
41	40	fveq2d	|- ( 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. ) ) ) )
42	41	eqeq1d	|- ( 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. ) )
43	37 42	imbi12d	|- ( 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. ) ) )
44		eleq1	|- ( w = <. b , c >. -> ( w e. a <-> <. b , c >. e. a ) )
45	44	ifbid	|- ( w = <. b , c >. -> if ( w e. a , .1. , .0. ) = if ( <. b , c >. e. a , .1. , .0. ) )
46	45	mpompt	|- ( w e. ( N X. N ) |-> if ( w e. a , .1. , .0. ) ) = ( b e. N , c e. N |-> if ( <. b , c >. e. a , .1. , .0. ) )
47		elmapi	|- ( a e. ( N ^m N ) -> a : N --> N )
48	47	adantl	|- ( ( ph /\ a e. ( N ^m N ) ) -> a : N --> N )
49	48	ffnd	|- ( ( ph /\ a e. ( N ^m N ) ) -> a Fn N )
50	49	3ad2ant1	|- ( ( ( ph /\ a e. ( N ^m N ) ) /\ b e. N /\ c e. N ) -> a Fn N )
51		simp2	|- ( ( ( ph /\ a e. ( N ^m N ) ) /\ b e. N /\ c e. N ) -> b e. N )
52		fnopfvb	|- ( ( a Fn N /\ b e. N ) -> ( ( a ` b ) = c <-> <. b , c >. e. a ) )
53	50 51 52	syl2anc	|- ( ( ( ph /\ a e. ( N ^m N ) ) /\ b e. N /\ c e. N ) -> ( ( a ` b ) = c <-> <. b , c >. e. a ) )
54	53	bicomd	|- ( ( ( ph /\ a e. ( N ^m N ) ) /\ b e. N /\ c e. N ) -> ( <. b , c >. e. a <-> ( a ` b ) = c ) )
55	54	ifbid	|- ( ( ( 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. ) )
56	55	mpoeq3dva	|- ( ( 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. ) ) )
57	46 56	syl5eq	|- ( ( 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. ) ) )
58	57	fveq2d	|- ( ( 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. ) ) ) )
59	1 2 3 4 5 6 7 8 9 10 11 12 13 14	mdetunilem8	|- ( ( ph /\ a : N --> N ) -> ( D ` ( b e. N , c e. N |-> if ( ( a ` b ) = c , .1. , .0. ) ) ) = .0. )
60	47 59	sylan2	|- ( ( ph /\ a e. ( N ^m N ) ) -> ( D ` ( b e. N , c e. N |-> if ( ( a ` b ) = c , .1. , .0. ) ) ) = .0. )
61	58 60	eqtrd	|- ( ( ph /\ a e. ( N ^m N ) ) -> ( D ` ( w e. ( N X. N ) |-> if ( w e. a , .1. , .0. ) ) ) = .0. )
62	43 61	chvarvv	|- ( ( ph /\ z e. ( N ^m N ) ) -> ( D ` ( w e. ( N X. N ) |-> if ( w e. z , .1. , .0. ) ) ) = .0. )
63	62	adantrl	|- ( ( 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	|- ( ( ( 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	30 35 64	3eqtrd	|- ( ( ( 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	|- ( ( 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	|- ( 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	|- ( ( N e. Fin /\ N e. Fin ) -> ( N X. N ) e. Fin )
69	8 8 68	syl2anc	|- ( ph -> ( N X. N ) e. Fin )
70		raleq	|- ( 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	|- ( 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	|- ( 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	72 15	elab2g	|- ( ( 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. ) ) )
74	69 73	syl	|- ( 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. ) ) )
75	67 74	mpbird	|- ( ph -> ( N X. N ) e. Y )
76		ssid	|- ( N X. N ) C_ ( N X. N )
77	69	3ad2ant1	|- ( ( ph /\ ( N X. N ) C_ ( N X. N ) /\ -. (/) e. Y ) -> ( N X. N ) e. Fin )
78		sseq1	|- ( a = (/) -> ( a C_ ( N X. N ) <-> (/) C_ ( N X. N ) ) )
79	78	3anbi2d	|- ( a = (/) -> ( ( ph /\ a C_ ( N X. N ) /\ -. (/) e. Y ) <-> ( ph /\ (/) C_ ( N X. N ) /\ -. (/) e. Y ) ) )
80		eleq1	|- ( a = (/) -> ( a e. Y <-> (/) e. Y ) )
81	80	notbid	|- ( a = (/) -> ( -. a e. Y <-> -. (/) e. Y ) )
82	79 81	imbi12d	|- ( a = (/) -> ( ( ( ph /\ a C_ ( N X. N ) /\ -. (/) e. Y ) -> -. a e. Y ) <-> ( ( ph /\ (/) C_ ( N X. N ) /\ -. (/) e. Y ) -> -. (/) e. Y ) ) )
83		sseq1	|- ( a = b -> ( a C_ ( N X. N ) <-> b C_ ( N X. N ) ) )
84	83	3anbi2d	|- ( a = b -> ( ( ph /\ a C_ ( N X. N ) /\ -. (/) e. Y ) <-> ( ph /\ b C_ ( N X. N ) /\ -. (/) e. Y ) ) )
85		eleq1	|- ( a = b -> ( a e. Y <-> b e. Y ) )
86	85	notbid	|- ( a = b -> ( -. a e. Y <-> -. b e. Y ) )
87	84 86	imbi12d	|- ( a = b -> ( ( ( ph /\ a C_ ( N X. N ) /\ -. (/) e. Y ) -> -. a e. Y ) <-> ( ( ph /\ b C_ ( N X. N ) /\ -. (/) e. Y ) -> -. b e. Y ) ) )
88		sseq1	|- ( a = ( b u. { c } ) -> ( a C_ ( N X. N ) <-> ( b u. { c } ) C_ ( N X. N ) ) )
89	88	3anbi2d	|- ( a = ( b u. { c } ) -> ( ( ph /\ a C_ ( N X. N ) /\ -. (/) e. Y ) <-> ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ -. (/) e. Y ) ) )
90		eleq1	|- ( a = ( b u. { c } ) -> ( a e. Y <-> ( b u. { c } ) e. Y ) )
91	90	notbid	|- ( a = ( b u. { c } ) -> ( -. a e. Y <-> -. ( b u. { c } ) e. Y ) )
92	89 91	imbi12d	|- ( 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 ) ) )
93		sseq1	|- ( a = ( N X. N ) -> ( a C_ ( N X. N ) <-> ( N X. N ) C_ ( N X. N ) ) )
94	93	3anbi2d	|- ( a = ( N X. N ) -> ( ( ph /\ a C_ ( N X. N ) /\ -. (/) e. Y ) <-> ( ph /\ ( N X. N ) C_ ( N X. N ) /\ -. (/) e. Y ) ) )
95		eleq1	|- ( a = ( N X. N ) -> ( a e. Y <-> ( N X. N ) e. Y ) )
96	95	notbid	|- ( a = ( N X. N ) -> ( -. a e. Y <-> -. ( N X. N ) e. Y ) )
97	94 96	imbi12d	|- ( 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 ) ) )
98		simp3	|- ( ( ph /\ (/) C_ ( N X. N ) /\ -. (/) e. Y ) -> -. (/) e. Y )
99		ssun1	|- b C_ ( b u. { c } )
100		sstr2	|- ( b C_ ( b u. { c } ) -> ( ( b u. { c } ) C_ ( N X. N ) -> b C_ ( N X. N ) ) )
101	99 100	ax-mp	|- ( ( b u. { c } ) C_ ( N X. N ) -> b C_ ( N X. N ) )
102	101	3anim2i	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ -. (/) e. Y ) -> ( ph /\ b C_ ( N X. N ) /\ -. (/) e. Y ) )
103	102	imim1i	|- ( ( ( ph /\ b C_ ( N X. N ) /\ -. (/) e. Y ) -> -. b e. Y ) -> ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ -. (/) e. Y ) -> -. b e. Y ) )
104		simpl1	|- ( ( ( 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 )
105		simpl2	|- ( ( ( 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 ) )
106		simprll	|- ( ( ( 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 )
107	1 3 2	matbas2i	|- ( a e. B -> a e. ( K ^m ( N X. N ) ) )
108		elmapi	|- ( a e. ( K ^m ( N X. N ) ) -> a : ( N X. N ) --> K )
109	107 108	syl	|- ( a e. B -> a : ( N X. N ) --> K )
110	109	3ad2ant3	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> a : ( N X. N ) --> K )
111	110	feqmptd	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> a = ( e e. ( N X. N ) |-> ( a ` e ) ) )
112	111	reseq1d	|- ( ( 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 ) ) )
113	9	3ad2ant1	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> R e. Ring )
114		ringgrp	|- ( R e. Ring -> R e. Grp )
115	113 114	syl	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> R e. Grp )
116	115	adantr	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> R e. Grp )
117	110	adantr	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> a : ( N X. N ) --> K )
118		simp2	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( b u. { c } ) C_ ( N X. N ) )
119	118	unssbd	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> { c } C_ ( N X. N ) )
120		vex	|- c e. _V
121	120	snss	|- ( c e. ( N X. N ) <-> { c } C_ ( N X. N ) )
122	119 121	sylibr	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> c e. ( N X. N ) )
123		xp1st	|- ( c e. ( N X. N ) -> ( 1st ` c ) e. N )
124	122 123	syl	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( 1st ` c ) e. N )
125	124	snssd	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> { ( 1st ` c ) } C_ N )
126		xpss1	|- ( { ( 1st ` c ) } C_ N -> ( { ( 1st ` c ) } X. N ) C_ ( N X. N ) )
127	125 126	syl	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( { ( 1st ` c ) } X. N ) C_ ( N X. N ) )
128	127	sselda	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> e e. ( N X. N ) )
129	117 128	ffvelrnd	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> ( a ` e ) e. K )
130	3 5	ringidcl	|- ( R e. Ring -> .1. e. K )
131	113 130	syl	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> .1. e. K )
132	3 4	ring0cl	|- ( R e. Ring -> .0. e. K )
133	113 132	syl	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> .0. e. K )
134	131 133	ifcld	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> if ( e e. d , .1. , .0. ) e. K )
135	134	adantr	|- ( ( ( 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 )
136		eqid	|- ( -g ` R ) = ( -g ` R )
137	3 6 136	grpnpcan	|- ( ( 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 ) )
138	116 129 135 137	syl3anc	|- ( ( ( 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 ) )
139	138	eqcomd	|- ( ( ( 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. ) ) )
140	139	adantr	|- ( ( ( ( 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. ) ) )
141		iftrue	|- ( 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. ) ) )
142		iftrue	|- ( e = c -> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) = if ( e e. d , .1. , .0. ) )
143	141 142	oveq12d	|- ( 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. ) ) )
144	143	adantl	|- ( ( ( ( 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. ) ) )
145	140 144	eqtr4d	|- ( ( ( ( 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 ) ) ) )
146	3 6 4	grplid	|- ( ( R e. Grp /\ ( a ` e ) e. K ) -> ( .0. .+ ( a ` e ) ) = ( a ` e ) )
147	116 129 146	syl2anc	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> ( .0. .+ ( a ` e ) ) = ( a ` e ) )
148	147	eqcomd	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> ( a ` e ) = ( .0. .+ ( a ` e ) ) )
149	148	adantr	|- ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) /\ -. e = c ) -> ( a ` e ) = ( .0. .+ ( a ` e ) ) )
150		iffalse	|- ( -. e = c -> if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) = .0. )
151		iffalse	|- ( -. e = c -> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) = ( a ` e ) )
152	150 151	oveq12d	|- ( -. 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 ) ) )
153	152	adantl	|- ( ( ( ( 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 ) ) )
154	149 153	eqtr4d	|- ( ( ( ( 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 ) ) ) )
155	145 154	pm2.61dan	|- ( ( ( 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 ) ) ) )
156	155	mpteq2dva	|- ( ( 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 ) ) ) ) )
157		snfi	|- { ( 1st ` c ) } e. Fin
158	8	3ad2ant1	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> N e. Fin )
159		xpfi	|- ( ( { ( 1st ` c ) } e. Fin /\ N e. Fin ) -> ( { ( 1st ` c ) } X. N ) e. Fin )
160	157 158 159	sylancr	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( { ( 1st ` c ) } X. N ) e. Fin )
161		ovex	|- ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) e. _V
162	4	fvexi	|- .0. e. _V
163	161 162	ifex	|- if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) e. _V
164	163	a1i	|- ( ( ( 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 )
165	5	fvexi	|- .1. e. _V
166	165 162	ifex	|- if ( e e. d , .1. , .0. ) e. _V
167		fvex	|- ( a ` e ) e. _V
168	166 167	ifex	|- if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) e. _V
169	168	a1i	|- ( ( ( 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 )
170		xp1st	|- ( e e. ( { ( 1st ` c ) } X. N ) -> ( 1st ` e ) e. { ( 1st ` c ) } )
171		elsni	|- ( ( 1st ` e ) e. { ( 1st ` c ) } -> ( 1st ` e ) = ( 1st ` c ) )
172		iftrue	|- ( ( 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. ) )
173	170 171 172	3syl	|- ( 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. ) )
174	173	mpteq2ia	|- ( 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. ) )
175	174	a1i	|- ( ( 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. ) ) )
176		eqidd	|- ( ( 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 ) ) ) )
177	160 164 169 175 176	offval2	|- ( ( 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 ) ) ) ) )
178	156 177	eqtr4d	|- ( ( 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 ) ) ) ) )
179	127	resmptd	|- ( ( 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 ) ) )
180	127	resmptd	|- ( ( 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 ) ) ) )
181	127	resmptd	|- ( ( 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 ) ) ) )
182	180 181	oveq12d	|- ( ( 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 ) ) ) ) )
183	178 179 182	3eqtr4d	|- ( ( 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 ) ) ) )
184	112 183	eqtrd	|- ( ( 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 ) ) ) )
185	111	reseq1d	|- ( ( 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 ) ) )
186		xp1st	|- ( e e. ( ( N \ { ( 1st ` c ) } ) X. N ) -> ( 1st ` e ) e. ( N \ { ( 1st ` c ) } ) )
187		eldifsni	|- ( ( 1st ` e ) e. ( N \ { ( 1st ` c ) } ) -> ( 1st ` e ) =/= ( 1st ` c ) )
188	186 187	syl	|- ( e e. ( ( N \ { ( 1st ` c ) } ) X. N ) -> ( 1st ` e ) =/= ( 1st ` c ) )
189	188	neneqd	|- ( e e. ( ( N \ { ( 1st ` c ) } ) X. N ) -> -. ( 1st ` e ) = ( 1st ` c ) )
190	189	adantl	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( ( N \ { ( 1st ` c ) } ) X. N ) ) -> -. ( 1st ` e ) = ( 1st ` c ) )
191	190	iffalsed	|- ( ( ( 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 ) )
192	191	mpteq2dva	|- ( ( 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 ) ) )
193		difss	|- ( N \ { ( 1st ` c ) } ) C_ N
194		xpss1	|- ( ( N \ { ( 1st ` c ) } ) C_ N -> ( ( N \ { ( 1st ` c ) } ) X. N ) C_ ( N X. N ) )
195	193 194	ax-mp	|- ( ( N \ { ( 1st ` c ) } ) X. N ) C_ ( N X. N )
196		resmpt	|- ( ( ( 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 ) ) ) )
197	195 196	mp1i	|- ( ( 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 ) ) ) )
198		resmpt	|- ( ( ( 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 ) ) )
199	195 198	mp1i	|- ( ( 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 ) ) )
200	192 197 199	3eqtr4rd	|- ( ( 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 ) ) )
201	185 200	eqtrd	|- ( ( 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 ) ) )
202		fveq2	|- ( e = c -> ( 1st ` e ) = ( 1st ` c ) )
203	190 202	nsyl	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( ( N \ { ( 1st ` c ) } ) X. N ) ) -> -. e = c )
204	203	iffalsed	|- ( ( ( 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 ) )
205	204	mpteq2dva	|- ( ( 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 ) ) )
206		resmpt	|- ( ( ( 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 ) ) ) )
207	195 206	mp1i	|- ( ( 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 ) ) ) )
208	205 207 199	3eqtr4rd	|- ( ( 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 ) ) )
209	185 208	eqtrd	|- ( ( 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 ) ) )
210	134	adantr	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( N X. N ) ) -> if ( e e. d , .1. , .0. ) e. K )
211	110	ffvelrnda	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( N X. N ) ) -> ( a ` e ) e. K )
212	210 211	ifcld	|- ( ( ( 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 )
213	212	fmpttd	|- ( ( 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 )
214	3	fvexi	|- K e. _V
215	68	anidms	|- ( N e. Fin -> ( N X. N ) e. Fin )
216	158 215	syl	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( N X. N ) e. Fin )
217		elmapg	|- ( ( 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 ) )
218	214 216 217	sylancr	|- ( ( 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 ) )
219	213 218	mpbird	|- ( ( 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 ) ) )
220	1 3	matbas2	|- ( ( N e. Fin /\ R e. Ring ) -> ( K ^m ( N X. N ) ) = ( Base ` A ) )
221	158 113 220	syl2anc	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( K ^m ( N X. N ) ) = ( Base ` A ) )
222	221 2	eqtr4di	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( K ^m ( N X. N ) ) = B )
223	219 222	eleqtrd	|- ( ( 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 )
224		simp3	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> a e. B )
225	115	adantr	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( N X. N ) ) -> R e. Grp )
226	3 136	grpsubcl	|- ( ( 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 )
227	225 211 210 226	syl3anc	|- ( ( ( 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 )
228	133	adantr	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( N X. N ) ) -> .0. e. K )
229	227 228	ifcld	|- ( ( ( 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 )
230	229 211	ifcld	|- ( ( ( 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 )
231	230	fmpttd	|- ( ( 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 )
232		elmapg	|- ( ( 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 ) )
233	214 216 232	sylancr	|- ( ( 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 ) )
234	231 233	mpbird	|- ( ( 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 ) ) )
235	234 222	eleqtrd	|- ( ( 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 )
236	12	3ad2ant1	|- ( ( 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 ) ) ) )
237		reseq1	|- ( x = a -> ( x |` ( { w } X. N ) ) = ( a |` ( { w } X. N ) ) )
238	237	eqeq1d	|- ( 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 ) ) ) ) )
239		reseq1	|- ( x = a -> ( x |` ( ( N \ { w } ) X. N ) ) = ( a |` ( ( N \ { w } ) X. N ) ) )
240	239	eqeq1d	|- ( x = a -> ( ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) <-> ( a |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) ) )
241	239	eqeq1d	|- ( x = a -> ( ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) <-> ( a |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) )
242	238 240 241	3anbi123d	|- ( 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 ) ) ) ) )
243		fveqeq2	|- ( x = a -> ( ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) <-> ( D ` a ) = ( ( D ` y ) .+ ( D ` z ) ) ) )
244	242 243	imbi12d	|- ( 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 ) ) ) ) )
245	244	2ralbidv	|- ( 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 ) ) ) ) )
246		reseq1	|- ( 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 ) ) )
247	246	oveq1d	|- ( 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 ) ) ) )
248	247	eqeq2d	|- ( 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 ) ) ) ) )
249		reseq1	|- ( 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 ) ) )
250	249	eqeq2d	|- ( 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 ) ) ) )
251	248 250	3anbi12d	|- ( 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 ) ) ) ) )
252		fveq2	|- ( 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 ) ) ) ) )
253	252	oveq1d	|- ( 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 ) ) )
254	253	eqeq2d	|- ( 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 ` a ) = ( ( D ` y ) .+ ( D ` z ) ) <-> ( D ` a ) = ( ( 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 ) ) ) )
255	251 254	imbi12d	|- ( 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 ) ) ) -> ( D ` a ) = ( ( D ` y ) .+ ( D ` z ) ) ) <-> ( ( ( 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 ) ) ) -> ( D ` a ) = ( ( 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 ) ) ) ) )
256	255	2ralbidv	|- ( 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. 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 ) ) ) <-> A. z e. B A. w e. 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 ) ) ) -> ( D ` a ) = ( ( 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 ) ) ) ) )
257	245 256	rspc2va	|- ( ( ( 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 ) /\ 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 ) ) ) ) -> A. z e. B A. w e. 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 ) ) ) -> ( D ` a ) = ( ( 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 ) ) ) )
258	224 235 236 257	syl21anc	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> A. z e. B A. w e. 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 ) ) ) -> ( D ` a ) = ( ( 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 ) ) ) )
259		reseq1	|- ( z = ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) -> ( z |` ( { w } X. N ) ) = ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( { w } X. N ) ) )
260	259	oveq2d	|- ( z = ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .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 ) ) ) |` ( { 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 .+ ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( { w } X. N ) ) ) )
261	260	eqeq2d	|- ( z = ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) -> ( ( 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 |` ( { 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 .+ ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( { w } X. N ) ) ) ) )
262		reseq1	|- ( z = ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) -> ( z |` ( ( N \ { w } ) X. N ) ) = ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { w } ) X. N ) ) )
263	262	eqeq2d	|- ( z = ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) -> ( ( a |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) <-> ( a |` ( ( N \ { w } ) X. N ) ) = ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { w } ) X. N ) ) ) )
264	261 263	3anbi13d	|- ( z = ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) -> ( ( ( 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 ) ) ) <-> ( ( 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 .+ ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( { 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 ) ) = ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { w } ) X. N ) ) ) ) )
265		fveq2	|- ( z = ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) -> ( D ` z ) = ( D ` ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) )
266	265	oveq2d	|- ( z = ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) -> ( ( 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 ) ) = ( ( 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 ` ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) ) )
267	266	eqeq2d	|- ( z = ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) -> ( ( D ` a ) = ( ( 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 ) ) <-> ( D ` a ) = ( ( 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 ` ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) ) ) )
268	264 267	imbi12d	|- ( z = ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) -> ( ( ( ( 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 ) ) ) -> ( D ` a ) = ( ( 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 ) ) ) <-> ( ( ( 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 .+ ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( { 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 ) ) = ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` a ) = ( ( 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 ` ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) ) ) ) )
269		sneq	|- ( w = ( 1st ` c ) -> { w } = { ( 1st ` c ) } )
270	269	xpeq1d	|- ( w = ( 1st ` c ) -> ( { w } X. N ) = ( { ( 1st ` c ) } X. N ) )
271	270	reseq2d	|- ( w = ( 1st ` c ) -> ( a |` ( { w } X. N ) ) = ( a |` ( { ( 1st ` c ) } X. N ) ) )
272	270	reseq2d	|- ( w = ( 1st ` c ) -> ( ( 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 ) ) = ( ( 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 ) ) )
273	270	reseq2d	|- ( w = ( 1st ` c ) -> ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( { w } X. N ) ) = ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( { ( 1st ` c ) } X. N ) ) )
274	272 273	oveq12d	|- ( w = ( 1st ` c ) -> ( ( ( 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 .+ ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( { 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 ) ) ) |` ( { ( 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 ) ) ) )
275	271 274	eqeq12d	|- ( w = ( 1st ` c ) -> ( ( 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 .+ ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( { w } X. N ) ) ) <-> ( 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 ) ) ) ) )
276	269	difeq2d	|- ( w = ( 1st ` c ) -> ( N \ { w } ) = ( N \ { ( 1st ` c ) } ) )
277	276	xpeq1d	|- ( w = ( 1st ` c ) -> ( ( N \ { w } ) X. N ) = ( ( N \ { ( 1st ` c ) } ) X. N ) )
278	277	reseq2d	|- ( w = ( 1st ` c ) -> ( a |` ( ( N \ { w } ) X. N ) ) = ( a |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) )
279	277	reseq2d	|- ( w = ( 1st ` c ) -> ( ( 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 ) ) = ( ( 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 ) ) )
280	278 279	eqeq12d	|- ( w = ( 1st ` c ) -> ( ( 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 \ { ( 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 ) ) ) )
281	277	reseq2d	|- ( w = ( 1st ` c ) -> ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { w } ) X. N ) ) = ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) )
282	278 281	eqeq12d	|- ( w = ( 1st ` c ) -> ( ( a |` ( ( N \ { w } ) X. N ) ) = ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { w } ) X. N ) ) <-> ( 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 ) ) ) )
283	275 280 282	3anbi123d	|- ( w = ( 1st ` c ) -> ( ( ( 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 .+ ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( { 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 ) ) = ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { w } ) X. N ) ) ) <-> ( ( 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 ) ) ) /\ ( 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 ) ) /\ ( 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 ) ) ) ) )
284	283	imbi1d	|- ( w = ( 1st ` c ) -> ( ( ( ( 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 .+ ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( { 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 ) ) = ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` a ) = ( ( 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 ` ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) ) ) <-> ( ( ( 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 ) ) ) /\ ( 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 ) ) /\ ( 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 ) ) ) -> ( D ` a ) = ( ( 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 ` ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) ) ) ) )
285	268 284	rspc2va	|- ( ( ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) e. B /\ ( 1st ` c ) e. N ) /\ A. z e. B A. w e. 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 ) ) ) -> ( D ` a ) = ( ( 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 ) ) ) ) -> ( ( ( 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 ) ) ) /\ ( 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 ) ) /\ ( 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 ) ) ) -> ( D ` a ) = ( ( 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 ` ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) ) ) )
286	223 124 258 285	syl21anc	|- ( ( 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 ) ) ) /\ ( 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 ) ) /\ ( 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 ) ) ) -> ( D ` a ) = ( ( 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 ` ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) ) ) )
287	184 201 209 286	mp3and	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( D ` a ) = ( ( 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 ` ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) ) )
288	104 105 106 287	syl3anc	|- ( ( ( 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. ) ) ) -> ( D ` a ) = ( ( 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 ` ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) ) )
289		fveq2	|- ( e = c -> ( a ` e ) = ( a ` c ) )
290		elequ1	|- ( e = c -> ( e e. d <-> c e. d ) )
291	290	ifbid	|- ( e = c -> if ( e e. d , .1. , .0. ) = if ( c e. d , .1. , .0. ) )
292	289 291	oveq12d	|- ( e = c -> ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) = ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) )
293	292	adantl	|- ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) /\ e = c ) -> ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) = ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) )
294	110 122	ffvelrnd	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( a ` c ) e. K )
295	131 133	ifcld	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> if ( c e. d , .1. , .0. ) e. K )
296	3 136	grpsubcl	|- ( ( R e. Grp /\ ( a ` c ) e. K /\ if ( c e. d , .1. , .0. ) e. K ) -> ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) e. K )
297	115 294 295 296	syl3anc	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) e. K )
298	3 7 5	ringridm	|- ( ( R e. Ring /\ ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) e. K ) -> ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. .1. ) = ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) )
299	113 297 298	syl2anc	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. .1. ) = ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) )
300	299	ad2antrr	|- ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) /\ e = c ) -> ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. .1. ) = ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) )
301	293 300	eqtr4d	|- ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) /\ e = c ) -> ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. .1. ) )
302	141	adantl	|- ( ( ( ( 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. ) = ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) )
303		iftrue	|- ( e = c -> if ( e = c , .1. , .0. ) = .1. )
304	303	oveq2d	|- ( e = c -> ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. if ( e = c , .1. , .0. ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. .1. ) )
305	304	adantl	|- ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) /\ e = c ) -> ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. if ( e = c , .1. , .0. ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. .1. ) )
306	301 302 305	3eqtr4d	|- ( ( ( ( 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. ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. if ( e = c , .1. , .0. ) ) )
307	3 7 4	ringrz	|- ( ( R e. Ring /\ ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) e. K ) -> ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. .0. ) = .0. )
308	113 297 307	syl2anc	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. .0. ) = .0. )
309	308	eqcomd	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> .0. = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. .0. ) )
310	309	ad2antrr	|- ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) /\ -. e = c ) -> .0. = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. .0. ) )
311	150	adantl	|- ( ( ( ( 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. ) = .0. )
312		iffalse	|- ( -. e = c -> if ( e = c , .1. , .0. ) = .0. )
313	312	oveq2d	|- ( -. e = c -> ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. if ( e = c , .1. , .0. ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. .0. ) )
314	313	adantl	|- ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) /\ -. e = c ) -> ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. if ( e = c , .1. , .0. ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. .0. ) )
315	310 311 314	3eqtr4d	|- ( ( ( ( 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. ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. if ( e = c , .1. , .0. ) ) )
316	306 315	pm2.61dan	|- ( ( ( 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. ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. if ( e = c , .1. , .0. ) ) )
317	170	adantl	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> ( 1st ` e ) e. { ( 1st ` c ) } )
318	317 171	syl	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> ( 1st ` e ) = ( 1st ` c ) )
319	318	iftrued	|- ( ( ( 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 ) ) = if ( e = c , ( ( a ` e ) ( -g ` R ) if ( e e. d , .1. , .0. ) ) , .0. ) )
320	318	iftrued	|- ( ( ( 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 , .1. , .0. ) , ( a ` e ) ) = if ( e = c , .1. , .0. ) )
321	320	oveq2d	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. if ( e = c , .1. , .0. ) ) )
322	316 319 321	3eqtr4d	|- ( ( ( 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 ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) )
323	322	mpteq2dva	|- ( ( 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 ) |-> ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ) )
324		ovexd	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( { ( 1st ` c ) } X. N ) ) -> ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) e. _V )
325	165 162	ifex	|- if ( e = c , .1. , .0. ) e. _V
326	325 167	ifex	|- if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) e. _V
327	326	a1i	|- ( ( ( 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 , .1. , .0. ) , ( a ` e ) ) e. _V )
328		fconstmpt	|- ( ( { ( 1st ` c ) } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) = ( e e. ( { ( 1st ` c ) } X. N ) |-> ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) )
329	328	a1i	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( { ( 1st ` c ) } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) = ( e e. ( { ( 1st ` c ) } X. N ) |-> ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) ) )
330	127	resmptd	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( { ( 1st ` c ) } X. N ) ) = ( e e. ( { ( 1st ` c ) } X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) )
331	160 324 327 329 330	offval2	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( ( { ( 1st ` c ) } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( { ( 1st ` c ) } X. N ) ) ) = ( e e. ( { ( 1st ` c ) } X. N ) |-> ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ) )
332	323 180 331	3eqtr4d	|- ( ( 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 ) ) = ( ( ( { ( 1st ` c ) } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( { ( 1st ` c ) } X. N ) ) ) )
333		iffalse	|- ( -. ( 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 ) )
334		iffalse	|- ( -. ( 1st ` e ) = ( 1st ` c ) -> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) = ( a ` e ) )
335	333 334	eqtr4d	|- ( -. ( 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 ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) )
336	190 335	syl	|- ( ( ( 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 ) ) = if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) )
337	336	mpteq2dva	|- ( ( 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 ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) )
338		resmpt	|- ( ( ( N \ { ( 1st ` c ) } ) X. N ) C_ ( N X. N ) -> ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) = ( e e. ( ( N \ { ( 1st ` c ) } ) X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) )
339	195 338	mp1i	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) = ( e e. ( ( N \ { ( 1st ` c ) } ) X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) )
340	337 197 339	3eqtr4d	|- ( ( 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 X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) )
341	131 133	ifcld	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> if ( e = c , .1. , .0. ) e. K )
342	341	adantr	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( N X. N ) ) -> if ( e = c , .1. , .0. ) e. K )
343	342 211	ifcld	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ e e. ( N X. N ) ) -> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) e. K )
344	343	fmpttd	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) : ( N X. N ) --> K )
345		elmapg	|- ( ( K e. _V /\ ( N X. N ) e. Fin ) -> ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) e. ( K ^m ( N X. N ) ) <-> ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) : ( N X. N ) --> K ) )
346	214 216 345	sylancr	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) e. ( K ^m ( N X. N ) ) <-> ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) : ( N X. N ) --> K ) )
347	344 346	mpbird	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) e. ( K ^m ( N X. N ) ) )
348	347 222	eleqtrd	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) e. B )
349	13	3ad2ant1	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> 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 ) ) ) )
350		reseq1	|- ( x = ( 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 ) ) ) -> ( x |` ( { 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 ) ) )
351	350	eqeq1d	|- ( x = ( 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 ) ) ) -> ( ( x |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( 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 ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) ) )
352		reseq1	|- ( x = ( 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 ) ) ) -> ( x |` ( ( 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 ) ) )
353	352	eqeq1d	|- ( x = ( 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 ) ) ) -> ( ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( 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 ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) )
354	351 353	anbi12d	|- ( x = ( 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 ) ) ) -> ( ( ( 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 ) ) ) <-> ( ( ( 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 ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( 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 ) ) ) |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) ) )
355		fveqeq2	|- ( x = ( 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 ` x ) = ( y .x. ( 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 ) ) ) ) = ( y .x. ( D ` z ) ) ) )
356	354 355	imbi12d	|- ( x = ( 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 ) ) ) -> ( ( ( ( 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 ) ) ) <-> ( ( ( ( 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 ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( 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 ) ) ) |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( 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 ) ) ) ) = ( y .x. ( D ` z ) ) ) ) )
357	356	2ralbidv	|- ( x = ( 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. 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 ) ) ) <-> A. z e. B A. w e. 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 ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( 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 ) ) ) |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( 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 ) ) ) ) = ( y .x. ( D ` z ) ) ) ) )
358		sneq	|- ( y = ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) -> { y } = { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } )
359	358	xpeq2d	|- ( y = ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) -> ( ( { w } X. N ) X. { y } ) = ( ( { w } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) )
360	359	oveq1d	|- ( y = ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) -> ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) = ( ( ( { w } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( z |` ( { w } X. N ) ) ) )
361	360	eqeq2d	|- ( y = ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) -> ( ( ( 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 ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( 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 ) ) = ( ( ( { w } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( z |` ( { w } X. N ) ) ) ) )
362	361	anbi1d	|- ( y = ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) -> ( ( ( ( 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 ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( 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 ) ) ) |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( 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 ) ) ) |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( 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 ) ) ) |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) ) )
363		oveq1	|- ( y = ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) -> ( y .x. ( D ` z ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. ( D ` z ) ) )
364	363	eqeq2d	|- ( y = ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) -> ( ( 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 ) ) ) ) = ( y .x. ( 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 ) ) ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. ( D ` z ) ) ) )
365	362 364	imbi12d	|- ( y = ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) -> ( ( ( ( ( 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 ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( 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 ) ) ) |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( 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 ) ) ) ) = ( y .x. ( D ` z ) ) ) <-> ( ( ( ( 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 ) ) = ( ( ( { w } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( 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 ) ) ) |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( 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 ) ) ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. ( D ` z ) ) ) ) )
366	365	2ralbidv	|- ( y = ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) -> ( A. z e. B A. w e. 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 ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( 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 ) ) ) |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( 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 ) ) ) ) = ( y .x. ( D ` z ) ) ) <-> A. z e. B A. w e. 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 ) ) = ( ( ( { w } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( 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 ) ) ) |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( 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 ) ) ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. ( D ` z ) ) ) ) )
367	357 366	rspc2va	|- ( ( ( ( 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 /\ ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) e. K ) /\ 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 ) ) ) ) -> A. z e. B A. w e. 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 ) ) = ( ( ( { w } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( 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 ) ) ) |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( 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 ) ) ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. ( D ` z ) ) ) )
368	235 297 349 367	syl21anc	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> A. z e. B A. w e. 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 ) ) = ( ( ( { w } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( 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 ) ) ) |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( 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 ) ) ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. ( D ` z ) ) ) )
369		reseq1	|- ( z = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) -> ( z |` ( { w } X. N ) ) = ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( { w } X. N ) ) )
370	369	oveq2d	|- ( z = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) -> ( ( ( { w } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( z |` ( { w } X. N ) ) ) = ( ( ( { w } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( { w } X. N ) ) ) )
371	370	eqeq2d	|- ( z = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .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 ) ) ) |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( 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 ) ) = ( ( ( { w } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( { w } X. N ) ) ) ) )
372		reseq1	|- ( z = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) -> ( z |` ( ( N \ { w } ) X. N ) ) = ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { w } ) X. N ) ) )
373	372	eqeq2d	|- ( z = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .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 ) ) ) |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( 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 ) ) = ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { w } ) X. N ) ) ) )
374	371 373	anbi12d	|- ( z = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .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 ) ) ) |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( 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 ) ) ) |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( 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 ) ) ) |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( { 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 ) ) = ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { w } ) X. N ) ) ) ) )
375		fveq2	|- ( z = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) -> ( D ` z ) = ( D ` ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ) )
376	375	oveq2d	|- ( z = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) -> ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. ( D ` z ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. ( D ` ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ) ) )
377	376	eqeq2d	|- ( z = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) -> ( ( 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 ) ) ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. ( 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 ) ) ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. ( D ` ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ) ) ) )
378	374 377	imbi12d	|- ( z = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .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 ) ) ) |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( 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 ) ) ) |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( 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 ) ) ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. ( D ` z ) ) ) <-> ( ( ( ( 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 ) ) = ( ( ( { w } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( { 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 ) ) = ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { w } ) X. N ) ) ) -> ( 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 ) ) ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. ( D ` ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ) ) ) ) )
379	270	xpeq1d	|- ( w = ( 1st ` c ) -> ( ( { w } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) = ( ( { ( 1st ` c ) } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) )
380	270	reseq2d	|- ( w = ( 1st ` c ) -> ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( { w } X. N ) ) = ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( { ( 1st ` c ) } X. N ) ) )
381	379 380	oveq12d	|- ( w = ( 1st ` c ) -> ( ( ( { w } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( { w } X. N ) ) ) = ( ( ( { ( 1st ` c ) } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( { ( 1st ` c ) } X. N ) ) ) )
382	272 381	eqeq12d	|- ( w = ( 1st ` c ) -> ( ( ( 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 ) ) = ( ( ( { w } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( { 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 ) ) ) |` ( { ( 1st ` c ) } X. N ) ) = ( ( ( { ( 1st ` c ) } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( { ( 1st ` c ) } X. N ) ) ) ) )
383	277	reseq2d	|- ( w = ( 1st ` c ) -> ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { w } ) X. N ) ) = ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) )
384	279 383	eqeq12d	|- ( w = ( 1st ` c ) -> ( ( ( 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 ) ) = ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( ( 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 \ { ( 1st ` c ) } ) X. N ) ) = ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) ) )
385	382 384	anbi12d	|- ( w = ( 1st ` c ) -> ( ( ( ( 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 ) ) = ( ( ( { w } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( { 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 ) ) = ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( ( 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 ) ) ) |` ( { ( 1st ` c ) } X. N ) ) = ( ( ( { ( 1st ` c ) } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( 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 ) ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) = ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) ) ) )
386	385	imbi1d	|- ( w = ( 1st ` c ) -> ( ( ( ( ( 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 ) ) = ( ( ( { w } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( { 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 ) ) = ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { w } ) X. N ) ) ) -> ( 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 ) ) ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. ( D ` ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .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 ) ) ) |` ( { ( 1st ` c ) } X. N ) ) = ( ( ( { ( 1st ` c ) } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( 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 ) ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) = ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) ) -> ( 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 ) ) ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. ( D ` ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ) ) ) ) )
387	378 386	rspc2va	|- ( ( ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) e. B /\ ( 1st ` c ) e. N ) /\ A. z e. B A. w e. 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 ) ) = ( ( ( { w } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( 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 ) ) ) |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( 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 ) ) ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. ( D ` z ) ) ) ) -> ( ( ( ( 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 ) ) = ( ( ( { ( 1st ` c ) } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( 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 ) ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) = ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) ) -> ( 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 ) ) ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. ( D ` ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ) ) ) )
388	348 124 368 387	syl21anc	|- ( ( 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 ) ) = ( ( ( { ( 1st ` c ) } X. N ) X. { ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) } ) oF .x. ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( 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 ) ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) = ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) |` ( ( N \ { ( 1st ` c ) } ) X. N ) ) ) -> ( 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 ) ) ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. ( D ` ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ) ) ) )
389	332 340 388	mp2and	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( 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 ) ) ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. ( D ` ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ) ) )
390	389	oveq1d	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( 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 ` ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) ) = ( ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. ( D ` ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ) ) .+ ( D ` ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) ) )
391	104 105 106 390	syl3anc	|- ( ( ( 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. ) ) ) -> ( ( 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 ` ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) ) = ( ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. ( D ` ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ) ) .+ ( D ` ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) ) )
392		simpl3	|- ( ( ( 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 } ) e. Y )
393		simprlr	|- ( ( ( 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. ) ) ) -> d e. ( N ^m N ) )
394		simprr	|- ( ( ( 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. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) )
395		ralss	|- ( b C_ ( b u. { c } ) -> ( A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) <-> A. w e. ( b u. { c } ) ( w e. b -> ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) )
396	99 395	ax-mp	|- ( A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) <-> A. w e. ( b u. { c } ) ( w e. b -> ( a ` w ) = if ( w e. d , .1. , .0. ) ) )
397		iftrue	|- ( ( 1st ` w ) = ( 1st ` c ) -> if ( ( 1st ` w ) = ( 1st ` c ) , if ( w = c , .1. , .0. ) , ( a ` w ) ) = if ( w = c , .1. , .0. ) )
398	397	adantl	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ ( 1st ` w ) = ( 1st ` c ) ) -> if ( ( 1st ` w ) = ( 1st ` c ) , if ( w = c , .1. , .0. ) , ( a ` w ) ) = if ( w = c , .1. , .0. ) )
399		ibar	|- ( ( 1st ` w ) = ( 1st ` c ) -> ( ( 2nd ` w ) = ( 2nd ` c ) <-> ( ( 1st ` w ) = ( 1st ` c ) /\ ( 2nd ` w ) = ( 2nd ` c ) ) ) )
400	399	adantl	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ ( 1st ` w ) = ( 1st ` c ) ) -> ( ( 2nd ` w ) = ( 2nd ` c ) <-> ( ( 1st ` w ) = ( 1st ` c ) /\ ( 2nd ` w ) = ( 2nd ` c ) ) ) )
401		relxp	|- Rel ( N X. N )
402		simpl2	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) -> ( b u. { c } ) C_ ( N X. N ) )
403	402	sselda	|- ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) -> w e. ( N X. N ) )
404	403	adantr	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ ( 1st ` w ) = ( 1st ` c ) ) -> w e. ( N X. N ) )
405		1st2nd	|- ( ( Rel ( N X. N ) /\ w e. ( N X. N ) ) -> w = <. ( 1st ` w ) , ( 2nd ` w ) >. )
406	401 404 405	sylancr	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ ( 1st ` w ) = ( 1st ` c ) ) -> w = <. ( 1st ` w ) , ( 2nd ` w ) >. )
407	406	eleq1d	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ ( 1st ` w ) = ( 1st ` c ) ) -> ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) <-> <. ( 1st ` w ) , ( 2nd ` w ) >. e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) ) )
408		simpr	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) -> d e. ( N ^m N ) )
409		elmapi	|- ( d e. ( N ^m N ) -> d : N --> N )
410	409	adantl	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) -> d : N --> N )
411	124	adantr	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) -> ( 1st ` c ) e. N )
412		xp2nd	|- ( c e. ( N X. N ) -> ( 2nd ` c ) e. N )
413	122 412	syl	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( 2nd ` c ) e. N )
414	413	adantr	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) -> ( 2nd ` c ) e. N )
415		fsets	|- ( ( ( d e. ( N ^m N ) /\ d : N --> N ) /\ ( 1st ` c ) e. N /\ ( 2nd ` c ) e. N ) -> ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) : N --> N )
416	408 410 411 414 415	syl211anc	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) -> ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) : N --> N )
417	416	ffnd	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) -> ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) Fn N )
418	417	ad2antrr	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ ( 1st ` w ) = ( 1st ` c ) ) -> ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) Fn N )
419		xp1st	|- ( w e. ( N X. N ) -> ( 1st ` w ) e. N )
420	403 419	syl	|- ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) -> ( 1st ` w ) e. N )
421	420	adantr	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ ( 1st ` w ) = ( 1st ` c ) ) -> ( 1st ` w ) e. N )
422		fnopfvb	|- ( ( ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) Fn N /\ ( 1st ` w ) e. N ) -> ( ( ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) ` ( 1st ` w ) ) = ( 2nd ` w ) <-> <. ( 1st ` w ) , ( 2nd ` w ) >. e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) ) )
423	418 421 422	syl2anc	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ ( 1st ` w ) = ( 1st ` c ) ) -> ( ( ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) ` ( 1st ` w ) ) = ( 2nd ` w ) <-> <. ( 1st ` w ) , ( 2nd ` w ) >. e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) ) )
424		fveq2	|- ( ( 1st ` w ) = ( 1st ` c ) -> ( ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) ` ( 1st ` w ) ) = ( ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) ` ( 1st ` c ) ) )
425	424	adantl	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ ( 1st ` w ) = ( 1st ` c ) ) -> ( ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) ` ( 1st ` w ) ) = ( ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) ` ( 1st ` c ) ) )
426		vex	|- d e. _V
427		fvex	|- ( 1st ` c ) e. _V
428		fvex	|- ( 2nd ` c ) e. _V
429		fvsetsid	|- ( ( d e. _V /\ ( 1st ` c ) e. _V /\ ( 2nd ` c ) e. _V ) -> ( ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) ` ( 1st ` c ) ) = ( 2nd ` c ) )
430	426 427 428 429	mp3an	|- ( ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) ` ( 1st ` c ) ) = ( 2nd ` c )
431	425 430	eqtrdi	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ ( 1st ` w ) = ( 1st ` c ) ) -> ( ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) ` ( 1st ` w ) ) = ( 2nd ` c ) )
432	431	eqeq1d	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ ( 1st ` w ) = ( 1st ` c ) ) -> ( ( ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) ` ( 1st ` w ) ) = ( 2nd ` w ) <-> ( 2nd ` c ) = ( 2nd ` w ) ) )
433		eqcom	|- ( ( 2nd ` c ) = ( 2nd ` w ) <-> ( 2nd ` w ) = ( 2nd ` c ) )
434	432 433	bitrdi	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ ( 1st ` w ) = ( 1st ` c ) ) -> ( ( ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) ` ( 1st ` w ) ) = ( 2nd ` w ) <-> ( 2nd ` w ) = ( 2nd ` c ) ) )
435	407 423 434	3bitr2rd	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ ( 1st ` w ) = ( 1st ` c ) ) -> ( ( 2nd ` w ) = ( 2nd ` c ) <-> w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) ) )
436	122	ad3antrrr	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ ( 1st ` w ) = ( 1st ` c ) ) -> c e. ( N X. N ) )
437		xpopth	|- ( ( w e. ( N X. N ) /\ c e. ( N X. N ) ) -> ( ( ( 1st ` w ) = ( 1st ` c ) /\ ( 2nd ` w ) = ( 2nd ` c ) ) <-> w = c ) )
438	404 436 437	syl2anc	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ ( 1st ` w ) = ( 1st ` c ) ) -> ( ( ( 1st ` w ) = ( 1st ` c ) /\ ( 2nd ` w ) = ( 2nd ` c ) ) <-> w = c ) )
439	400 435 438	3bitr3rd	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ ( 1st ` w ) = ( 1st ` c ) ) -> ( w = c <-> w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) ) )
440	439	ifbid	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ ( 1st ` w ) = ( 1st ` c ) ) -> if ( w = c , .1. , .0. ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) )
441	398 440	eqtrd	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ ( 1st ` w ) = ( 1st ` c ) ) -> if ( ( 1st ` w ) = ( 1st ` c ) , if ( w = c , .1. , .0. ) , ( a ` w ) ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) )
442	441	a1d	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ ( 1st ` w ) = ( 1st ` c ) ) -> ( ( w e. b -> ( a ` w ) = if ( w e. d , .1. , .0. ) ) -> if ( ( 1st ` w ) = ( 1st ` c ) , if ( w = c , .1. , .0. ) , ( a ` w ) ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) ) )
443		elsni	|- ( w e. { c } -> w = c )
444	443	fveq2d	|- ( w e. { c } -> ( 1st ` w ) = ( 1st ` c ) )
445	444	con3i	|- ( -. ( 1st ` w ) = ( 1st ` c ) -> -. w e. { c } )
446	445	adantl	|- ( ( w e. ( b u. { c } ) /\ -. ( 1st ` w ) = ( 1st ` c ) ) -> -. w e. { c } )
447		elun	|- ( w e. ( b u. { c } ) <-> ( w e. b \/ w e. { c } ) )
448	447	biimpi	|- ( w e. ( b u. { c } ) -> ( w e. b \/ w e. { c } ) )
449	448	adantr	|- ( ( w e. ( b u. { c } ) /\ -. ( 1st ` w ) = ( 1st ` c ) ) -> ( w e. b \/ w e. { c } ) )
450		orel2	|- ( -. w e. { c } -> ( ( w e. b \/ w e. { c } ) -> w e. b ) )
451	446 449 450	sylc	|- ( ( w e. ( b u. { c } ) /\ -. ( 1st ` w ) = ( 1st ` c ) ) -> w e. b )
452	451	adantll	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ -. ( 1st ` w ) = ( 1st ` c ) ) -> w e. b )
453		iffalse	|- ( -. ( 1st ` w ) = ( 1st ` c ) -> if ( ( 1st ` w ) = ( 1st ` c ) , if ( w = c , .1. , .0. ) , if ( w e. d , .1. , .0. ) ) = if ( w e. d , .1. , .0. ) )
454	453	adantl	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ -. ( 1st ` w ) = ( 1st ` c ) ) -> if ( ( 1st ` w ) = ( 1st ` c ) , if ( w = c , .1. , .0. ) , if ( w e. d , .1. , .0. ) ) = if ( w e. d , .1. , .0. ) )
455		setsres	|- ( d e. _V -> ( ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) |` ( _V \ { ( 1st ` c ) } ) ) = ( d |` ( _V \ { ( 1st ` c ) } ) ) )
456	455	eleq2d	|- ( d e. _V -> ( <. ( 1st ` w ) , ( 2nd ` w ) >. e. ( ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) |` ( _V \ { ( 1st ` c ) } ) ) <-> <. ( 1st ` w ) , ( 2nd ` w ) >. e. ( d |` ( _V \ { ( 1st ` c ) } ) ) ) )
457	426 456	mp1i	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ -. ( 1st ` w ) = ( 1st ` c ) ) -> ( <. ( 1st ` w ) , ( 2nd ` w ) >. e. ( ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) |` ( _V \ { ( 1st ` c ) } ) ) <-> <. ( 1st ` w ) , ( 2nd ` w ) >. e. ( d |` ( _V \ { ( 1st ` c ) } ) ) ) )
458		fvex	|- ( 1st ` w ) e. _V
459	458	a1i	|- ( -. ( 1st ` w ) = ( 1st ` c ) -> ( 1st ` w ) e. _V )
460		neqne	|- ( -. ( 1st ` w ) = ( 1st ` c ) -> ( 1st ` w ) =/= ( 1st ` c ) )
461		eldifsn	|- ( ( 1st ` w ) e. ( _V \ { ( 1st ` c ) } ) <-> ( ( 1st ` w ) e. _V /\ ( 1st ` w ) =/= ( 1st ` c ) ) )
462	459 460 461	sylanbrc	|- ( -. ( 1st ` w ) = ( 1st ` c ) -> ( 1st ` w ) e. ( _V \ { ( 1st ` c ) } ) )
463		fvex	|- ( 2nd ` w ) e. _V
464	463	opres	|- ( ( 1st ` w ) e. ( _V \ { ( 1st ` c ) } ) -> ( <. ( 1st ` w ) , ( 2nd ` w ) >. e. ( ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) |` ( _V \ { ( 1st ` c ) } ) ) <-> <. ( 1st ` w ) , ( 2nd ` w ) >. e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) ) )
465	464	adantl	|- ( ( w e. ( N X. N ) /\ ( 1st ` w ) e. ( _V \ { ( 1st ` c ) } ) ) -> ( <. ( 1st ` w ) , ( 2nd ` w ) >. e. ( ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) |` ( _V \ { ( 1st ` c ) } ) ) <-> <. ( 1st ` w ) , ( 2nd ` w ) >. e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) ) )
466		1st2nd2	|- ( w e. ( N X. N ) -> w = <. ( 1st ` w ) , ( 2nd ` w ) >. )
467	466	eleq1d	|- ( w e. ( N X. N ) -> ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) <-> <. ( 1st ` w ) , ( 2nd ` w ) >. e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) ) )
468	467	adantr	|- ( ( w e. ( N X. N ) /\ ( 1st ` w ) e. ( _V \ { ( 1st ` c ) } ) ) -> ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) <-> <. ( 1st ` w ) , ( 2nd ` w ) >. e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) ) )
469	465 468	bitr4d	|- ( ( w e. ( N X. N ) /\ ( 1st ` w ) e. ( _V \ { ( 1st ` c ) } ) ) -> ( <. ( 1st ` w ) , ( 2nd ` w ) >. e. ( ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) |` ( _V \ { ( 1st ` c ) } ) ) <-> w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) ) )
470	403 462 469	syl2an	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ -. ( 1st ` w ) = ( 1st ` c ) ) -> ( <. ( 1st ` w ) , ( 2nd ` w ) >. e. ( ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) |` ( _V \ { ( 1st ` c ) } ) ) <-> w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) ) )
471	463	opres	|- ( ( 1st ` w ) e. ( _V \ { ( 1st ` c ) } ) -> ( <. ( 1st ` w ) , ( 2nd ` w ) >. e. ( d |` ( _V \ { ( 1st ` c ) } ) ) <-> <. ( 1st ` w ) , ( 2nd ` w ) >. e. d ) )
472	471	adantl	|- ( ( w e. ( N X. N ) /\ ( 1st ` w ) e. ( _V \ { ( 1st ` c ) } ) ) -> ( <. ( 1st ` w ) , ( 2nd ` w ) >. e. ( d |` ( _V \ { ( 1st ` c ) } ) ) <-> <. ( 1st ` w ) , ( 2nd ` w ) >. e. d ) )
473	466	eleq1d	|- ( w e. ( N X. N ) -> ( w e. d <-> <. ( 1st ` w ) , ( 2nd ` w ) >. e. d ) )
474	473	adantr	|- ( ( w e. ( N X. N ) /\ ( 1st ` w ) e. ( _V \ { ( 1st ` c ) } ) ) -> ( w e. d <-> <. ( 1st ` w ) , ( 2nd ` w ) >. e. d ) )
475	472 474	bitr4d	|- ( ( w e. ( N X. N ) /\ ( 1st ` w ) e. ( _V \ { ( 1st ` c ) } ) ) -> ( <. ( 1st ` w ) , ( 2nd ` w ) >. e. ( d |` ( _V \ { ( 1st ` c ) } ) ) <-> w e. d ) )
476	403 462 475	syl2an	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ -. ( 1st ` w ) = ( 1st ` c ) ) -> ( <. ( 1st ` w ) , ( 2nd ` w ) >. e. ( d |` ( _V \ { ( 1st ` c ) } ) ) <-> w e. d ) )
477	457 470 476	3bitr3rd	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ -. ( 1st ` w ) = ( 1st ` c ) ) -> ( w e. d <-> w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) ) )
478	477	ifbid	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ -. ( 1st ` w ) = ( 1st ` c ) ) -> if ( w e. d , .1. , .0. ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) )
479	454 478	eqtrd	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ -. ( 1st ` w ) = ( 1st ` c ) ) -> if ( ( 1st ` w ) = ( 1st ` c ) , if ( w = c , .1. , .0. ) , if ( w e. d , .1. , .0. ) ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) )
480		ifeq2	|- ( ( a ` w ) = if ( w e. d , .1. , .0. ) -> if ( ( 1st ` w ) = ( 1st ` c ) , if ( w = c , .1. , .0. ) , ( a ` w ) ) = if ( ( 1st ` w ) = ( 1st ` c ) , if ( w = c , .1. , .0. ) , if ( w e. d , .1. , .0. ) ) )
481	480	eqeq1d	|- ( ( a ` w ) = if ( w e. d , .1. , .0. ) -> ( if ( ( 1st ` w ) = ( 1st ` c ) , if ( w = c , .1. , .0. ) , ( a ` w ) ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) <-> if ( ( 1st ` w ) = ( 1st ` c ) , if ( w = c , .1. , .0. ) , if ( w e. d , .1. , .0. ) ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) ) )
482	479 481	syl5ibrcom	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ -. ( 1st ` w ) = ( 1st ` c ) ) -> ( ( a ` w ) = if ( w e. d , .1. , .0. ) -> if ( ( 1st ` w ) = ( 1st ` c ) , if ( w = c , .1. , .0. ) , ( a ` w ) ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) ) )
483	452 482	embantd	|- ( ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) /\ -. ( 1st ` w ) = ( 1st ` c ) ) -> ( ( w e. b -> ( a ` w ) = if ( w e. d , .1. , .0. ) ) -> if ( ( 1st ` w ) = ( 1st ` c ) , if ( w = c , .1. , .0. ) , ( a ` w ) ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) ) )
484	442 483	pm2.61dan	|- ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) -> ( ( w e. b -> ( a ` w ) = if ( w e. d , .1. , .0. ) ) -> if ( ( 1st ` w ) = ( 1st ` c ) , if ( w = c , .1. , .0. ) , ( a ` w ) ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) ) )
485		fveqeq2	|- ( e = w -> ( ( 1st ` e ) = ( 1st ` c ) <-> ( 1st ` w ) = ( 1st ` c ) ) )
486		equequ1	|- ( e = w -> ( e = c <-> w = c ) )
487	486	ifbid	|- ( e = w -> if ( e = c , .1. , .0. ) = if ( w = c , .1. , .0. ) )
488		fveq2	|- ( e = w -> ( a ` e ) = ( a ` w ) )
489	485 487 488	ifbieq12d	|- ( e = w -> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) = if ( ( 1st ` w ) = ( 1st ` c ) , if ( w = c , .1. , .0. ) , ( a ` w ) ) )
490		eqid	|- ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) )
491	165 162	ifex	|- if ( w = c , .1. , .0. ) e. _V
492		fvex	|- ( a ` w ) e. _V
493	491 492	ifex	|- if ( ( 1st ` w ) = ( 1st ` c ) , if ( w = c , .1. , .0. ) , ( a ` w ) ) e. _V
494	489 490 493	fvmpt	|- ( w e. ( N X. N ) -> ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( ( 1st ` w ) = ( 1st ` c ) , if ( w = c , .1. , .0. ) , ( a ` w ) ) )
495	494	eqeq1d	|- ( w e. ( N X. N ) -> ( ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) <-> if ( ( 1st ` w ) = ( 1st ` c ) , if ( w = c , .1. , .0. ) , ( a ` w ) ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) ) )
496	403 495	syl	|- ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) -> ( ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) <-> if ( ( 1st ` w ) = ( 1st ` c ) , if ( w = c , .1. , .0. ) , ( a ` w ) ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) ) )
497	484 496	sylibrd	|- ( ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) /\ w e. ( b u. { c } ) ) -> ( ( w e. b -> ( a ` w ) = if ( w e. d , .1. , .0. ) ) -> ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) ) )
498	497	ralimdva	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) -> ( A. w e. ( b u. { c } ) ( w e. b -> ( a ` w ) = if ( w e. d , .1. , .0. ) ) -> A. w e. ( b u. { c } ) ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) ) )
499	396 498	syl5bi	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ d e. ( N ^m N ) ) -> ( A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) -> A. w e. ( b u. { c } ) ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) ) )
500	499	impr	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> A. w e. ( b u. { c } ) ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) )
501	500	3adantr1	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> A. w e. ( b u. { c } ) ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) )
502	348	adantr	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) e. B )
503		simpr2	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> d e. ( N ^m N ) )
504	503 409	syl	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> d : N --> N )
505	124	adantr	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> ( 1st ` c ) e. N )
506	413	adantr	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> ( 2nd ` c ) e. N )
507	503 504 505 506 415	syl211anc	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) : N --> N )
508	158 158	elmapd	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) e. ( N ^m N ) <-> ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) : N --> N ) )
509	508	adantr	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> ( ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) e. ( N ^m N ) <-> ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) : N --> N ) )
510	507 509	mpbird	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) e. ( N ^m N ) )
511		simpr1	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> ( b u. { c } ) e. Y )
512		raleq	|- ( x = ( b u. { c } ) -> ( A. w e. x ( y ` w ) = if ( w e. z , .1. , .0. ) <-> A. w e. ( b u. { c } ) ( y ` w ) = if ( w e. z , .1. , .0. ) ) )
513	512	imbi1d	|- ( x = ( b u. { c } ) -> ( ( A. w e. x ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) <-> ( A. w e. ( b u. { c } ) ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) ) )
514	513	2ralbidv	|- ( x = ( b u. { c } ) -> ( 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. ( b u. { c } ) ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) ) )
515	514 15	elab2g	|- ( ( b u. { c } ) e. Y -> ( ( b u. { c } ) e. Y <-> A. y e. B A. z e. ( N ^m N ) ( A. w e. ( b u. { c } ) ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) ) )
516	515	ibi	|- ( ( b u. { c } ) e. Y -> A. y e. B A. z e. ( N ^m N ) ( A. w e. ( b u. { c } ) ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) )
517	511 516	syl	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> A. y e. B A. z e. ( N ^m N ) ( A. w e. ( b u. { c } ) ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) )
518		fveq1	|- ( y = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) -> ( y ` w ) = ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ` w ) )
519	518	eqeq1d	|- ( y = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) -> ( ( y ` w ) = if ( w e. z , .1. , .0. ) <-> ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. z , .1. , .0. ) ) )
520	519	ralbidv	|- ( y = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) -> ( A. w e. ( b u. { c } ) ( y ` w ) = if ( w e. z , .1. , .0. ) <-> A. w e. ( b u. { c } ) ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. z , .1. , .0. ) ) )
521		fveqeq2	|- ( y = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) -> ( ( D ` y ) = .0. <-> ( D ` ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ) = .0. ) )
522	520 521	imbi12d	|- ( y = ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) -> ( ( A. w e. ( b u. { c } ) ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) <-> ( A. w e. ( b u. { c } ) ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ) = .0. ) ) )
523		eleq2	|- ( z = ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) -> ( w e. z <-> w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) ) )
524	523	ifbid	|- ( z = ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) -> if ( w e. z , .1. , .0. ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) )
525	524	eqeq2d	|- ( z = ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) -> ( ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. z , .1. , .0. ) <-> ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) ) )
526	525	ralbidv	|- ( z = ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) -> ( A. w e. ( b u. { c } ) ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. z , .1. , .0. ) <-> A. w e. ( b u. { c } ) ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) ) )
527	526	imbi1d	|- ( z = ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) -> ( ( A. w e. ( b u. { c } ) ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ) = .0. ) <-> ( A. w e. ( b u. { c } ) ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) -> ( D ` ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ) = .0. ) ) )
528	522 527	rspc2va	|- ( ( ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) e. B /\ ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) e. ( N ^m N ) ) /\ A. y e. B A. z e. ( N ^m N ) ( A. w e. ( b u. { c } ) ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) ) -> ( A. w e. ( b u. { c } ) ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) -> ( D ` ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ) = .0. ) )
529	502 510 517 528	syl21anc	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> ( A. w e. ( b u. { c } ) ( ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. ( d sSet <. ( 1st ` c ) , ( 2nd ` c ) >. ) , .1. , .0. ) -> ( D ` ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ) = .0. ) )
530	501 529	mpd	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> ( D ` ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ) = .0. )
531	530	oveq2d	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. ( D ` ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ) ) = ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. .0. ) )
532	118	unssad	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> b C_ ( N X. N ) )
533	532	adantr	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> b C_ ( N X. N ) )
534		simpr3	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) )
535		ssel2	|- ( ( b C_ ( N X. N ) /\ w e. b ) -> w e. ( N X. N ) )
536	535	adantr	|- ( ( ( b C_ ( N X. N ) /\ w e. b ) /\ ( a ` w ) = if ( w e. d , .1. , .0. ) ) -> w e. ( N X. N ) )
537		elequ1	|- ( e = w -> ( e e. d <-> w e. d ) )
538	537	ifbid	|- ( e = w -> if ( e e. d , .1. , .0. ) = if ( w e. d , .1. , .0. ) )
539	486 538 488	ifbieq12d	|- ( e = w -> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) = if ( w = c , if ( w e. d , .1. , .0. ) , ( a ` w ) ) )
540		eqid	|- ( 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 ) ) )
541	165 162	ifex	|- if ( w e. d , .1. , .0. ) e. _V
542	541 492	ifex	|- if ( w = c , if ( w e. d , .1. , .0. ) , ( a ` w ) ) e. _V
543	539 540 542	fvmpt	|- ( w e. ( N X. N ) -> ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w = c , if ( w e. d , .1. , .0. ) , ( a ` w ) ) )
544	536 543	syl	|- ( ( ( b C_ ( N X. N ) /\ w e. b ) /\ ( a ` w ) = if ( w e. d , .1. , .0. ) ) -> ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w = c , if ( w e. d , .1. , .0. ) , ( a ` w ) ) )
545		ifeq2	|- ( ( a ` w ) = if ( w e. d , .1. , .0. ) -> if ( w = c , if ( w e. d , .1. , .0. ) , ( a ` w ) ) = if ( w = c , if ( w e. d , .1. , .0. ) , if ( w e. d , .1. , .0. ) ) )
546	545	adantl	|- ( ( ( b C_ ( N X. N ) /\ w e. b ) /\ ( a ` w ) = if ( w e. d , .1. , .0. ) ) -> if ( w = c , if ( w e. d , .1. , .0. ) , ( a ` w ) ) = if ( w = c , if ( w e. d , .1. , .0. ) , if ( w e. d , .1. , .0. ) ) )
547		ifid	|- if ( w = c , if ( w e. d , .1. , .0. ) , if ( w e. d , .1. , .0. ) ) = if ( w e. d , .1. , .0. )
548	546 547	eqtrdi	|- ( ( ( b C_ ( N X. N ) /\ w e. b ) /\ ( a ` w ) = if ( w e. d , .1. , .0. ) ) -> if ( w = c , if ( w e. d , .1. , .0. ) , ( a ` w ) ) = if ( w e. d , .1. , .0. ) )
549	544 548	eqtrd	|- ( ( ( b C_ ( N X. N ) /\ w e. b ) /\ ( a ` w ) = if ( w e. d , .1. , .0. ) ) -> ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. d , .1. , .0. ) )
550	549	ex	|- ( ( b C_ ( N X. N ) /\ w e. b ) -> ( ( a ` w ) = if ( w e. d , .1. , .0. ) -> ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. d , .1. , .0. ) ) )
551	550	ralimdva	|- ( b C_ ( N X. N ) -> ( A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) -> A. w e. b ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. d , .1. , .0. ) ) )
552	533 534 551	sylc	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> A. w e. b ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. d , .1. , .0. ) )
553	142 291	eqtrd	|- ( e = c -> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) = if ( c e. d , .1. , .0. ) )
554	165 162	ifex	|- if ( c e. d , .1. , .0. ) e. _V
555	553 540 554	fvmpt	|- ( c e. ( N X. N ) -> ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` c ) = if ( c e. d , .1. , .0. ) )
556	122 555	syl	|- ( ( 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 ) ) ) ` c ) = if ( c e. d , .1. , .0. ) )
557	556	adantr	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` c ) = if ( c e. d , .1. , .0. ) )
558		fveq2	|- ( w = c -> ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) = ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` c ) )
559		elequ1	|- ( w = c -> ( w e. d <-> c e. d ) )
560	559	ifbid	|- ( w = c -> if ( w e. d , .1. , .0. ) = if ( c e. d , .1. , .0. ) )
561	558 560	eqeq12d	|- ( w = c -> ( ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. d , .1. , .0. ) <-> ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` c ) = if ( c e. d , .1. , .0. ) ) )
562	561	ralunsn	|- ( c e. _V -> ( A. w e. ( b u. { c } ) ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. d , .1. , .0. ) <-> ( A. w e. b ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. d , .1. , .0. ) /\ ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` c ) = if ( c e. d , .1. , .0. ) ) ) )
563	562	elv	|- ( A. w e. ( b u. { c } ) ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. d , .1. , .0. ) <-> ( A. w e. b ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. d , .1. , .0. ) /\ ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` c ) = if ( c e. d , .1. , .0. ) ) )
564	552 557 563	sylanbrc	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> A. w e. ( b u. { c } ) ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. d , .1. , .0. ) )
565	223	adantr	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) e. B )
566		fveq1	|- ( y = ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) -> ( y ` w ) = ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) )
567	566	eqeq1d	|- ( y = ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) -> ( ( y ` w ) = if ( w e. z , .1. , .0. ) <-> ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. z , .1. , .0. ) ) )
568	567	ralbidv	|- ( y = ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) -> ( A. w e. ( b u. { c } ) ( y ` w ) = if ( w e. z , .1. , .0. ) <-> A. w e. ( b u. { c } ) ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. z , .1. , .0. ) ) )
569		fveqeq2	|- ( y = ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) -> ( ( D ` y ) = .0. <-> ( D ` ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) = .0. ) )
570	568 569	imbi12d	|- ( y = ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) -> ( ( A. w e. ( b u. { c } ) ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) <-> ( A. w e. ( b u. { c } ) ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) = .0. ) ) )
571		elequ2	|- ( z = d -> ( w e. z <-> w e. d ) )
572	571	ifbid	|- ( z = d -> if ( w e. z , .1. , .0. ) = if ( w e. d , .1. , .0. ) )
573	572	eqeq2d	|- ( z = d -> ( ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. z , .1. , .0. ) <-> ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. d , .1. , .0. ) ) )
574	573	ralbidv	|- ( z = d -> ( A. w e. ( b u. { c } ) ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. z , .1. , .0. ) <-> A. w e. ( b u. { c } ) ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. d , .1. , .0. ) ) )
575	574	imbi1d	|- ( z = d -> ( ( A. w e. ( b u. { c } ) ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) = .0. ) <-> ( A. w e. ( b u. { c } ) ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. d , .1. , .0. ) -> ( D ` ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) = .0. ) ) )
576	570 575	rspc2va	|- ( ( ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) e. B /\ d e. ( N ^m N ) ) /\ A. y e. B A. z e. ( N ^m N ) ( A. w e. ( b u. { c } ) ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) ) -> ( A. w e. ( b u. { c } ) ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. d , .1. , .0. ) -> ( D ` ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) = .0. ) )
577	565 503 517 576	syl21anc	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> ( A. w e. ( b u. { c } ) ( ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ` w ) = if ( w e. d , .1. , .0. ) -> ( D ` ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) = .0. ) )
578	564 577	mpd	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> ( D ` ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) = .0. )
579	531 578	oveq12d	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> ( ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. ( D ` ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ) ) .+ ( D ` ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) ) = ( ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. .0. ) .+ .0. ) )
580	308	oveq1d	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. .0. ) .+ .0. ) = ( .0. .+ .0. ) )
581	3 6 4	grplid	|- ( ( R e. Grp /\ .0. e. K ) -> ( .0. .+ .0. ) = .0. )
582	115 133 581	syl2anc	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( .0. .+ .0. ) = .0. )
583	580 582	eqtrd	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) -> ( ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. .0. ) .+ .0. ) = .0. )
584	583	adantr	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> ( ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. .0. ) .+ .0. ) = .0. )
585	579 584	eqtrd	|- ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ a e. B ) /\ ( ( b u. { c } ) e. Y /\ d e. ( N ^m N ) /\ A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) ) ) -> ( ( ( ( a ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. ( D ` ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ) ) .+ ( D ` ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) ) = .0. )
586	104 105 106 392 393 394 585	syl33anc	|- ( ( ( 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 ` c ) ( -g ` R ) if ( c e. d , .1. , .0. ) ) .x. ( D ` ( e e. ( N X. N ) |-> if ( ( 1st ` e ) = ( 1st ` c ) , if ( e = c , .1. , .0. ) , ( a ` e ) ) ) ) ) .+ ( D ` ( e e. ( N X. N ) |-> if ( e = c , if ( e e. d , .1. , .0. ) , ( a ` e ) ) ) ) ) = .0. )
587	288 391 586	3eqtrd	|- ( ( ( 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. ) ) ) -> ( D ` a ) = .0. )
588	587	expr	|- ( ( ( 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. ) -> ( D ` a ) = .0. ) )
589	588	ralrimivva	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ ( b u. { c } ) e. Y ) -> A. a e. B A. d e. ( N ^m N ) ( A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) -> ( D ` a ) = .0. ) )
590		fveq1	|- ( a = y -> ( a ` w ) = ( y ` w ) )
591	590	eqeq1d	|- ( a = y -> ( ( a ` w ) = if ( w e. d , .1. , .0. ) <-> ( y ` w ) = if ( w e. d , .1. , .0. ) ) )
592	591	ralbidv	|- ( a = y -> ( A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) <-> A. w e. b ( y ` w ) = if ( w e. d , .1. , .0. ) ) )
593		fveqeq2	|- ( a = y -> ( ( D ` a ) = .0. <-> ( D ` y ) = .0. ) )
594	592 593	imbi12d	|- ( a = y -> ( ( A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) -> ( D ` a ) = .0. ) <-> ( A. w e. b ( y ` w ) = if ( w e. d , .1. , .0. ) -> ( D ` y ) = .0. ) ) )
595		elequ2	|- ( d = z -> ( w e. d <-> w e. z ) )
596	595	ifbid	|- ( d = z -> if ( w e. d , .1. , .0. ) = if ( w e. z , .1. , .0. ) )
597	596	eqeq2d	|- ( d = z -> ( ( y ` w ) = if ( w e. d , .1. , .0. ) <-> ( y ` w ) = if ( w e. z , .1. , .0. ) ) )
598	597	ralbidv	|- ( d = z -> ( A. w e. b ( y ` w ) = if ( w e. d , .1. , .0. ) <-> A. w e. b ( y ` w ) = if ( w e. z , .1. , .0. ) ) )
599	598	imbi1d	|- ( d = z -> ( ( A. w e. b ( y ` w ) = if ( w e. d , .1. , .0. ) -> ( D ` y ) = .0. ) <-> ( A. w e. b ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) ) )
600	594 599	cbvral2vw	|- ( A. a e. B A. d e. ( N ^m N ) ( A. w e. b ( a ` w ) = if ( w e. d , .1. , .0. ) -> ( D ` a ) = .0. ) <-> A. y e. B A. z e. ( N ^m N ) ( A. w e. b ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) )
601	589 600	sylib	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ ( b u. { c } ) e. Y ) -> A. y e. B A. z e. ( N ^m N ) ( A. w e. b ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) )
602		vex	|- b e. _V
603		raleq	|- ( x = b -> ( A. w e. x ( y ` w ) = if ( w e. z , .1. , .0. ) <-> A. w e. b ( y ` w ) = if ( w e. z , .1. , .0. ) ) )
604	603	imbi1d	|- ( x = b -> ( ( A. w e. x ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) <-> ( A. w e. b ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) ) )
605	604	2ralbidv	|- ( x = b -> ( 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. b ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) ) )
606	602 605 15	elab2	|- ( b e. Y <-> A. y e. B A. z e. ( N ^m N ) ( A. w e. b ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) )
607	601 606	sylibr	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ ( b u. { c } ) e. Y ) -> b e. Y )
608	607	3expia	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) ) -> ( ( b u. { c } ) e. Y -> b e. Y ) )
609	608	con3d	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) ) -> ( -. b e. Y -> -. ( b u. { c } ) e. Y ) )
610	609	3adant3	|- ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ -. (/) e. Y ) -> ( -. b e. Y -> -. ( b u. { c } ) e. Y ) )
611	610	a1i	|- ( ( b e. Fin /\ -. c e. b ) -> ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ -. (/) e. Y ) -> ( -. b e. Y -> -. ( b u. { c } ) e. Y ) ) )
612	611	a2d	|- ( ( b e. Fin /\ -. c e. b ) -> ( ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ -. (/) e. Y ) -> -. b e. Y ) -> ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ -. (/) e. Y ) -> -. ( b u. { c } ) e. Y ) ) )
613	103 612	syl5	|- ( ( b e. Fin /\ -. c e. b ) -> ( ( ( ph /\ b C_ ( N X. N ) /\ -. (/) e. Y ) -> -. b e. Y ) -> ( ( ph /\ ( b u. { c } ) C_ ( N X. N ) /\ -. (/) e. Y ) -> -. ( b u. { c } ) e. Y ) ) )
614	82 87 92 97 98 613	findcard2s	|- ( ( N X. N ) e. Fin -> ( ( ph /\ ( N X. N ) C_ ( N X. N ) /\ -. (/) e. Y ) -> -. ( N X. N ) e. Y ) )
615	77 614	mpcom	|- ( ( ph /\ ( N X. N ) C_ ( N X. N ) /\ -. (/) e. Y ) -> -. ( N X. N ) e. Y )
616	615	3exp	|- ( ph -> ( ( N X. N ) C_ ( N X. N ) -> ( -. (/) e. Y -> -. ( N X. N ) e. Y ) ) )
617	76 616	mpi	|- ( ph -> ( -. (/) e. Y -> -. ( N X. N ) e. Y ) )
618	75 617	mt4d	|- ( ph -> (/) e. Y )
619	618	adantr	|- ( ( ph /\ a e. B ) -> (/) e. Y )
620		0ex	|- (/) e. _V
621		raleq	|- ( x = (/) -> ( A. w e. x ( y ` w ) = if ( w e. z , .1. , .0. ) <-> A. w e. (/) ( y ` w ) = if ( w e. z , .1. , .0. ) ) )
622	621	imbi1d	|- ( x = (/) -> ( ( A. w e. x ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) <-> ( A. w e. (/) ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) ) )
623	622	2ralbidv	|- ( 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. ) <-> A. y e. B A. z e. ( N ^m N ) ( A. w e. (/) ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) ) )
624	620 623 15	elab2	|- ( (/) e. Y <-> A. y e. B A. z e. ( N ^m N ) ( A. w e. (/) ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) )
625	619 624	sylib	|- ( ( ph /\ a e. B ) -> A. y e. B A. z e. ( N ^m N ) ( A. w e. (/) ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) )
626		fveq1	|- ( y = a -> ( y ` w ) = ( a ` w ) )
627	626	eqeq1d	|- ( y = a -> ( ( y ` w ) = if ( w e. z , .1. , .0. ) <-> ( a ` w ) = if ( w e. z , .1. , .0. ) ) )
628	627	ralbidv	|- ( y = a -> ( A. w e. (/) ( y ` w ) = if ( w e. z , .1. , .0. ) <-> A. w e. (/) ( a ` w ) = if ( w e. z , .1. , .0. ) ) )
629		fveqeq2	|- ( y = a -> ( ( D ` y ) = .0. <-> ( D ` a ) = .0. ) )
630	628 629	imbi12d	|- ( y = a -> ( ( A. w e. (/) ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) <-> ( A. w e. (/) ( a ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` a ) = .0. ) ) )
631		eleq2	|- ( z = ( _I |` N ) -> ( w e. z <-> w e. ( _I |` N ) ) )
632	631	ifbid	|- ( z = ( _I |` N ) -> if ( w e. z , .1. , .0. ) = if ( w e. ( _I |` N ) , .1. , .0. ) )
633	632	eqeq2d	|- ( z = ( _I |` N ) -> ( ( a ` w ) = if ( w e. z , .1. , .0. ) <-> ( a ` w ) = if ( w e. ( _I |` N ) , .1. , .0. ) ) )
634	633	ralbidv	|- ( z = ( _I |` N ) -> ( A. w e. (/) ( a ` w ) = if ( w e. z , .1. , .0. ) <-> A. w e. (/) ( a ` w ) = if ( w e. ( _I |` N ) , .1. , .0. ) ) )
635	634	imbi1d	|- ( z = ( _I |` N ) -> ( ( A. w e. (/) ( a ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` a ) = .0. ) <-> ( A. w e. (/) ( a ` w ) = if ( w e. ( _I |` N ) , .1. , .0. ) -> ( D ` a ) = .0. ) ) )
636	630 635	rspc2va	|- ( ( ( a e. B /\ ( _I |` N ) e. ( N ^m N ) ) /\ A. y e. B A. z e. ( N ^m N ) ( A. w e. (/) ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) ) -> ( A. w e. (/) ( a ` w ) = if ( w e. ( _I |` N ) , .1. , .0. ) -> ( D ` a ) = .0. ) )
637	17 23 625 636	syl21anc	|- ( ( ph /\ a e. B ) -> ( A. w e. (/) ( a ` w ) = if ( w e. ( _I |` N ) , .1. , .0. ) -> ( D ` a ) = .0. ) )
638	16 637	mpi	|- ( ( ph /\ a e. B ) -> ( D ` a ) = .0. )
639	638	mpteq2dva	|- ( ph -> ( a e. B |-> ( D ` a ) ) = ( a e. B |-> .0. ) )
640	10	feqmptd	|- ( ph -> D = ( a e. B |-> ( D ` a ) ) )
641		fconstmpt	|- ( B X. { .0. } ) = ( a e. B |-> .0. )
642	641	a1i	|- ( ph -> ( B X. { .0. } ) = ( a e. B |-> .0. ) )
643	639 640 642	3eqtr4d	|- ( ph -> D = ( B X. { .0. } ) )