Metamath Proof Explorer

Theorem mdetunilem2

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 ) ) ) )
mdetunilem2.ph 
|- ( ps -> ph )
mdetunilem2.eg 
|- ( ps -> ( E e. N /\ G e. N /\ E =/= G ) )
mdetunilem2.f 
|- ( ( ps /\ b e. N ) -> F e. K )
mdetunilem2.h 
|- ( ( ps /\ a e. N /\ b e. N ) -> H e. K )
Assertion mdetunilem2 
|- ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = E , F , if ( a = G , F , H ) ) ) ) = .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 mdetunilem2.ph 
 |-  ( ps -> ph )
15 mdetunilem2.eg 
 |-  ( ps -> ( E e. N /\ G e. N /\ E =/= G ) )
16 mdetunilem2.f 
 |-  ( ( ps /\ b e. N ) -> F e. K )
17 mdetunilem2.h 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> H e. K )
18 14 8 syl 
 |-  ( ps -> N e. Fin )
19 14 9 syl 
 |-  ( ps -> R e. Ring )
20 16 3adant2 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> F e. K )
21 20 17 ifcld 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> if ( a = G , F , H ) e. K )
22 20 21 ifcld 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> if ( a = E , F , if ( a = G , F , H ) ) e. K )
23 1 3 2 18 19 22 matbas2d 
 |-  ( ps -> ( a e. N , b e. N |-> if ( a = E , F , if ( a = G , F , H ) ) ) e. B )
24 eqidd 
 |-  ( ( ps /\ w e. N ) -> ( a e. N , b e. N |-> if ( a = E , F , if ( a = G , F , H ) ) ) = ( a e. N , b e. N |-> if ( a = E , F , if ( a = G , F , H ) ) ) )
25 iftrue 
 |-  ( a = E -> if ( a = E , F , if ( a = G , F , H ) ) = F )
26 csbeq1a 
 |-  ( b = w -> F = [_ w / b ]_ F )
27 25 26 sylan9eq 
 |-  ( ( a = E /\ b = w ) -> if ( a = E , F , if ( a = G , F , H ) ) = [_ w / b ]_ F )
28 27 adantl 
 |-  ( ( ( ps /\ w e. N ) /\ ( a = E /\ b = w ) ) -> if ( a = E , F , if ( a = G , F , H ) ) = [_ w / b ]_ F )
29 eqidd 
 |-  ( ( ( ps /\ w e. N ) /\ a = E ) -> N = N )
30 15 simp1d 
 |-  ( ps -> E e. N )
31 30 adantr 
 |-  ( ( ps /\ w e. N ) -> E e. N )
32 simpr 
 |-  ( ( ps /\ w e. N ) -> w e. N )
33 nfv 
 |-  F/ b ( ps /\ w e. N )
34 nfcsb1v 
 |-  F/_ b [_ w / b ]_ F
35 34 nfel1 
 |-  F/ b [_ w / b ]_ F e. K
36 33 35 nfim 
 |-  F/ b ( ( ps /\ w e. N ) -> [_ w / b ]_ F e. K )
37 eleq1w 
 |-  ( b = w -> ( b e. N <-> w e. N ) )
38 37 anbi2d 
 |-  ( b = w -> ( ( ps /\ b e. N ) <-> ( ps /\ w e. N ) ) )
39 26 eleq1d 
 |-  ( b = w -> ( F e. K <-> [_ w / b ]_ F e. K ) )
40 38 39 imbi12d 
 |-  ( b = w -> ( ( ( ps /\ b e. N ) -> F e. K ) <-> ( ( ps /\ w e. N ) -> [_ w / b ]_ F e. K ) ) )
41 36 40 16 chvarfv 
 |-  ( ( ps /\ w e. N ) -> [_ w / b ]_ F e. K )
42 nfv 
 |-  F/ a ( ps /\ w e. N )
43 nfcv 
 |-  F/_ b E
44 nfcv 
 |-  F/_ a w
45 nfcv 
 |-  F/_ a [_ w / b ]_ F
