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 ) ) ) |