Metamath Proof Explorer

Theorem mdetdiaglem

Description: Lemma for mdetdiag . Previously part of proof for mdet1 . (Contributed by SO, 10-Jul-2018) (Revised by AV, 17-Aug-2019)

Ref Expression
Hypotheses mdetdiag.d 
|- D = ( N maDet R )
mdetdiag.a 
|- A = ( N Mat R )
mdetdiag.b 
|- B = ( Base ` A )
mdetdiag.g 
|- G = ( mulGrp ` R )
mdetdiag.0 
|- .0. = ( 0g ` R )
mdetdiaglem.g 
|- H = ( Base ` ( SymGrp ` N ) )
mdetdiaglem.z 
|- Z = ( ZRHom ` R )
mdetdiaglem.s 
|- S = ( pmSgn ` N )
mdetdiaglem.t 
|- .x. = ( .r ` R )
Assertion mdetdiaglem 
|- ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) /\ ( P e. H /\ P =/= ( _I |` N ) ) ) -> ( ( ( Z o. S ) ` P ) .x. ( G gsum ( k e. N |-> ( ( P ` k ) M k ) ) ) ) = .0. )

Proof

Step Hyp Ref Expression
1 mdetdiag.d 
 |-  D = ( N maDet R )
2 mdetdiag.a 
 |-  A = ( N Mat R )
3 mdetdiag.b 
 |-  B = ( Base ` A )
4 mdetdiag.g 
 |-  G = ( mulGrp ` R )
5 mdetdiag.0 
 |-  .0. = ( 0g ` R )
6 mdetdiaglem.g 
 |-  H = ( Base ` ( SymGrp ` N ) )
7 mdetdiaglem.z 
 |-  Z = ( ZRHom ` R )
8 mdetdiaglem.s 
 |-  S = ( pmSgn ` N )
9 mdetdiaglem.t 
 |-  .x. = ( .r ` R )
10 7 a1i 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) /\ ( P e. H /\ P =/= ( _I |` N ) ) ) -> Z = ( ZRHom ` R ) )
11 8 a1i 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) /\ ( P e. H /\ P =/= ( _I |` N ) ) ) -> S = ( pmSgn ` N ) )
12 10 11 coeq12d 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) /\ ( P e. H /\ P =/= ( _I |` N ) ) ) -> ( Z o. S ) = ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) )
13 12 fveq1d 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) /\ ( P e. H /\ P =/= ( _I |` N ) ) ) -> ( ( Z o. S ) ` P ) = ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` P ) )
14 eqid 
 |-  ( SymGrp ` N ) = ( SymGrp ` N )
15 14 6 symgbasf1o 
 |-  ( P e. H -> P : N -1-1-onto-> N )
16 f1ofn 
 |-  ( P : N -1-1-onto-> N -> P Fn N )
17 15 16 syl 
 |-  ( P e. H -> P Fn N )
18 fnnfpeq0 
 |-  ( P Fn N -> ( dom ( P \ _I ) = (/) <-> P = ( _I |` N ) ) )
19 17 18 syl 
 |-  ( P e. H -> ( dom ( P \ _I ) = (/) <-> P = ( _I |` N ) ) )
20 19 adantl 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ P e. H ) -> ( dom ( P \ _I ) = (/) <-> P = ( _I |` N ) ) )
21 20 bicomd 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ P e. H ) -> ( P = ( _I |` N ) <-> dom ( P \ _I ) = (/) ) )
22 21 necon3bid 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ P e. H ) -> ( P =/= ( _I |` N ) <-> dom ( P \ _I ) =/= (/) ) )
23 n0 
 |-  ( dom ( P \ _I ) =/= (/) <-> E. s s e. dom ( P \ _I ) )
24 eqid 
 |-  ( Base ` G ) = ( Base ` G )
25 eqid 
 |-  ( .r ` R ) = ( .r ` R )
