Metamath Proof Explorer

Theorem mdetunilem5

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 ) ) ) )
mdetunilem5.ph 
|- ( ps -> ph )
mdetunilem5.e 
|- ( ps -> E e. N )
mdetunilem5.fgh 
|- ( ( ps /\ a e. N /\ b e. N ) -> ( F e. K /\ G e. K /\ H e. K ) )
Assertion mdetunilem5 
|- ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = E , ( F .+ G ) , H ) ) ) = ( ( D ` ( a e. N , b e. N |-> if ( a = E , F , H ) ) ) .+ ( D ` ( a e. N , b e. N |-> if ( a = E , G , H ) ) ) ) )

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 mdetunilem5.ph 
 |-  ( ps -> ph )
15 mdetunilem5.e 
 |-  ( ps -> E e. N )
16 mdetunilem5.fgh 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> ( F e. K /\ G e. K /\ H e. K ) )
17 14 8 syl 
 |-  ( ps -> N e. Fin )
18 14 9 syl 
 |-  ( ps -> R e. Ring )
19 18 3ad2ant1 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> R e. Ring )
20 16 simp1d 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> F e. K )
21 16 simp2d 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> G e. K )
22 3 6 ringacl 
 |-  ( ( R e. Ring /\ F e. K /\ G e. K ) -> ( F .+ G ) e. K )
23 19 20 21 22 syl3anc 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> ( F .+ G ) e. K )
24 16 simp3d 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> H e. K )
25 23 24 ifcld 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> if ( a = E , ( F .+ G ) , H ) e. K )
26 1 3 2 17 18 25 matbas2d 
 |-  ( ps -> ( a e. N , b e. N |-> if ( a = E , ( F .+ G ) , H ) ) e. B )
27 20 24 ifcld 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> if ( a = E , F , H ) e. K )
28 1 3 2 17 18 27 matbas2d 
 |-  ( ps -> ( a e. N , b e. N |-> if ( a = E , F , H ) ) e. B )
29 21 24 ifcld 
 |-  ( ( ps /\ a e. N /\ b e. N ) -> if ( a = E , G , H ) e. K )
30 1 3 2 17 18 29 matbas2d 
 |-  ( ps -> ( a e. N , b e. N |-> if ( a = E , G , H ) ) e. B )
31 snex 
 |-  { E } e. _V
32 31 a1i 
 |-  ( ps -> { E } e. _V )
33 15 snssd 
 |-  ( ps -> { E } C_ N )
34 33 3ad2ant1 
 |-  ( ( ps /\ a e. { E } /\ b e. N ) -> { E } C_ N )
35 simp2 
 |-  ( ( ps /\ a e. { E } /\ b e. N ) -> a e. { E } )
36 34 35 sseldd 
 |-  ( ( ps /\ a e. { E } /\ b e. N ) -> a e. N )
37 36 20 syld3an2 
 |-  ( ( ps /\ a e. { E } /\ b e. N ) -> F e. K )
38 36 21 syld3an2 
 |-  ( ( ps /\ a e. { E } /\ b e. N ) -> G e. K )
39 eqidd 
 |-  ( ps -> ( a e. { E } , b e. N |-> F ) = ( a e. { E } , b e. N |-> F ) )
40 eqidd 
 |-  ( ps -> ( a e. { E } , b e. N |-> G ) = ( a e. { E } , b e. N |-> G ) )
41 32 17 37 38 39 40 offval22 
 |-  ( ps -> ( ( a e. { E } , b e. N |-> F ) oF .+ ( a e. { E } , b e. N |-> G ) ) = ( a e. { E } , b e. N |-> ( F .+ G ) ) )
42 41 eqcomd 
 |-  ( ps -> ( a e. { E } , b e. N |-> ( F .+ G ) ) = ( ( a e. { E } , b e. N |-> F ) oF .+ ( a e. { E } , b e. N |-> G ) ) )
43 mposnif 
 |-  ( a e. { E } , b e. N |-> if ( a = E , ( F .+ G ) , H ) ) = ( a e. { E } , b e. N |-> ( F .+ G ) )
44 mposnif 
 |-  ( a e. { E } , b e. N |-> if ( a = E , F , H ) ) = ( a e. { E } , b e. N |-> F )
45 mposnif 
 |-  ( a e. { E } , b e. N |-> if ( a = E , G , H ) ) = ( a e. { E } , b e. N |-> G )
46 44 45 oveq12i 
 |-  ( ( a e. { E } , b e. N |-> if ( a = E , F , H ) ) oF .+ ( a e. { E } , b e. N |-> if ( a = E , G , H ) ) ) = ( ( a e. { E } , b e. N |-> F ) oF .+ ( a e. { E } , b e. N |-> G ) )
