Metamath Proof Explorer

Theorem mdetunilem3

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 ) ) ) )
Assertion mdetunilem3 
|- ( ( ( ph /\ E e. B /\ F e. B ) /\ ( G e. B /\ H e. N /\ ( E |` ( { H } X. N ) ) = ( ( F |` ( { H } X. N ) ) oF .+ ( G |` ( { H } X. N ) ) ) ) /\ ( ( E |` ( ( N \ { H } ) X. N ) ) = ( F |` ( ( N \ { H } ) X. N ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) ) -> ( D ` E ) = ( ( D ` F ) .+ ( D ` G ) ) )

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 simp23 
 |-  ( ( ( ph /\ E e. B /\ F e. B ) /\ ( G e. B /\ H e. N /\ ( E |` ( { H } X. N ) ) = ( ( F |` ( { H } X. N ) ) oF .+ ( G |` ( { H } X. N ) ) ) ) /\ ( ( E |` ( ( N \ { H } ) X. N ) ) = ( F |` ( ( N \ { H } ) X. N ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) ) -> ( E |` ( { H } X. N ) ) = ( ( F |` ( { H } X. N ) ) oF .+ ( G |` ( { H } X. N ) ) ) )
15 simp3l 
 |-  ( ( ( ph /\ E e. B /\ F e. B ) /\ ( G e. B /\ H e. N /\ ( E |` ( { H } X. N ) ) = ( ( F |` ( { H } X. N ) ) oF .+ ( G |` ( { H } X. N ) ) ) ) /\ ( ( E |` ( ( N \ { H } ) X. N ) ) = ( F |` ( ( N \ { H } ) X. N ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) ) -> ( E |` ( ( N \ { H } ) X. N ) ) = ( F |` ( ( N \ { H } ) X. N ) ) )
16 simp3r 
 |-  ( ( ( ph /\ E e. B /\ F e. B ) /\ ( G e. B /\ H e. N /\ ( E |` ( { H } X. N ) ) = ( ( F |` ( { H } X. N ) ) oF .+ ( G |` ( { H } X. N ) ) ) ) /\ ( ( E |` ( ( N \ { H } ) X. N ) ) = ( F |` ( ( N \ { H } ) X. N ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) ) -> ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) )
17 simprl 
 |-  ( ( ( ph /\ E e. B /\ F e. B ) /\ ( G e. B /\ H e. N ) ) -> G e. B )
18 simprr 
 |-  ( ( ( ph /\ E e. B /\ F e. B ) /\ ( G e. B /\ H e. N ) ) -> H e. N )
19 simpl2 
 |-  ( ( ( ph /\ E e. B /\ F e. B ) /\ ( G e. B /\ H e. N ) ) -> E e. B )
20 simpl3 
 |-  ( ( ( ph /\ E e. B /\ F e. B ) /\ ( G e. B /\ H e. N ) ) -> F e. B )
21 simpl1 
 |-  ( ( ( ph /\ E e. B /\ F e. B ) /\ ( G e. B /\ H e. N ) ) -> ph )
22 21 12 syl 
 |-  ( ( ( ph /\ E e. B /\ F e. B ) /\ ( G e. B /\ H e. N ) ) -> 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 ) ) ) )
23 reseq1 
 |-  ( x = E -> ( x |` ( { w } X. N ) ) = ( E |` ( { w } X. N ) ) )
24 23 eqeq1d 
 |-  ( x = E -> ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) <-> ( E |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) ) )
25 reseq1 
 |-  ( x = E -> ( x |` ( ( N \ { w } ) X. N ) ) = ( E |` ( ( N \ { w } ) X. N ) ) )
26 25 eqeq1d 
 |-  ( x = E -> ( ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) <-> ( E |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) ) )
27 25 eqeq1d 
 |-  ( x = E -> ( ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) <-> ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) )
28 24 26 27 3anbi123d 
 |-  ( x = E -> ( ( ( 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 ) ) ) <-> ( ( E |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) ) )
29 fveq2 
 |-  ( x = E -> ( D ` x ) = ( D ` E ) )
30 29 eqeq1d 
 |-  ( x = E -> ( ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) <-> ( D ` E ) = ( ( D ` y ) .+ ( D ` z ) ) ) )
31 28 30 imbi12d 
 |-  ( x = E -> ( ( ( ( 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 ) ) ) <-> ( ( ( E |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` E ) = ( ( D ` y ) .+ ( D ` z ) ) ) ) )