26 4 25 mgpplusg 
 |-  ( .r ` R ) = ( +g ` G )
27 4 crngmgp 
 |-  ( R e. CRing -> G e. CMnd )
28 27 3ad2ant1 
 |-  ( ( R e. CRing /\ N e. Fin /\ M e. B ) -> G e. CMnd )
29 28 ad2antrr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> G e. CMnd )
30 simpll2 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> N e. Fin )
31 eqid 
 |-  ( Base ` R ) = ( Base ` R )
32 2 31 3 matbas2i 
 |-  ( M e. B -> M e. ( ( Base ` R ) ^m ( N X. N ) ) )
33 32 3ad2ant3 
 |-  ( ( R e. CRing /\ N e. Fin /\ M e. B ) -> M e. ( ( Base ` R ) ^m ( N X. N ) ) )
34 elmapi 
 |-  ( M e. ( ( Base ` R ) ^m ( N X. N ) ) -> M : ( N X. N ) --> ( Base ` R ) )
35 33 34 syl 
 |-  ( ( R e. CRing /\ N e. Fin /\ M e. B ) -> M : ( N X. N ) --> ( Base ` R ) )
36 4 31 mgpbas 
 |-  ( Base ` R ) = ( Base ` G )
37 36 eqcomi 
 |-  ( Base ` G ) = ( Base ` R )
38 37 a1i 
 |-  ( ( R e. CRing /\ N e. Fin /\ M e. B ) -> ( Base ` G ) = ( Base ` R ) )
39 38 feq3d 
 |-  ( ( R e. CRing /\ N e. Fin /\ M e. B ) -> ( M : ( N X. N ) --> ( Base ` G ) <-> M : ( N X. N ) --> ( Base ` R ) ) )
40 35 39 mpbird 
 |-  ( ( R e. CRing /\ N e. Fin /\ M e. B ) -> M : ( N X. N ) --> ( Base ` G ) )
41 40 ad3antrrr 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) /\ k e. N ) -> M : ( N X. N ) --> ( Base ` G ) )
42 14 6 symgbasf 
 |-  ( P e. H -> P : N --> N )
43 42 ad2antrl 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> P : N --> N )
44 43 ffvelrnda 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) /\ k e. N ) -> ( P ` k ) e. N )
45 simpr 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) /\ k e. N ) -> k e. N )
46 41 44 45 fovrnd 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) /\ k e. N ) -> ( ( P ` k ) M k ) e. ( Base ` G ) )
47 disjdif 
 |-  ( { s } i^i ( N \ { s } ) ) = (/)
48 47 a1i 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> ( { s } i^i ( N \ { s } ) ) = (/) )
49 difss 
 |-  ( P \ _I ) C_ P
50 dmss 
 |-  ( ( P \ _I ) C_ P -> dom ( P \ _I ) C_ dom P )
51 49 50 ax-mp 
 |-  dom ( P \ _I ) C_ dom P
52 42 adantl 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ P e. H ) -> P : N --> N )
53 51 52 fssdm 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ P e. H ) -> dom ( P \ _I ) C_ N )
54 53 sseld 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ P e. H ) -> ( s e. dom ( P \ _I ) -> s e. N ) )
55 54 impr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> s e. N )
56 55 snssd 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> { s } C_ N )
57 undif 
 |-  ( { s } C_ N <-> ( { s } u. ( N \ { s } ) ) = N )
58 56 57 sylib 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> ( { s } u. ( N \ { s } ) ) = N )
59 58 eqcomd 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> N = ( { s } u. ( N \ { s } ) ) )
60 24 26 29 30 46 48 59 gsummptfidmsplit 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> ( G gsum ( k e. N |-> ( ( P ` k ) M k ) ) ) = ( ( G gsum ( k e. { s } |-> ( ( P ` k ) M k ) ) ) ( .r ` R ) ( G gsum ( k e. ( N \ { s } ) |-> ( ( P ` k ) M k ) ) ) ) )
61 crngring 
 |-  ( R e. CRing -> R e. Ring )
