Metamath Proof Explorer

Theorem mdetunilem1

Description: Lemma for mdetuni . (Contributed by SO, 14-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 mdetunilem1 
|- ( ( ( ph /\ E e. B /\ A. w e. N ( F E w ) = ( G E w ) ) /\ ( F e. N /\ G e. N /\ F =/= G ) ) -> ( D ` E ) = .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 simpr3 
 |-  ( ( ( ph /\ E e. B /\ A. w e. N ( F E w ) = ( G E w ) ) /\ ( F e. N /\ G e. N /\ F =/= G ) ) -> F =/= G )
15 simpl3 
 |-  ( ( ( ph /\ E e. B /\ A. w e. N ( F E w ) = ( G E w ) ) /\ ( F e. N /\ G e. N /\ F =/= G ) ) -> A. w e. N ( F E w ) = ( G E w ) )
16 neeq2 
 |-  ( z = G -> ( F =/= z <-> F =/= G ) )
17 oveq1 
 |-  ( z = G -> ( z E w ) = ( G E w ) )
18 17 eqeq2d 
 |-  ( z = G -> ( ( F E w ) = ( z E w ) <-> ( F E w ) = ( G E w ) ) )
19 18 ralbidv 
 |-  ( z = G -> ( A. w e. N ( F E w ) = ( z E w ) <-> A. w e. N ( F E w ) = ( G E w ) ) )
20 16 19 anbi12d 
 |-  ( z = G -> ( ( F =/= z /\ A. w e. N ( F E w ) = ( z E w ) ) <-> ( F =/= G /\ A. w e. N ( F E w ) = ( G E w ) ) ) )
21 20 imbi1d 
 |-  ( z = G -> ( ( ( F =/= z /\ A. w e. N ( F E w ) = ( z E w ) ) -> ( D ` E ) = .0. ) <-> ( ( F =/= G /\ A. w e. N ( F E w ) = ( G E w ) ) -> ( D ` E ) = .0. ) ) )
22 simpl2 
 |-  ( ( ( ph /\ E e. B /\ A. w e. N ( F E w ) = ( G E w ) ) /\ ( F e. N /\ G e. N /\ F =/= G ) ) -> E e. B )
23 simpr1 
 |-  ( ( ( ph /\ E e. B /\ A. w e. N ( F E w ) = ( G E w ) ) /\ ( F e. N /\ G e. N /\ F =/= G ) ) -> F e. N )
24 simpl1 
 |-  ( ( ( ph /\ E e. B /\ A. w e. N ( F E w ) = ( G E w ) ) /\ ( F e. N /\ G e. N /\ F =/= G ) ) -> ph )
25 24 11 syl 
 |-  ( ( ( ph /\ E e. B /\ A. w e. N ( F E w ) = ( G E w ) ) /\ ( F e. N /\ G e. N /\ F =/= G ) ) -> 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. ) )
26 oveq 
 |-  ( x = E -> ( y x w ) = ( y E w ) )
27 oveq 
 |-  ( x = E -> ( z x w ) = ( z E w ) )
28 26 27 eqeq12d 
 |-  ( x = E -> ( ( y x w ) = ( z x w ) <-> ( y E w ) = ( z E w ) ) )
29 28 ralbidv 
 |-  ( x = E -> ( A. w e. N ( y x w ) = ( z x w ) <-> A. w e. N ( y E w ) = ( z E w ) ) )
30 29 anbi2d 
 |-  ( x = E -> ( ( y =/= z /\ A. w e. N ( y x w ) = ( z x w ) ) <-> ( y =/= z /\ A. w e. N ( y E w ) = ( z E w ) ) ) )
31 fveqeq2 
 |-  ( x = E -> ( ( D ` x ) = .0. <-> ( D ` E ) = .0. ) )
32 30 31 imbi12d 
 |-  ( x = E -> ( ( ( y =/= z /\ A. w e. N ( y x w ) = ( z x w ) ) -> ( D ` x ) = .0. ) <-> ( ( y =/= z /\ A. w e. N ( y E w ) = ( z E w ) ) -> ( D ` E ) = .0. ) ) )
33 32 ralbidv 
 |-  ( x = E -> ( A. z e. N ( ( y =/= z /\ A. w e. N ( y x w ) = ( z x w ) ) -> ( D ` x ) = .0. ) <-> A. z e. N ( ( y =/= z /\ A. w e. N ( y E w ) = ( z E w ) ) -> ( D ` E ) = .0. ) ) )
34 neeq1 
 |-  ( y = F -> ( y =/= z <-> F =/= z ) )
35 oveq1 
 |-  ( y = F -> ( y E w ) = ( F E w ) )
36 35 eqeq1d 
 |-  ( y = F -> ( ( y E w ) = ( z E w ) <-> ( F E w ) = ( z E w ) ) )
37 36 ralbidv 
 |-  ( y = F -> ( A. w e. N ( y E w ) = ( z E w ) <-> A. w e. N ( F E w ) = ( z E w ) ) )
38 34 37 anbi12d 
 |-  ( y = F -> ( ( y =/= z /\ A. w e. N ( y E w ) = ( z E w ) ) <-> ( F =/= z /\ A. w e. N ( F E w ) = ( z E w ) ) ) )
39 38 imbi1d 
 |-  ( y = F -> ( ( ( y =/= z /\ A. w e. N ( y E w ) = ( z E w ) ) -> ( D ` E ) = .0. ) <-> ( ( F =/= z /\ A. w e. N ( F E w ) = ( z E w ) ) -> ( D ` E ) = .0. ) ) )
40 39 ralbidv 
 |-  ( y = F -> ( A. z e. N ( ( y =/= z /\ A. w e. N ( y E w ) = ( z E w ) ) -> ( D ` E ) = .0. ) <-> A. z e. N ( ( F =/= z /\ A. w e. N ( F E w ) = ( z E w ) ) -> ( D ` E ) = .0. ) ) )
41 33 40 rspc2va 
 |-  ( ( ( E e. B /\ F e. N ) /\ 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. ) ) -> A. z e. N ( ( F =/= z /\ A. w e. N ( F E w ) = ( z E w ) ) -> ( D ` E ) = .0. ) )
42 22 23 25 41 syl21anc 
 |-  ( ( ( ph /\ E e. B /\ A. w e. N ( F E w ) = ( G E w ) ) /\ ( F e. N /\ G e. N /\ F =/= G ) ) -> A. z e. N ( ( F =/= z /\ A. w e. N ( F E w ) = ( z E w ) ) -> ( D ` E ) = .0. ) )
43 simpr2 
 |-  ( ( ( ph /\ E e. B /\ A. w e. N ( F E w ) = ( G E w ) ) /\ ( F e. N /\ G e. N /\ F =/= G ) ) -> G e. N )
44 21 42 43 rspcdva 
 |-  ( ( ( ph /\ E e. B /\ A. w e. N ( F E w ) = ( G E w ) ) /\ ( F e. N /\ G e. N /\ F =/= G ) ) -> ( ( F =/= G /\ A. w e. N ( F E w ) = ( G E w ) ) -> ( D ` E ) = .0. ) )
45 14 15 44 mp2and 
 |-  ( ( ( ph /\ E e. B /\ A. w e. N ( F E w ) = ( G E w ) ) /\ ( F e. N /\ G e. N /\ F =/= G ) ) -> ( D ` E ) = .0. )