This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( ( 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 ffvelcdmda 
 |-  ( ( ( 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 ffvelcdmd 
 |-  ( ( 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 biimtrid 
 |-  ( ( ( 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. } ) )