62 61 adantr 
 |-  ( ( R e. CRing /\ N e. Fin ) -> R e. Ring )
63 4 ringmgp 
 |-  ( R e. Ring -> G e. Mnd )
64 62 63 syl 
 |-  ( ( R e. CRing /\ N e. Fin ) -> G e. Mnd )
65 64 3adant3 
 |-  ( ( R e. CRing /\ N e. Fin /\ M e. B ) -> G e. Mnd )
66 65 ad2antrr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> G e. Mnd )
67 vex 
 |-  s e. _V
68 67 a1i 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> s e. _V )
69 35 ad2antrr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> M : ( N X. N ) --> ( Base ` R ) )
70 43 55 ffvelrnd 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> ( P ` s ) e. N )
71 69 70 55 fovrnd 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> ( ( P ` s ) M s ) e. ( Base ` R ) )
72 fveq2 
 |-  ( k = s -> ( P ` k ) = ( P ` s ) )
73 id 
 |-  ( k = s -> k = s )
74 72 73 oveq12d 
 |-  ( k = s -> ( ( P ` k ) M k ) = ( ( P ` s ) M s ) )
75 36 74 gsumsn 
 |-  ( ( G e. Mnd /\ s e. _V /\ ( ( P ` s ) M s ) e. ( Base ` R ) ) -> ( G gsum ( k e. { s } |-> ( ( P ` k ) M k ) ) ) = ( ( P ` s ) M s ) )
76 66 68 71 75 syl3anc 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> ( G gsum ( k e. { s } |-> ( ( P ` k ) M k ) ) ) = ( ( P ` s ) M s ) )
77 simprr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> s e. dom ( P \ _I ) )
78 17 ad2antrl 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> P Fn N )
79 fnelnfp 
 |-  ( ( P Fn N /\ s e. N ) -> ( s e. dom ( P \ _I ) <-> ( P ` s ) =/= s ) )
80 78 55 79 syl2anc 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> ( s e. dom ( P \ _I ) <-> ( P ` s ) =/= s ) )
81 77 80 mpbid 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> ( P ` s ) =/= s )
82 42 ad2antrl 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> P : N --> N )
83 42 adantl 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ P e. H ) -> P : N --> N )
84 51 83 fssdm 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ P e. H ) -> dom ( P \ _I ) C_ N )
85 84 sseld 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ P e. H ) -> ( s e. dom ( P \ _I ) -> s e. N ) )
86 85 impr 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> s e. N )
87 82 86 ffvelrnd 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> ( P ` s ) e. N )
88 neeq1 
 |-  ( i = ( P ` s ) -> ( i =/= j <-> ( P ` s ) =/= j ) )
89 oveq1 
 |-  ( i = ( P ` s ) -> ( i M j ) = ( ( P ` s ) M j ) )
90 89 eqeq1d 
 |-  ( i = ( P ` s ) -> ( ( i M j ) = .0. <-> ( ( P ` s ) M j ) = .0. ) )
91 88 90 imbi12d 
 |-  ( i = ( P ` s ) -> ( ( i =/= j -> ( i M j ) = .0. ) <-> ( ( P ` s ) =/= j -> ( ( P ` s ) M j ) = .0. ) ) )
92 neeq2 
 |-  ( j = s -> ( ( P ` s ) =/= j <-> ( P ` s ) =/= s ) )
93 oveq2 
 |-  ( j = s -> ( ( P ` s ) M j ) = ( ( P ` s ) M s ) )
94 93 eqeq1d 
 |-  ( j = s -> ( ( ( P ` s ) M j ) = .0. <-> ( ( P ` s ) M s ) = .0. ) )
95 92 94 imbi12d 
 |-  ( j = s -> ( ( ( P ` s ) =/= j -> ( ( P ` s ) M j ) = .0. ) <-> ( ( P ` s ) =/= s -> ( ( P ` s ) M s ) = .0. ) ) )
96 91 95 rspc2v 
 |-  ( ( ( P ` s ) e. N /\ s e. N ) -> ( A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) -> ( ( P ` s ) =/= s -> ( ( P ` s ) M s ) = .0. ) ) )
