Metamath Proof Explorer

Theorem mdetunilem6

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 ) ) ) )
mdetunilem6.ph 
|- ( ps -> ph )
mdetunilem6.ef 
|- ( ps -> ( E e. N /\ F e. N /\ E =/= F ) )
mdetunilem6.gh 
|- ( ( ps /\ b e. N ) -> ( G e. K /\ H e. K ) )
mdetunilem6.i 
|- ( ( ps /\ a e. N /\ b e. N ) -> I e. K )
Assertion mdetunilem6 
|- ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = E , G , if ( a = F , H , I ) ) ) ) = ( ( invg ` R ) ` ( D ` ( a e. N , b e. N |-> if ( a = E , H , if ( a = F , G , I ) ) ) ) ) )

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 mdetunilem6.ph 
 |-  ( ps -> ph )
15 mdetunilem6.ef 
 |-  ( ps -> ( E e. N /\ F e. N /\ E =/= F ) )
16 mdetunilem6.gh 
 |-  ( ( ps /\ b e. N ) -> ( G e. K /\ H e. K ) )
17 mdetunilem6.i 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> I e. K )
18 15 simp1d 
 |-  ( ps -> E e. N )
19 16 simprd 
 |-  ( ( ps /\ b e. N ) -> H e. K )
20 19 3adant2 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> H e. K )
21 16 simpld 
 |-  ( ( ps /\ b e. N ) -> G e. K )
22 21 3adant2 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> G e. K )
23 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
24 14 9 23 3syl 
 |-  ( ps -> R e. Grp )
25 24 adantr 
 |-  ( ( ps /\ b e. N ) -> R e. Grp )
26 3 6 grpcl 
 |-  ( ( R e. Grp /\ H e. K /\ G e. K ) -> ( H .+ G ) e. K )
27 25 19 21 26 syl3anc 
 |-  ( ( ps /\ b e. N ) -> ( H .+ G ) e. K )
28 27 3adant2 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> ( H .+ G ) e. K )
29 28 17 ifcld 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> if ( a = F , ( H .+ G ) , I ) e. K )
30 20 22 29 3jca 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> ( H e. K /\ G e. K /\ if ( a = F , ( H .+ G ) , I ) e. K ) )
31 1 2 3 4 5 6 7 8 9 10 11 12 13 14 18 30 mdetunilem5 
 |-  ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = E , ( H .+ G ) , if ( a = F , ( H .+ G ) , I ) ) ) ) = ( ( D ` ( a e. N , b e. N |-> if ( a = E , H , if ( a = F , ( H .+ G ) , I ) ) ) ) .+ ( D ` ( a e. N , b e. N |-> if ( a = E , G , if ( a = F , ( H .+ G ) , I ) ) ) ) ) )
32 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 27 17 mdetunilem2 
 |-  ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = E , ( H .+ G ) , if ( a = F , ( H .+ G ) , I ) ) ) ) = .0. )
33 15 simp2d 
 |-  ( ps -> F e. N )
34 20 17 ifcld 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> if ( a = E , H , I ) e. K )
35 20 22 34 3jca 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> ( H e. K /\ G e. K /\ if ( a = E , H , I ) e. K ) )
36 1 2 3 4 5 6 7 8 9 10 11 12 13 14 33 35 mdetunilem5 
 |-  ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = F , ( H .+ G ) , if ( a = E , H , I ) ) ) ) = ( ( D ` ( a e. N , b e. N |-> if ( a = F , H , if ( a = E , H , I ) ) ) ) .+ ( D ` ( a e. N , b e. N |-> if ( a = F , G , if ( a = E , H , I ) ) ) ) ) )
37 15 simp3d 
 |-  ( ps -> E =/= F )
38 37 necomd 
 |-  ( ps -> F =/= E )
39 33 18 38 3jca 
 |-  ( ps -> ( F e. N /\ E e. N /\ F =/= E ) )
40 1 2 3 4 5 6 7 8 9 10 11 12 13 14 39 19 17 mdetunilem2 
 |-  ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = F , H , if ( a = E , H , I ) ) ) ) = .0. )
41 40 oveq1d 
 |-  ( ps -> ( ( D ` ( a e. N , b e. N |-> if ( a = F , H , if ( a = E , H , I ) ) ) ) .+ ( D ` ( a e. N , b e. N |-> if ( a = F , G , if ( a = E , H , I ) ) ) ) ) = ( .0. .+ ( D ` ( a e. N , b e. N |-> if ( a = F , G , if ( a = E , H , I ) ) ) ) ) )