46 24 28 29 31 32 41 42 33 43 44 45 34 ovmpodxf 
 |-  ( ( ps /\ w e. N ) -> ( E ( a e. N , b e. N |-> if ( a = E , F , if ( a = G , F , H ) ) ) w ) = [_ w / b ]_ F )
47 15 simp3d 
 |-  ( ps -> E =/= G )
48 47 adantr 
 |-  ( ( ps /\ w e. N ) -> E =/= G )
49 neeq2 
 |-  ( a = G -> ( E =/= a <-> E =/= G ) )
50 48 49 syl5ibrcom 
 |-  ( ( ps /\ w e. N ) -> ( a = G -> E =/= a ) )
51 50 imp 
 |-  ( ( ( ps /\ w e. N ) /\ a = G ) -> E =/= a )
52 51 necomd 
 |-  ( ( ( ps /\ w e. N ) /\ a = G ) -> a =/= E )
53 52 neneqd 
 |-  ( ( ( ps /\ w e. N ) /\ a = G ) -> -. a = E )
54 53 adantrr 
 |-  ( ( ( ps /\ w e. N ) /\ ( a = G /\ b = w ) ) -> -. a = E )
55 54 iffalsed 
 |-  ( ( ( ps /\ w e. N ) /\ ( a = G /\ b = w ) ) -> if ( a = E , F , if ( a = G , F , H ) ) = if ( a = G , F , H ) )
56 iftrue 
 |-  ( a = G -> if ( a = G , F , H ) = F )
57 56 26 sylan9eq 
 |-  ( ( a = G /\ b = w ) -> if ( a = G , F , H ) = [_ w / b ]_ F )
58 57 adantl 
 |-  ( ( ( ps /\ w e. N ) /\ ( a = G /\ b = w ) ) -> if ( a = G , F , H ) = [_ w / b ]_ F )
59 55 58 eqtrd 
 |-  ( ( ( ps /\ w e. N ) /\ ( a = G /\ b = w ) ) -> if ( a = E , F , if ( a = G , F , H ) ) = [_ w / b ]_ F )
60 eqidd 
 |-  ( ( ( ps /\ w e. N ) /\ a = G ) -> N = N )
61 15 simp2d 
 |-  ( ps -> G e. N )
62 61 adantr 
 |-  ( ( ps /\ w e. N ) -> G e. N )
63 nfcv 
 |-  F/_ b G
64 24 59 60 62 32 41 42 33 63 44 45 34 ovmpodxf 
 |-  ( ( ps /\ w e. N ) -> ( G ( a e. N , b e. N |-> if ( a = E , F , if ( a = G , F , H ) ) ) w ) = [_ w / b ]_ F )
65 46 64 eqtr4d 
 |-  ( ( ps /\ w e. N ) -> ( E ( a e. N , b e. N |-> if ( a = E , F , if ( a = G , F , H ) ) ) w ) = ( G ( a e. N , b e. N |-> if ( a = E , F , if ( a = G , F , H ) ) ) w ) )
66 65 ralrimiva 
 |-  ( ps -> A. w e. N ( E ( a e. N , b e. N |-> if ( a = E , F , if ( a = G , F , H ) ) ) w ) = ( G ( a e. N , b e. N |-> if ( a = E , F , if ( a = G , F , H ) ) ) w ) )
67 1 2 3 4 5 6 7 8 9 10 11 12 13 mdetunilem1 
 |-  ( ( ( ph /\ ( a e. N , b e. N |-> if ( a = E , F , if ( a = G , F , H ) ) ) e. B /\ A. w e. N ( E ( a e. N , b e. N |-> if ( a = E , F , if ( a = G , F , H ) ) ) w ) = ( G ( a e. N , b e. N |-> if ( a = E , F , if ( a = G , F , H ) ) ) w ) ) /\ ( E e. N /\ G e. N /\ E =/= G ) ) -> ( D ` ( a e. N , b e. N |-> if ( a = E , F , if ( a = G , F , H ) ) ) ) = .0. )
68 14 23 66 15 67 syl31anc 
 |-  ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = E , F , if ( a = G , F , H ) ) ) ) = .0. )