97 87 86 96 syl2anc 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> ( A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) -> ( ( P ` s ) =/= s -> ( ( P ` s ) M s ) = .0. ) ) )
98 97 impancom 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> ( ( P e. H /\ s e. dom ( P \ _I ) ) -> ( ( P ` s ) =/= s -> ( ( P ` s ) M s ) = .0. ) ) )
99 98 imp 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> ( ( P ` s ) =/= s -> ( ( P ` s ) M s ) = .0. ) )
100 81 99 mpd 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> ( ( P ` s ) M s ) = .0. )
101 76 100 eqtrd 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> ( G gsum ( k e. { s } |-> ( ( P ` k ) M k ) ) ) = .0. )
102 101 oveq1d 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> ( ( G gsum ( k e. { s } |-> ( ( P ` k ) M k ) ) ) ( .r ` R ) ( G gsum ( k e. ( N \ { s } ) |-> ( ( P ` k ) M k ) ) ) ) = ( .0. ( .r ` R ) ( G gsum ( k e. ( N \ { s } ) |-> ( ( P ` k ) M k ) ) ) ) )
103 61 3ad2ant1 
 |-  ( ( R e. CRing /\ N e. Fin /\ M e. B ) -> R e. Ring )
104 103 ad2antrr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> R e. Ring )
105 28 adantr 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ P e. H ) -> G e. CMnd )
106 simpl2 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ P e. H ) -> N e. Fin )
107 difss 
 |-  ( N \ { s } ) C_ N
108 ssfi 
 |-  ( ( N e. Fin /\ ( N \ { s } ) C_ N ) -> ( N \ { s } ) e. Fin )
109 106 107 108 sylancl 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ P e. H ) -> ( N \ { s } ) e. Fin )
110 35 ad2antrr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ P e. H ) /\ k e. ( N \ { s } ) ) -> M : ( N X. N ) --> ( Base ` R ) )
111 83 adantr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ P e. H ) /\ k e. ( N \ { s } ) ) -> P : N --> N )
112 eldifi 
 |-  ( k e. ( N \ { s } ) -> k e. N )
113 112 adantl 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ P e. H ) /\ k e. ( N \ { s } ) ) -> k e. N )
114 111 113 ffvelrnd 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ P e. H ) /\ k e. ( N \ { s } ) ) -> ( P ` k ) e. N )
115 110 114 113 fovrnd 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ P e. H ) /\ k e. ( N \ { s } ) ) -> ( ( P ` k ) M k ) e. ( Base ` R ) )
116 115 ralrimiva 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ P e. H ) -> A. k e. ( N \ { s } ) ( ( P ` k ) M k ) e. ( Base ` R ) )
117 36 105 109 116 gsummptcl 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ P e. H ) -> ( G gsum ( k e. ( N \ { s } ) |-> ( ( P ` k ) M k ) ) ) e. ( Base ` R ) )
118 117 ad2ant2r 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> ( G gsum ( k e. ( N \ { s } ) |-> ( ( P ` k ) M k ) ) ) e. ( Base ` R ) )
119 31 25 5 ringlz 
 |-  ( ( R e. Ring /\ ( G gsum ( k e. ( N \ { s } ) |-> ( ( P ` k ) M k ) ) ) e. ( Base ` R ) ) -> ( .0. ( .r ` R ) ( G gsum ( k e. ( N \ { s } ) |-> ( ( P ` k ) M k ) ) ) ) = .0. )
120 104 118 119 syl2anc 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> ( .0. ( .r ` R ) ( G gsum ( k e. ( N \ { s } ) |-> ( ( P ` k ) M k ) ) ) ) = .0. )
121 60 102 120 3eqtrd 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ ( P e. H /\ s e. dom ( P \ _I ) ) ) -> ( G gsum ( k e. N |-> ( ( P ` k ) M k ) ) ) = .0. )
122 121 expr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ P e. H ) -> ( s e. dom ( P \ _I ) -> ( G gsum ( k e. N |-> ( ( P ` k ) M k ) ) ) = .0. ) )
123 122 exlimdv 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ P e. H ) -> ( E. s s e. dom ( P \ _I ) -> ( G gsum ( k e. N |-> ( ( P ` k ) M k ) ) ) = .0. ) )
124 23 123 syl5bi 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ P e. H ) -> ( dom ( P \ _I ) =/= (/) -> ( G gsum ( k e. N |-> ( ( P ` k ) M k ) ) ) = .0. ) )
125 22 124 sylbid 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ P e. H ) -> ( P =/= ( _I |` N ) -> ( G gsum ( k e. N |-> ( ( P ` k ) M k ) ) ) = .0. ) )
126 125 expimpd 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> ( ( P e. H /\ P =/= ( _I |` N ) ) -> ( G gsum ( k e. N |-> ( ( P ` k ) M k ) ) ) = .0. ) )
127 126 3impia 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) /\ ( P e. H /\ P =/= ( _I |` N ) ) ) -> ( G gsum ( k e. N |-> ( ( P ` k ) M k ) ) ) = .0. )
128 13 127 oveq12d 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) /\ ( P e. H /\ P =/= ( _I |` N ) ) ) -> ( ( ( Z o. S ) ` P ) .x. ( G gsum ( k e. N |-> ( ( P ` k ) M k ) ) ) ) = ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` P ) .x. .0. ) )
129 3simpa 
 |-  ( ( R e. CRing /\ N e. Fin /\ M e. B ) -> ( R e. CRing /\ N e. Fin ) )
130 simpl 
 |-  ( ( P e. H /\ P =/= ( _I |` N ) ) -> P e. H )
131 61 ad2antrr 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ P e. H ) -> R e. Ring )
132 zrhpsgnmhm 
 |-  ( ( R e. Ring /\ N e. Fin ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) )