42 37 neneqd 
 |-  ( ps -> -. E = F )
43 eqtr2 
 |-  ( ( a = E /\ a = F ) -> E = F )
44 42 43 nsyl 
 |-  ( ps -> -. ( a = E /\ a = F ) )
45 44 3ad2ant1 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> -. ( a = E /\ a = F ) )
46 ifcomnan 
 |-  ( -. ( a = E /\ a = F ) -> if ( a = E , H , if ( a = F , G , I ) ) = if ( a = F , G , if ( a = E , H , I ) ) )
47 45 46 syl 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> if ( a = E , H , if ( a = F , G , I ) ) = if ( a = F , G , if ( a = E , H , I ) ) )
48 47 mpoeq3dva 
 |-  ( ps -> ( a e. N , b e. N |-> if ( a = E , H , if ( a = F , G , I ) ) ) = ( a e. N , b e. N |-> if ( a = F , G , if ( a = E , H , I ) ) ) )
49 48 fveq2d 
 |-  ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = E , H , if ( a = F , G , I ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = F , G , if ( a = E , H , I ) ) ) ) )
50 14 10 syl 
 |-  ( ps -> D : B --> K )
51 14 8 syl 
 |-  ( ps -> N e. Fin )
52 22 17 ifcld 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> if ( a = F , G , I ) e. K )
53 20 52 ifcld 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> if ( a = E , H , if ( a = F , G , I ) ) e. K )
54 1 3 2 51 24 53 matbas2d 
 |-  ( ps -> ( a e. N , b e. N |-> if ( a = E , H , if ( a = F , G , I ) ) ) e. B )
55 50 54 ffvelcdmd 
 |-  ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = E , H , if ( a = F , G , I ) ) ) ) e. K )
56 49 55 eqeltrrd 
 |-  ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = F , G , if ( a = E , H , I ) ) ) ) e. K )