47 42 43 46 3eqtr4g 
 |-  ( ps -> ( a e. { E } , b e. N |-> if ( a = E , ( F .+ G ) , H ) ) = ( ( a e. { E } , b e. N |-> if ( a = E , F , H ) ) oF .+ ( a e. { E } , b e. N |-> if ( a = E , G , H ) ) ) )
48 ssid 
 |-  N C_ N
49 resmpo 
 |-  ( ( { E } C_ N /\ N C_ N ) -> ( ( a e. N , b e. N |-> if ( a = E , ( F .+ G ) , H ) ) |` ( { E } X. N ) ) = ( a e. { E } , b e. N |-> if ( a = E , ( F .+ G ) , H ) ) )
50 33 48 49 sylancl 
 |-  ( ps -> ( ( a e. N , b e. N |-> if ( a = E , ( F .+ G ) , H ) ) |` ( { E } X. N ) ) = ( a e. { E } , b e. N |-> if ( a = E , ( F .+ G ) , H ) ) )
51 resmpo 
 |-  ( ( { E } C_ N /\ N C_ N ) -> ( ( a e. N , b e. N |-> if ( a = E , F , H ) ) |` ( { E } X. N ) ) = ( a e. { E } , b e. N |-> if ( a = E , F , H ) ) )
52 33 48 51 sylancl 
 |-  ( ps -> ( ( a e. N , b e. N |-> if ( a = E , F , H ) ) |` ( { E } X. N ) ) = ( a e. { E } , b e. N |-> if ( a = E , F , H ) ) )
53 resmpo 
 |-  ( ( { E } C_ N /\ N C_ N ) -> ( ( a e. N , b e. N |-> if ( a = E , G , H ) ) |` ( { E } X. N ) ) = ( a e. { E } , b e. N |-> if ( a = E , G , H ) ) )
54 33 48 53 sylancl 
 |-  ( ps -> ( ( a e. N , b e. N |-> if ( a = E , G , H ) ) |` ( { E } X. N ) ) = ( a e. { E } , b e. N |-> if ( a = E , G , H ) ) )
55 52 54 oveq12d 
 |-  ( ps -> ( ( ( a e. N , b e. N |-> if ( a = E , F , H ) ) |` ( { E } X. N ) ) oF .+ ( ( a e. N , b e. N |-> if ( a = E , G , H ) ) |` ( { E } X. N ) ) ) = ( ( a e. { E } , b e. N |-> if ( a = E , F , H ) ) oF .+ ( a e. { E } , b e. N |-> if ( a = E , G , H ) ) ) )
56 47 50 55 3eqtr4d 
 |-  ( ps -> ( ( a e. N , b e. N |-> if ( a = E , ( F .+ G ) , H ) ) |` ( { E } X. N ) ) = ( ( ( a e. N , b e. N |-> if ( a = E , F , H ) ) |` ( { E } X. N ) ) oF .+ ( ( a e. N , b e. N |-> if ( a = E , G , H ) ) |` ( { E } X. N ) ) ) )
57 eldifsni 
 |-  ( a e. ( N \ { E } ) -> a =/= E )
58 57 3ad2ant2 
 |-  ( ( ps /\ a e. ( N \ { E } ) /\ b e. N ) -> a =/= E )
59 58 neneqd 
 |-  ( ( ps /\ a e. ( N \ { E } ) /\ b e. N ) -> -. a = E )
60 iffalse 
 |-  ( -. a = E -> if ( a = E , ( F .+ G ) , H ) = H )
61 iffalse 
 |-  ( -. a = E -> if ( a = E , F , H ) = H )
62 60 61 eqtr4d 
 |-  ( -. a = E -> if ( a = E , ( F .+ G ) , H ) = if ( a = E , F , H ) )
63 59 62 syl 
 |-  ( ( ps /\ a e. ( N \ { E } ) /\ b e. N ) -> if ( a = E , ( F .+ G ) , H ) = if ( a = E , F , H ) )
64 63 mpoeq3dva 
 |-  ( ps -> ( a e. ( N \ { E } ) , b e. N |-> if ( a = E , ( F .+ G ) , H ) ) = ( a e. ( N \ { E } ) , b e. N |-> if ( a = E , F , H ) ) )
65 difss 
 |-  ( N \ { E } ) C_ N
66 resmpo 
 |-  ( ( ( N \ { E } ) C_ N /\ N C_ N ) -> ( ( a e. N , b e. N |-> if ( a = E , ( F .+ G ) , H ) ) |` ( ( N \ { E } ) X. N ) ) = ( a e. ( N \ { E } ) , b e. N |-> if ( a = E , ( F .+ G ) , H ) ) )
