Metamath Proof Explorer

Theorem mdetunilem4

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 mdetunilem4 
|- ( ( ph /\ ( E e. B /\ F e. K /\ G e. B ) /\ ( H e. N /\ ( E |` ( { H } X. N ) ) = ( ( ( { H } X. N ) X. { F } ) oF .x. ( G |` ( { H } X. N ) ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) ) -> ( D ` E ) = ( F .x. ( 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 simp32 
 |-  ( ( ph /\ ( E e. B /\ F e. K /\ G e. B ) /\ ( H e. N /\ ( E |` ( { H } X. N ) ) = ( ( ( { H } X. N ) X. { F } ) oF .x. ( G |` ( { H } X. N ) ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) ) -> ( E |` ( { H } X. N ) ) = ( ( ( { H } X. N ) X. { F } ) oF .x. ( G |` ( { H } X. N ) ) ) )
15 simp33 
 |-  ( ( ph /\ ( E e. B /\ F e. K /\ G e. B ) /\ ( H e. N /\ ( E |` ( { H } X. N ) ) = ( ( ( { H } X. N ) X. { F } ) oF .x. ( G |` ( { H } X. N ) ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) ) -> ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) )
16 simp1 
 |-  ( ( H e. N /\ ( E |` ( { H } X. N ) ) = ( ( ( { H } X. N ) X. { F } ) oF .x. ( G |` ( { H } X. N ) ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) -> H e. N )
17 simp23 
 |-  ( ( ph /\ ( E e. B /\ F e. K /\ G e. B ) /\ H e. N ) -> G e. B )
18 simp3 
 |-  ( ( ph /\ ( E e. B /\ F e. K /\ G e. B ) /\ H e. N ) -> H e. N )
19 simp21 
 |-  ( ( ph /\ ( E e. B /\ F e. K /\ G e. B ) /\ H e. N ) -> E e. B )
20 simp22 
 |-  ( ( ph /\ ( E e. B /\ F e. K /\ G e. B ) /\ H e. N ) -> F e. K )
21 13 3ad2ant1 
 |-  ( ( ph /\ ( E e. B /\ F e. K /\ G e. B ) /\ H e. N ) -> 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 ) ) ) )
22 reseq1 
 |-  ( x = E -> ( x |` ( { w } X. N ) ) = ( E |` ( { w } X. N ) ) )
23 22 eqeq1d 
 |-  ( x = E -> ( ( x |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) <-> ( E |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) ) )
24 reseq1 
 |-  ( x = E -> ( x |` ( ( N \ { w } ) X. N ) ) = ( E |` ( ( N \ { w } ) X. N ) ) )
25 24 eqeq1d 
 |-  ( x = E -> ( ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) <-> ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) )
26 23 25 anbi12d 
 |-  ( x = 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 |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) ) )
27 fveqeq2 
 |-  ( x = E -> ( ( D ` x ) = ( y .x. ( D ` z ) ) <-> ( D ` E ) = ( y .x. ( D ` z ) ) ) )
28 26 27 imbi12d 
 |-  ( x = 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 |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` E ) = ( y .x. ( D ` z ) ) ) ) )
29 28 2ralbidv 
 |-  ( x = 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 |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` E ) = ( y .x. ( D ` z ) ) ) ) )
30 sneq 
 |-  ( y = F -> { y } = { F } )
31 30 xpeq2d 
 |-  ( y = F -> ( ( { w } X. N ) X. { y } ) = ( ( { w } X. N ) X. { F } ) )
32 31 oveq1d 
 |-  ( y = F -> ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) = ( ( ( { w } X. N ) X. { F } ) oF .x. ( z |` ( { w } X. N ) ) ) )
33 32 eqeq2d 
 |-  ( y = F -> ( ( E |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) <-> ( E |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { F } ) oF .x. ( z |` ( { w } X. N ) ) ) ) )
34 33 anbi1d 
 |-  ( y = F -> ( ( ( E |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) <-> ( ( E |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { F } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) ) )
35 oveq1 
 |-  ( y = F -> ( y .x. ( D ` z ) ) = ( F .x. ( D ` z ) ) )
36 35 eqeq2d 
 |-  ( y = F -> ( ( D ` E ) = ( y .x. ( D ` z ) ) <-> ( D ` E ) = ( F .x. ( D ` z ) ) ) )
37 34 36 imbi12d 
 |-  ( y = F -> ( ( ( ( E |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` E ) = ( y .x. ( D ` z ) ) ) <-> ( ( ( E |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { F } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` E ) = ( F .x. ( D ` z ) ) ) ) )
38 37 2ralbidv 
 |-  ( y = F -> ( A. z e. B A. w e. N ( ( ( E |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` E ) = ( y .x. ( D ` z ) ) ) <-> A. z e. B A. w e. N ( ( ( E |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { F } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` E ) = ( F .x. ( D ` z ) ) ) ) )
39 29 38 rspc2va 
 |-  ( ( ( E e. B /\ F 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 |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { F } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` E ) = ( F .x. ( D ` z ) ) ) )
40 19 20 21 39 syl21anc 
 |-  ( ( ph /\ ( E e. B /\ F e. K /\ G e. B ) /\ H e. N ) -> A. z e. B A. w e. N ( ( ( E |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { F } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` E ) = ( F .x. ( D ` z ) ) ) )
41 reseq1 
 |-  ( z = G -> ( z |` ( { w } X. N ) ) = ( G |` ( { w } X. N ) ) )
42 41 oveq2d 
 |-  ( z = G -> ( ( ( { w } X. N ) X. { F } ) oF .x. ( z |` ( { w } X. N ) ) ) = ( ( ( { w } X. N ) X. { F } ) oF .x. ( G |` ( { w } X. N ) ) ) )
43 42 eqeq2d 
 |-  ( z = G -> ( ( E |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { F } ) oF .x. ( z |` ( { w } X. N ) ) ) <-> ( E |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { F } ) oF .x. ( G |` ( { w } X. N ) ) ) ) )
44 reseq1 
 |-  ( z = G -> ( z |` ( ( N \ { w } ) X. N ) ) = ( G |` ( ( N \ { w } ) X. N ) ) )
45 44 eqeq2d 
 |-  ( z = G -> ( ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) <-> ( E |` ( ( N \ { w } ) X. N ) ) = ( G |` ( ( N \ { w } ) X. N ) ) ) )
46 43 45 anbi12d 
 |-  ( z = G -> ( ( ( E |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { F } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) <-> ( ( E |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { F } ) oF .x. ( G |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( G |` ( ( N \ { w } ) X. N ) ) ) ) )
47 fveq2 
 |-  ( z = G -> ( D ` z ) = ( D ` G ) )
48 47 oveq2d 
 |-  ( z = G -> ( F .x. ( D ` z ) ) = ( F .x. ( D ` G ) ) )
49 48 eqeq2d 
 |-  ( z = G -> ( ( D ` E ) = ( F .x. ( D ` z ) ) <-> ( D ` E ) = ( F .x. ( D ` G ) ) ) )
50 46 49 imbi12d 
 |-  ( z = G -> ( ( ( ( E |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { F } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` E ) = ( F .x. ( D ` z ) ) ) <-> ( ( ( E |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { F } ) oF .x. ( G |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( G |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` E ) = ( F .x. ( D ` G ) ) ) ) )
51 sneq 
 |-  ( w = H -> { w } = { H } )
52 51 xpeq1d 
 |-  ( w = H -> ( { w } X. N ) = ( { H } X. N ) )
53 52 reseq2d 
 |-  ( w = H -> ( E |` ( { w } X. N ) ) = ( E |` ( { H } X. N ) ) )
54 52 xpeq1d 
 |-  ( w = H -> ( ( { w } X. N ) X. { F } ) = ( ( { H } X. N ) X. { F } ) )
55 52 reseq2d 
 |-  ( w = H -> ( G |` ( { w } X. N ) ) = ( G |` ( { H } X. N ) ) )
56 54 55 oveq12d 
 |-  ( w = H -> ( ( ( { w } X. N ) X. { F } ) oF .x. ( G |` ( { w } X. N ) ) ) = ( ( ( { H } X. N ) X. { F } ) oF .x. ( G |` ( { H } X. N ) ) ) )
57 53 56 eqeq12d 
 |-  ( w = H -> ( ( E |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { F } ) oF .x. ( G |` ( { w } X. N ) ) ) <-> ( E |` ( { H } X. N ) ) = ( ( ( { H } X. N ) X. { F } ) oF .x. ( G |` ( { H } X. N ) ) ) ) )
58 51 difeq2d 
 |-  ( w = H -> ( N \ { w } ) = ( N \ { H } ) )
59 58 xpeq1d 
 |-  ( w = H -> ( ( N \ { w } ) X. N ) = ( ( N \ { H } ) X. N ) )
60 59 reseq2d 
 |-  ( w = H -> ( E |` ( ( N \ { w } ) X. N ) ) = ( E |` ( ( N \ { H } ) X. N ) ) )
61 59 reseq2d 
 |-  ( w = H -> ( G |` ( ( N \ { w } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) )
62 60 61 eqeq12d 
 |-  ( w = H -> ( ( E |` ( ( N \ { w } ) X. N ) ) = ( G |` ( ( N \ { w } ) X. N ) ) <-> ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) )
63 57 62 anbi12d 
 |-  ( w = H -> ( ( ( E |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { F } ) oF .x. ( G |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( G |` ( ( N \ { w } ) X. N ) ) ) <-> ( ( E |` ( { H } X. N ) ) = ( ( ( { H } X. N ) X. { F } ) oF .x. ( G |` ( { H } X. N ) ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) ) )
64 63 imbi1d 
 |-  ( w = H -> ( ( ( ( E |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { F } ) oF .x. ( G |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( G |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` E ) = ( F .x. ( D ` G ) ) ) <-> ( ( ( E |` ( { H } X. N ) ) = ( ( ( { H } X. N ) X. { F } ) oF .x. ( G |` ( { H } X. N ) ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) -> ( D ` E ) = ( F .x. ( D ` G ) ) ) ) )
65 50 64 rspc2va 
 |-  ( ( ( G e. B /\ H e. N ) /\ A. z e. B A. w e. N ( ( ( E |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { F } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( E |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` E ) = ( F .x. ( D ` z ) ) ) ) -> ( ( ( E |` ( { H } X. N ) ) = ( ( ( { H } X. N ) X. { F } ) oF .x. ( G |` ( { H } X. N ) ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) -> ( D ` E ) = ( F .x. ( D ` G ) ) ) )
66 17 18 40 65 syl21anc 
 |-  ( ( ph /\ ( E e. B /\ F e. K /\ G e. B ) /\ H e. N ) -> ( ( ( E |` ( { H } X. N ) ) = ( ( ( { H } X. N ) X. { F } ) oF .x. ( G |` ( { H } X. N ) ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) -> ( D ` E ) = ( F .x. ( D ` G ) ) ) )
67 16 66 syl3an3 
 |-  ( ( ph /\ ( E e. B /\ F e. K /\ G e. B ) /\ ( H e. N /\ ( E |` ( { H } X. N ) ) = ( ( ( { H } X. N ) X. { F } ) oF .x. ( G |` ( { H } X. N ) ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) ) -> ( ( ( E |` ( { H } X. N ) ) = ( ( ( { H } X. N ) X. { F } ) oF .x. ( G |` ( { H } X. N ) ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) -> ( D ` E ) = ( F .x. ( D ` G ) ) ) )
68 14 15 67 mp2and 
 |-  ( ( ph /\ ( E e. B /\ F e. K /\ G e. B ) /\ ( H e. N /\ ( E |` ( { H } X. N ) ) = ( ( ( { H } X. N ) X. { F } ) oF .x. ( G |` ( { H } X. N ) ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) ) -> ( D ` E ) = ( F .x. ( D ` G ) ) )