57 3 6 4 grplid 
 |-  ( ( R e. Grp /\ ( D ` ( a e. N , b e. N |-> if ( a = F , G , if ( a = E , H , I ) ) ) ) e. K ) -> ( .0. .+ ( D ` ( a e. N , b e. N |-> if ( a = F , G , if ( a = E , H , I ) ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = F , G , if ( a = E , H , I ) ) ) ) )
58 24 56 57 syl2anc 
 |-  ( ps -> ( .0. .+ ( D ` ( a e. N , b e. N |-> if ( a = F , G , if ( a = E , H , I ) ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = F , G , if ( a = E , H , I ) ) ) ) )
59 36 41 58 3eqtrd 
 |-  ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = F , ( H .+ G ) , if ( a = E , H , I ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = F , G , if ( a = E , H , I ) ) ) ) )
60 ifcomnan 
 |-  ( -. ( a = E /\ a = F ) -> if ( a = E , H , if ( a = F , ( H .+ G ) , I ) ) = if ( a = F , ( H .+ G ) , if ( a = E , H , I ) ) )
61 45 60 syl 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> if ( a = E , H , if ( a = F , ( H .+ G ) , I ) ) = if ( a = F , ( H .+ G ) , if ( a = E , H , I ) ) )
62 61 mpoeq3dva 
 |-  ( ps -> ( a e. N , b e. N |-> if ( a = E , H , if ( a = F , ( H .+ G ) , I ) ) ) = ( a e. N , b e. N |-> if ( a = F , ( H .+ G ) , if ( a = E , H , I ) ) ) )
63 62 fveq2d 
 |-  ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = E , H , if ( a = F , ( H .+ G ) , I ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = F , ( H .+ G ) , if ( a = E , H , I ) ) ) ) )
64 59 63 49 3eqtr4d 
 |-  ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = E , H , if ( a = F , ( H .+ G ) , I ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = E , H , if ( a = F , G , I ) ) ) ) )
65 22 17 ifcld 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> if ( a = E , G , I ) e. K )
66 20 22 65 3jca 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> ( H e. K /\ G e. K /\ if ( a = E , G , I ) e. K ) )
67 1 2 3 4 5 6 7 8 9 10 11 12 13 14 33 66 mdetunilem5 
 |-  ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = F , ( H .+ G ) , if ( a = E , G , I ) ) ) ) = ( ( D ` ( a e. N , b e. N |-> if ( a = F , H , if ( a = E , G , I ) ) ) ) .+ ( D ` ( a e. N , b e. N |-> if ( a = F , G , if ( a = E , G , I ) ) ) ) ) )
68 1 2 3 4 5 6 7 8 9 10 11 12 13 14 39 21 17 mdetunilem2 
 |-  ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = F , G , if ( a = E , G , I ) ) ) ) = .0. )
69 68 oveq2d 
 |-  ( ps -> ( ( D ` ( a e. N , b e. N |-> if ( a = F , H , if ( a = E , G , I ) ) ) ) .+ ( D ` ( a e. N , b e. N |-> if ( a = F , G , if ( a = E , G , I ) ) ) ) ) = ( ( D ` ( a e. N , b e. N |-> if ( a = F , H , if ( a = E , G , I ) ) ) ) .+ .0. ) )
70 ifcomnan 
 |-  ( -. ( a = E /\ a = F ) -> if ( a = E , G , if ( a = F , H , I ) ) = if ( a = F , H , if ( a = E , G , I ) ) )
71 45 70 syl 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> if ( a = E , G , if ( a = F , H , I ) ) = if ( a = F , H , if ( a = E , G , I ) ) )
72 71 mpoeq3dva 
 |-  ( ps -> ( a e. N , b e. N |-> if ( a = E , G , if ( a = F , H , I ) ) ) = ( a e. N , b e. N |-> if ( a = F , H , if ( a = E , G , I ) ) ) )
73 72 fveq2d 
 |-  ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = E , G , if ( a = F , H , I ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = F , H , if ( a = E , G , I ) ) ) ) )
74 20 17 ifcld 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> if ( a = F , H , I ) e. K )
75 22 74 ifcld 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> if ( a = E , G , if ( a = F , H , I ) ) e. K )
76 1 3 2 51 24 75 matbas2d 
 |-  ( ps -> ( a e. N , b e. N |-> if ( a = E , G , if ( a = F , H , I ) ) ) e. B )
77 50 76 ffvelcdmd 
 |-  ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = E , G , if ( a = F , H , I ) ) ) ) e. K )
78 73 77 eqeltrrd 
 |-  ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = F , H , if ( a = E , G , I ) ) ) ) e. K )