32 31 2ralbidv 
 |-  ( x = E -> ( 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 ( ( ( E |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` E ) = ( ( D ` y ) .+ ( D ` z ) ) ) ) )
33 reseq1 
 |-  ( y = F -> ( y |` ( { w } X. N ) ) = ( F |` ( { w } X. N ) ) )
34 33 oveq1d 
 |-  ( y = F -> ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) = ( ( F |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) )
35 34 eqeq2d 
 |-  ( y = F -> ( ( E |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) <-> ( E |` ( { w } X. N ) ) = ( ( F |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) ) )
36 reseq1 
 |-  ( y = F -> ( y |` ( ( N \ { w } ) X. N ) ) = ( F |` ( ( N \ { w } ) X. N ) ) )
37 36 eqeq2d 
 |-  ( y = F -> ( ( E |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) <-> ( E |` ( ( N \ { w } ) X. N ) ) = ( F |` ( ( N \ { w } ) X. N ) ) ) )
38 35 37 3anbi12d 
 |-  ( y = F -> ( ( ( E |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) <-> ( ( E |` ( { w } X. N ) ) = ( ( F |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( F |` ( ( N \ { w } ) X. N ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) ) )
39 fveq2 
 |-  ( y = F -> ( D ` y ) = ( D ` F ) )
40 39 oveq1d 
 |-  ( y = F -> ( ( D ` y ) .+ ( D ` z ) ) = ( ( D ` F ) .+ ( D ` z ) ) )
41 40 eqeq2d 
 |-  ( y = F -> ( ( D ` E ) = ( ( D ` y ) .+ ( D ` z ) ) <-> ( D ` E ) = ( ( D ` F ) .+ ( D ` z ) ) ) )
42 38 41 imbi12d 
 |-  ( y = F -> ( ( ( ( E |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` E ) = ( ( D ` y ) .+ ( D ` z ) ) ) <-> ( ( ( E |` ( { w } X. N ) ) = ( ( F |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( F |` ( ( N \ { w } ) X. N ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` E ) = ( ( D ` F ) .+ ( D ` z ) ) ) ) )
43 42 2ralbidv 
 |-  ( y = F -> ( A. z e. B A. w e. N ( ( ( E |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` E ) = ( ( D ` y ) .+ ( D ` z ) ) ) <-> A. z e. B A. w e. N ( ( ( E |` ( { w } X. N ) ) = ( ( F |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( F |` ( ( N \ { w } ) X. N ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` E ) = ( ( D ` F ) .+ ( D ` z ) ) ) ) )
44 32 43 rspc2va 
 |-  ( ( ( E e. B /\ F 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 ( ( ( E |` ( { w } X. N ) ) = ( ( F |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( F |` ( ( N \ { w } ) X. N ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` E ) = ( ( D ` F ) .+ ( D ` z ) ) ) )
45 19 20 22 44 syl21anc 
 |-  ( ( ( ph /\ E e. B /\ F e. B ) /\ ( G e. B /\ H e. N ) ) -> A. z e. B A. w e. N ( ( ( E |` ( { w } X. N ) ) = ( ( F |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( F |` ( ( N \ { w } ) X. N ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` E ) = ( ( D ` F ) .+ ( D ` z ) ) ) )
46 reseq1 
 |-  ( z = G -> ( z |` ( { w } X. N ) ) = ( G |` ( { w } X. N ) ) )
47 46 oveq2d 
 |-  ( z = G -> ( ( F |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) = ( ( F |` ( { w } X. N ) ) oF .+ ( G |` ( { w } X. N ) ) ) )
48 47 eqeq2d 
 |-  ( z = G -> ( ( E |` ( { w } X. N ) ) = ( ( F |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) <-> ( E |` ( { w } X. N ) ) = ( ( F |` ( { w } X. N ) ) oF .+ ( G |` ( { w } X. N ) ) ) ) )
49 reseq1 
 |-  ( z = G -> ( z |` ( ( N \ { w } ) X. N ) ) = ( G |` ( ( N \ { w } ) X. N ) ) )
50 49 eqeq2d 
 |-  ( z = G -> ( ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) <-> ( E |` ( ( N \ { w } ) X. N ) ) = ( G |` ( ( N \ { w } ) X. N ) ) ) )
51 48 50 3anbi13d 
 |-  ( z = G -> ( ( ( E |` ( { w } X. N ) ) = ( ( F |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( F |` ( ( N \ { w } ) X. N ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) <-> ( ( E |` ( { w } X. N ) ) = ( ( F |` ( { w } X. N ) ) oF .+ ( G |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( F |` ( ( N \ { w } ) X. N ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( G |` ( ( N \ { w } ) X. N ) ) ) ) )
52 fveq2 
 |-  ( z = G -> ( D ` z ) = ( D ` G ) )
53 52 oveq2d 
 |-  ( z = G -> ( ( D ` F ) .+ ( D ` z ) ) = ( ( D ` F ) .+ ( D ` G ) ) )
54 53 eqeq2d 
 |-  ( z = G -> ( ( D ` E ) = ( ( D ` F ) .+ ( D ` z ) ) <-> ( D ` E ) = ( ( D ` F ) .+ ( D ` G ) ) ) )
55 51 54 imbi12d 
 |-  ( z = G -> ( ( ( ( E |` ( { w } X. N ) ) = ( ( F |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( F |` ( ( N \ { w } ) X. N ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` E ) = ( ( D ` F ) .+ ( D ` z ) ) ) <-> ( ( ( E |` ( { w } X. N ) ) = ( ( F |` ( { w } X. N ) ) oF .+ ( G |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( F |` ( ( N \ { w } ) X. N ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( G |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` E ) = ( ( D ` F ) .+ ( D ` G ) ) ) ) )
56 sneq 
 |-  ( w = H -> { w } = { H } )
57 56 xpeq1d 
 |-  ( w = H -> ( { w } X. N ) = ( { H } X. N ) )
58 57 reseq2d 
 |-  ( w = H -> ( E |` ( { w } X. N ) ) = ( E |` ( { H } X. N ) ) )
59 57 reseq2d 
 |-  ( w = H -> ( F |` ( { w } X. N ) ) = ( F |` ( { H } X. N ) ) )
60 57 reseq2d 
 |-  ( w = H -> ( G |` ( { w } X. N ) ) = ( G |` ( { H } X. N ) ) )
61 59 60 oveq12d 
 |-  ( w = H -> ( ( F |` ( { w } X. N ) ) oF .+ ( G |` ( { w } X. N ) ) ) = ( ( F |` ( { H } X. N ) ) oF .+ ( G |` ( { H } X. N ) ) ) )
62 58 61 eqeq12d 
 |-  ( w = H -> ( ( E |` ( { w } X. N ) ) = ( ( F |` ( { w } X. N ) ) oF .+ ( G |` ( { w } X. N ) ) ) <-> ( E |` ( { H } X. N ) ) = ( ( F |` ( { H } X. N ) ) oF .+ ( G |` ( { H } X. N ) ) ) ) )
63 56 difeq2d 
 |-  ( w = H -> ( N \ { w } ) = ( N \ { H } ) )
64 63 xpeq1d 
 |-  ( w = H -> ( ( N \ { w } ) X. N ) = ( ( N \ { H } ) X. N ) )
65 64 reseq2d 
 |-  ( w = H -> ( E |` ( ( N \ { w } ) X. N ) ) = ( E |` ( ( N \ { H } ) X. N ) ) )
66 64 reseq2d 
 |-  ( w = H -> ( F |` ( ( N \ { w } ) X. N ) ) = ( F |` ( ( N \ { H } ) X. N ) ) )
67 65 66 eqeq12d 
 |-  ( w = H -> ( ( E |` ( ( N \ { w } ) X. N ) ) = ( F |` ( ( N \ { w } ) X. N ) ) <-> ( E |` ( ( N \ { H } ) X. N ) ) = ( F |` ( ( N \ { H } ) X. N ) ) ) )
68 64 reseq2d 
 |-  ( w = H -> ( G |` ( ( N \ { w } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) )
69 65 68 eqeq12d 
 |-  ( w = H -> ( ( E |` ( ( N \ { w } ) X. N ) ) = ( G |` ( ( N \ { w } ) X. N ) ) <-> ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) )
70 62 67 69 3anbi123d 
 |-  ( w = H -> ( ( ( E |` ( { w } X. N ) ) = ( ( F |` ( { w } X. N ) ) oF .+ ( G |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( F |` ( ( N \ { w } ) X. N ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( G |` ( ( N \ { w } ) X. N ) ) ) <-> ( ( E |` ( { H } X. N ) ) = ( ( F |` ( { H } X. N ) ) oF .+ ( G |` ( { H } X. N ) ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( F |` ( ( N \ { H } ) X. N ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) ) )
71 70 imbi1d 
 |-  ( w = H -> ( ( ( ( E |` ( { w } X. N ) ) = ( ( F |` ( { w } X. N ) ) oF .+ ( G |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( F |` ( ( N \ { w } ) X. N ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( G |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` E ) = ( ( D ` F ) .+ ( D ` G ) ) ) <-> ( ( ( E |` ( { H } X. N ) ) = ( ( F |` ( { H } X. N ) ) oF .+ ( G |` ( { H } X. N ) ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( F |` ( ( N \ { H } ) X. N ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) -> ( D ` E ) = ( ( D ` F ) .+ ( D ` G ) ) ) ) )
72 55 71 rspc2va 
 |-  ( ( ( G e. B /\ H e. N ) /\ A. z e. B A. w e. N ( ( ( E |` ( { w } X. N ) ) = ( ( F |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( F |` ( ( N \ { w } ) X. N ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` E ) = ( ( D ` F ) .+ ( D ` z ) ) ) ) -> ( ( ( E |` ( { H } X. N ) ) = ( ( F |` ( { H } X. N ) ) oF .+ ( G |` ( { H } X. N ) ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( F |` ( ( N \ { H } ) X. N ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) -> ( D ` E ) = ( ( D ` F ) .+ ( D ` G ) ) ) )
73 17 18 45 72 syl21anc 
 |-  ( ( ( ph /\ E e. B /\ F e. B ) /\ ( G e. B /\ H e. N ) ) -> ( ( ( E |` ( { H } X. N ) ) = ( ( F |` ( { H } X. N ) ) oF .+ ( G |` ( { H } X. N ) ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( F |` ( ( N \ { H } ) X. N ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) -> ( D ` E ) = ( ( D ` F ) .+ ( D ` G ) ) ) )
74 73 3adantr3 
 |-  ( ( ( ph /\ E e. B /\ F e. B ) /\ ( G e. B /\ H e. N /\ ( E |` ( { H } X. N ) ) = ( ( F |` ( { H } X. N ) ) oF .+ ( G |` ( { H } X. N ) ) ) ) ) -> ( ( ( E |` ( { H } X. N ) ) = ( ( F |` ( { H } X. N ) ) oF .+ ( G |` ( { H } X. N ) ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( F |` ( ( N \ { H } ) X. N ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) -> ( D ` E ) = ( ( D ` F ) .+ ( D ` G ) ) ) )
75 74 3adant3 
 |-  ( ( ( ph /\ E e. B /\ F e. B ) /\ ( G e. B /\ H e. N /\ ( E |` ( { H } X. N ) ) = ( ( F |` ( { H } X. N ) ) oF .+ ( G |` ( { H } X. N ) ) ) ) /\ ( ( E |` ( ( N \ { H } ) X. N ) ) = ( F |` ( ( N \ { H } ) X. N ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) ) -> ( ( ( E |` ( { H } X. N ) ) = ( ( F |` ( { H } X. N ) ) oF .+ ( G |` ( { H } X. N ) ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( F |` ( ( N \ { H } ) X. N ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) -> ( D ` E ) = ( ( D ` F ) .+ ( D ` G ) ) ) )
76 14 15 16 75 mp3and 
 |-  ( ( ( ph /\ E e. B /\ F e. B ) /\ ( G e. B /\ H e. N /\ ( E |` ( { H } X. N ) ) = ( ( F |` ( { H } X. N ) ) oF .+ ( G |` ( { H } X. N ) ) ) ) /\ ( ( E |` ( ( N \ { H } ) X. N ) ) = ( F |` ( ( N \ { H } ) X. N ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) ) -> ( D ` E ) = ( ( D ` F ) .+ ( D ` G ) ) )