133 61 132 sylan 
 |-  ( ( R e. CRing /\ N e. Fin ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) )
134 eqid 
 |-  ( Base ` ( mulGrp ` R ) ) = ( Base ` ( mulGrp ` R ) )
135 6 134 mhmf 
 |-  ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) : H --> ( Base ` ( mulGrp ` R ) ) )
136 133 135 syl 
 |-  ( ( R e. CRing /\ N e. Fin ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) : H --> ( Base ` ( mulGrp ` R ) ) )
137 136 ffvelrnda 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ P e. H ) -> ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` P ) e. ( Base ` ( mulGrp ` R ) ) )
138 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
139 138 31 mgpbas 
 |-  ( Base ` R ) = ( Base ` ( mulGrp ` R ) )
140 139 eqcomi 
 |-  ( Base ` ( mulGrp ` R ) ) = ( Base ` R )
141 140 9 5 ringrz 
 |-  ( ( R e. Ring /\ ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` P ) e. ( Base ` ( mulGrp ` R ) ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` P ) .x. .0. ) = .0. )
142 131 137 141 syl2anc 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ P e. H ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` P ) .x. .0. ) = .0. )
143 129 130 142 syl2an 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ ( P e. H /\ P =/= ( _I |` N ) ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` P ) .x. .0. ) = .0. )
144 143 3adant2 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) /\ ( P e. H /\ P =/= ( _I |` N ) ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` P ) .x. .0. ) = .0. )
145 128 144 eqtrd 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) /\ ( P e. H /\ P =/= ( _I |` N ) ) ) -> ( ( ( Z o. S ) ` P ) .x. ( G gsum ( k e. N |-> ( ( P ` k ) M k ) ) ) ) = .0. )