79 3 6 4 grprid 
 |-  ( ( R e. Grp /\ ( D ` ( a e. N , b e. N |-> if ( a = F , H , if ( a = E , G , I ) ) ) ) e. K ) -> ( ( D ` ( a e. N , b e. N |-> if ( a = F , H , if ( a = E , G , I ) ) ) ) .+ .0. ) = ( D ` ( a e. N , b e. N |-> if ( a = F , H , if ( a = E , G , I ) ) ) ) )
80 24 78 79 syl2anc 
 |-  ( ps -> ( ( D ` ( a e. N , b e. N |-> if ( a = F , H , if ( a = E , G , I ) ) ) ) .+ .0. ) = ( D ` ( a e. N , b e. N |-> if ( a = F , H , if ( a = E , G , I ) ) ) ) )
81 67 69 80 3eqtrd 
 |-  ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = F , ( H .+ G ) , if ( a = E , G , I ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = F , H , if ( a = E , G , I ) ) ) ) )
82 ifcomnan 
 |-  ( -. ( a = E /\ a = F ) -> if ( a = E , G , if ( a = F , ( H .+ G ) , I ) ) = if ( a = F , ( H .+ G ) , if ( a = E , G , I ) ) )
83 45 82 syl 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> if ( a = E , G , if ( a = F , ( H .+ G ) , I ) ) = if ( a = F , ( H .+ G ) , if ( a = E , G , I ) ) )
84 83 mpoeq3dva 
 |-  ( ps -> ( a e. N , b e. N |-> if ( a = E , G , if ( a = F , ( H .+ G ) , I ) ) ) = ( a e. N , b e. N |-> if ( a = F , ( H .+ G ) , if ( a = E , G , I ) ) ) )
85 84 fveq2d 
 |-  ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = E , G , if ( a = F , ( H .+ G ) , I ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = F , ( H .+ G ) , if ( a = E , G , I ) ) ) ) )
86 81 85 73 3eqtr4d 
 |-  ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = E , G , if ( a = F , ( H .+ G ) , I ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = E , G , if ( a = F , H , I ) ) ) ) )
87 64 86 oveq12d 
 |-  ( ps -> ( ( D ` ( a e. N , b e. N |-> if ( a = E , H , if ( a = F , ( H .+ G ) , I ) ) ) ) .+ ( D ` ( a e. N , b e. N |-> if ( a = E , G , if ( a = F , ( H .+ G ) , I ) ) ) ) ) = ( ( D ` ( a e. N , b e. N |-> if ( a = E , H , if ( a = F , G , I ) ) ) ) .+ ( D ` ( a e. N , b e. N |-> if ( a = E , G , if ( a = F , H , I ) ) ) ) ) )
88 31 32 87 3eqtr3rd 
 |-  ( ps -> ( ( D ` ( a e. N , b e. N |-> if ( a = E , H , if ( a = F , G , I ) ) ) ) .+ ( D ` ( a e. N , b e. N |-> if ( a = E , G , if ( a = F , H , I ) ) ) ) ) = .0. )
89 eqid 
 |-  ( invg ` R ) = ( invg ` R )
90 3 6 4 89 grpinvid1 
 |-  ( ( R e. Grp /\ ( D ` ( a e. N , b e. N |-> if ( a = E , H , if ( a = F , G , I ) ) ) ) e. K /\ ( D ` ( a e. N , b e. N |-> if ( a = E , G , if ( a = F , H , I ) ) ) ) e. K ) -> ( ( ( invg ` R ) ` ( D ` ( a e. N , b e. N |-> if ( a = E , H , if ( a = F , G , I ) ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = E , G , if ( a = F , H , I ) ) ) ) <-> ( ( D ` ( a e. N , b e. N |-> if ( a = E , H , if ( a = F , G , I ) ) ) ) .+ ( D ` ( a e. N , b e. N |-> if ( a = E , G , if ( a = F , H , I ) ) ) ) ) = .0. ) )
91 24 55 77 90 syl3anc 
 |-  ( ps -> ( ( ( invg ` R ) ` ( D ` ( a e. N , b e. N |-> if ( a = E , H , if ( a = F , G , I ) ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = E , G , if ( a = F , H , I ) ) ) ) <-> ( ( D ` ( a e. N , b e. N |-> if ( a = E , H , if ( a = F , G , I ) ) ) ) .+ ( D ` ( a e. N , b e. N |-> if ( a = E , G , if ( a = F , H , I ) ) ) ) ) = .0. ) )
92 88 91 mpbird 
 |-  ( ps -> ( ( invg ` R ) ` ( D ` ( a e. N , b e. N |-> if ( a = E , H , if ( a = F , G , I ) ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = E , G , if ( a = F , H , I ) ) ) ) )
93 92 eqcomd 
 |-  ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = E , G , if ( a = F , H , I ) ) ) ) = ( ( invg ` R ) ` ( D ` ( a e. N , b e. N |-> if ( a = E , H , if ( a = F , G , I ) ) ) ) ) )