67 65 48 66 mp2an 
 |-  ( ( a e. N , b e. N |-> if ( a = E , ( F .+ G ) , H ) ) |` ( ( N \ { E } ) X. N ) ) = ( a e. ( N \ { E } ) , b e. N |-> if ( a = E , ( F .+ G ) , H ) )
68 resmpo 
 |-  ( ( ( N \ { E } ) C_ N /\ N C_ N ) -> ( ( a e. N , b e. N |-> if ( a = E , F , H ) ) |` ( ( N \ { E } ) X. N ) ) = ( a e. ( N \ { E } ) , b e. N |-> if ( a = E , F , H ) ) )
69 65 48 68 mp2an 
 |-  ( ( a e. N , b e. N |-> if ( a = E , F , H ) ) |` ( ( N \ { E } ) X. N ) ) = ( a e. ( N \ { E } ) , b e. N |-> if ( a = E , F , H ) )
70 64 67 69 3eqtr4g 
 |-  ( ps -> ( ( a e. N , b e. N |-> if ( a = E , ( F .+ G ) , H ) ) |` ( ( N \ { E } ) X. N ) ) = ( ( a e. N , b e. N |-> if ( a = E , F , H ) ) |` ( ( N \ { E } ) X. N ) ) )
71 iffalse 
 |-  ( -. a = E -> if ( a = E , G , H ) = H )
72 60 71 eqtr4d 
 |-  ( -. a = E -> if ( a = E , ( F .+ G ) , H ) = if ( a = E , G , H ) )
73 59 72 syl 
 |-  ( ( ps /\ a e. ( N \ { E } ) /\ b e. N ) -> if ( a = E , ( F .+ G ) , H ) = if ( a = E , G , H ) )
74 73 mpoeq3dva 
 |-  ( ps -> ( a e. ( N \ { E } ) , b e. N |-> if ( a = E , ( F .+ G ) , H ) ) = ( a e. ( N \ { E } ) , b e. N |-> if ( a = E , G , H ) ) )
75 resmpo 
 |-  ( ( ( N \ { E } ) C_ N /\ N C_ N ) -> ( ( a e. N , b e. N |-> if ( a = E , G , H ) ) |` ( ( N \ { E } ) X. N ) ) = ( a e. ( N \ { E } ) , b e. N |-> if ( a = E , G , H ) ) )
76 65 48 75 mp2an 
 |-  ( ( a e. N , b e. N |-> if ( a = E , G , H ) ) |` ( ( N \ { E } ) X. N ) ) = ( a e. ( N \ { E } ) , b e. N |-> if ( a = E , G , H ) )
77 74 67 76 3eqtr4g 
 |-  ( ps -> ( ( a e. N , b e. N |-> if ( a = E , ( F .+ G ) , H ) ) |` ( ( N \ { E } ) X. N ) ) = ( ( a e. N , b e. N |-> if ( a = E , G , H ) ) |` ( ( N \ { E } ) X. N ) ) )
78 1 2 3 4 5 6 7 8 9 10 11 12 13 mdetunilem3 
 |-  ( ( ( ph /\ ( a e. N , b e. N |-> if ( a = E , ( F .+ G ) , H ) ) e. B /\ ( a e. N , b e. N |-> if ( a = E , F , H ) ) e. B ) /\ ( ( a e. N , b e. N |-> if ( a = E , G , H ) ) e. B /\ E e. N /\ ( ( a e. N , b e. N |-> if ( a = E , ( F .+ G ) , H ) ) |` ( { E } X. N ) ) = ( ( ( a e. N , b e. N |-> if ( a = E , F , H ) ) |` ( { E } X. N ) ) oF .+ ( ( a e. N , b e. N |-> if ( a = E , G , H ) ) |` ( { E } X. N ) ) ) ) /\ ( ( ( a e. N , b e. N |-> if ( a = E , ( F .+ G ) , H ) ) |` ( ( N \ { E } ) X. N ) ) = ( ( a e. N , b e. N |-> if ( a = E , F , H ) ) |` ( ( N \ { E } ) X. N ) ) /\ ( ( a e. N , b e. N |-> if ( a = E , ( F .+ G ) , H ) ) |` ( ( N \ { E } ) X. N ) ) = ( ( a e. N , b e. N |-> if ( a = E , G , H ) ) |` ( ( N \ { E } ) X. N ) ) ) ) -> ( D ` ( a e. N , b e. N |-> if ( a = E , ( F .+ G ) , H ) ) ) = ( ( D ` ( a e. N , b e. N |-> if ( a = E , F , H ) ) ) .+ ( D ` ( a e. N , b e. N |-> if ( a = E , G , H ) ) ) ) )
79 14 26 28 30 15 56 70 77 78 syl332anc 
 |-  ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = E , ( F .+ G ) , H ) ) ) = ( ( D ` ( a e. N , b e. N |-> if ( a = E , F , H ) ) ) .+ ( D ` ( a e. N , b e. N |-> if ( a = E , G , H ) ) ) ) )