Metamath Proof Explorer

Theorem cpmatacl

Description: The set of all constant polynomial matrices over a ring R is closed under addition. (Contributed by AV, 17-Nov-2019) (Proof shortened by AV, 28-Nov-2019)

Ref Expression
Hypotheses cpmatsrngpmat.s 
|- S = ( N ConstPolyMat R )
cpmatsrngpmat.p 
|- P = ( Poly1 ` R )
cpmatsrngpmat.c 
|- C = ( N Mat P )
Assertion cpmatacl 
|- ( ( N e. Fin /\ R e. Ring ) -> A. x e. S A. y e. S ( x ( +g ` C ) y ) e. S )

Proof

Step Hyp Ref Expression
1 cpmatsrngpmat.s 
 |-  S = ( N ConstPolyMat R )
2 cpmatsrngpmat.p 
 |-  P = ( Poly1 ` R )
3 cpmatsrngpmat.c 
 |-  C = ( N Mat P )
4 eqid 
 |-  ( Base ` C ) = ( Base ` C )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
7 1 2 3 4 5 6 cpmatelimp2 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( x e. S -> ( x e. ( Base ` C ) /\ A. i e. N A. j e. N E. a e. ( Base ` R ) ( i x j ) = ( ( algSc ` P ) ` a ) ) ) )
8 1 2 3 4 5 6 cpmatelimp2 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( y e. S -> ( y e. ( Base ` C ) /\ A. i e. N A. j e. N E. b e. ( Base ` R ) ( i y j ) = ( ( algSc ` P ) ` b ) ) ) )
9 r19.26-2 
 |-  ( A. i e. N A. j e. N ( E. a e. ( Base ` R ) ( i x j ) = ( ( algSc ` P ) ` a ) /\ E. b e. ( Base ` R ) ( i y j ) = ( ( algSc ` P ) ` b ) ) <-> ( A. i e. N A. j e. N E. a e. ( Base ` R ) ( i x j ) = ( ( algSc ` P ) ` a ) /\ A. i e. N A. j e. N E. b e. ( Base ` R ) ( i y j ) = ( ( algSc ` P ) ` b ) ) )
10 eqid 
 |-  ( +g ` R ) = ( +g ` R )
11 5 10 ringacl 
 |-  ( ( R e. Ring /\ a e. ( Base ` R ) /\ b e. ( Base ` R ) ) -> ( a ( +g ` R ) b ) e. ( Base ` R ) )
12 11 3expb 
 |-  ( ( R e. Ring /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) -> ( a ( +g ` R ) b ) e. ( Base ` R ) )
13 2 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
14 13 eqcomd 
 |-  ( R e. Ring -> ( Scalar ` P ) = R )
15 14 fveq2d 
 |-  ( R e. Ring -> ( +g ` ( Scalar ` P ) ) = ( +g ` R ) )
16 15 oveqd 
 |-  ( R e. Ring -> ( a ( +g ` ( Scalar ` P ) ) b ) = ( a ( +g ` R ) b ) )
17 16 eleq1d 
 |-  ( R e. Ring -> ( ( a ( +g ` ( Scalar ` P ) ) b ) e. ( Base ` R ) <-> ( a ( +g ` R ) b ) e. ( Base ` R ) ) )
18 17 adantr 
 |-  ( ( R e. Ring /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) -> ( ( a ( +g ` ( Scalar ` P ) ) b ) e. ( Base ` R ) <-> ( a ( +g ` R ) b ) e. ( Base ` R ) ) )
19 12 18 mpbird 
 |-  ( ( R e. Ring /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) -> ( a ( +g ` ( Scalar ` P ) ) b ) e. ( Base ` R ) )
20 19 ad5ant25 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) -> ( a ( +g ` ( Scalar ` P ) ) b ) e. ( Base ` R ) )
21 20 adantr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) /\ ( ( i y j ) = ( ( algSc ` P ) ` b ) /\ ( i x j ) = ( ( algSc ` P ) ` a ) ) ) -> ( a ( +g ` ( Scalar ` P ) ) b ) e. ( Base ` R ) )
22 fveq2 
 |-  ( c = ( a ( +g ` ( Scalar ` P ) ) b ) -> ( ( algSc ` P ) ` c ) = ( ( algSc ` P ) ` ( a ( +g ` ( Scalar ` P ) ) b ) ) )
23 22 eqeq2d 
 |-  ( c = ( a ( +g ` ( Scalar ` P ) ) b ) -> ( ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` c ) <-> ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` ( a ( +g ` ( Scalar ` P ) ) b ) ) ) )
24 23 adantl 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) /\ ( ( i y j ) = ( ( algSc ` P ) ` b ) /\ ( i x j ) = ( ( algSc ` P ) ` a ) ) ) /\ c = ( a ( +g ` ( Scalar ` P ) ) b ) ) -> ( ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` c ) <-> ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` ( a ( +g ` ( Scalar ` P ) ) b ) ) ) )
25 simpr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) -> ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) )
26 25 ancomd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) -> ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) )
27 26 anim1i 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) -> ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) )
28 27 ad2antrr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) /\ ( ( i y j ) = ( ( algSc ` P ) ` b ) /\ ( i x j ) = ( ( algSc ` P ) ` a ) ) ) -> ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) )
29 eqid 
 |-  ( +g ` C ) = ( +g ` C )
30 eqid 
 |-  ( +g ` P ) = ( +g ` P )
31 3 4 29 30 matplusgcell 
 |-  ( ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) -> ( i ( x ( +g ` C ) y ) j ) = ( ( i x j ) ( +g ` P ) ( i y j ) ) )
32 28 31 syl 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) /\ ( ( i y j ) = ( ( algSc ` P ) ` b ) /\ ( i x j ) = ( ( algSc ` P ) ` a ) ) ) -> ( i ( x ( +g ` C ) y ) j ) = ( ( i x j ) ( +g ` P ) ( i y j ) ) )
33 oveq12 
 |-  ( ( ( i x j ) = ( ( algSc ` P ) ` a ) /\ ( i y j ) = ( ( algSc ` P ) ` b ) ) -> ( ( i x j ) ( +g ` P ) ( i y j ) ) = ( ( ( algSc ` P ) ` a ) ( +g ` P ) ( ( algSc ` P ) ` b ) ) )
34 33 ancoms 
 |-  ( ( ( i y j ) = ( ( algSc ` P ) ` b ) /\ ( i x j ) = ( ( algSc ` P ) ` a ) ) -> ( ( i x j ) ( +g ` P ) ( i y j ) ) = ( ( ( algSc ` P ) ` a ) ( +g ` P ) ( ( algSc ` P ) ` b ) ) )
35 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
36 2 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
37 36 ad4antlr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) -> P e. Ring )
38 2 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
39 38 ad4antlr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) -> P e. LMod )
40 6 35 37 39 asclghm 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) -> ( algSc ` P ) e. ( ( Scalar ` P ) GrpHom P ) )
41 13 adantl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R = ( Scalar ` P ) )
42 41 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
43 42 eleq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( a e. ( Base ` R ) <-> a e. ( Base ` ( Scalar ` P ) ) ) )
44 43 biimpd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( a e. ( Base ` R ) -> a e. ( Base ` ( Scalar ` P ) ) ) )
45 44 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) -> ( a e. ( Base ` R ) -> a e. ( Base ` ( Scalar ` P ) ) ) )
46 45 adantrd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) -> ( ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) -> a e. ( Base ` ( Scalar ` P ) ) ) )
47 46 imp 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) -> a e. ( Base ` ( Scalar ` P ) ) )
48 13 ad3antlr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) -> R = ( Scalar ` P ) )
49 48 fveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
50 49 eleq2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) -> ( b e. ( Base ` R ) <-> b e. ( Base ` ( Scalar ` P ) ) ) )
51 50 biimpd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) -> ( b e. ( Base ` R ) -> b e. ( Base ` ( Scalar ` P ) ) ) )
52 51 adantld 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) -> ( ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) -> b e. ( Base ` ( Scalar ` P ) ) ) )
53 52 imp 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) -> b e. ( Base ` ( Scalar ` P ) ) )
54 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
55 eqid 
 |-  ( +g ` ( Scalar ` P ) ) = ( +g ` ( Scalar ` P ) )
56 54 55 30 ghmlin 
 |-  ( ( ( algSc ` P ) e. ( ( Scalar ` P ) GrpHom P ) /\ a e. ( Base ` ( Scalar ` P ) ) /\ b e. ( Base ` ( Scalar ` P ) ) ) -> ( ( algSc ` P ) ` ( a ( +g ` ( Scalar ` P ) ) b ) ) = ( ( ( algSc ` P ) ` a ) ( +g ` P ) ( ( algSc ` P ) ` b ) ) )
57 40 47 53 56 syl3anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) -> ( ( algSc ` P ) ` ( a ( +g ` ( Scalar ` P ) ) b ) ) = ( ( ( algSc ` P ) ` a ) ( +g ` P ) ( ( algSc ` P ) ` b ) ) )
58 57 eqcomd 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) -> ( ( ( algSc ` P ) ` a ) ( +g ` P ) ( ( algSc ` P ) ` b ) ) = ( ( algSc ` P ) ` ( a ( +g ` ( Scalar ` P ) ) b ) ) )
59 34 58 sylan9eqr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) /\ ( ( i y j ) = ( ( algSc ` P ) ` b ) /\ ( i x j ) = ( ( algSc ` P ) ` a ) ) ) -> ( ( i x j ) ( +g ` P ) ( i y j ) ) = ( ( algSc ` P ) ` ( a ( +g ` ( Scalar ` P ) ) b ) ) )
60 32 59 eqtrd 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) /\ ( ( i y j ) = ( ( algSc ` P ) ` b ) /\ ( i x j ) = ( ( algSc ` P ) ` a ) ) ) -> ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` ( a ( +g ` ( Scalar ` P ) ) b ) ) )
61 21 24 60 rspcedvd 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) /\ ( ( i y j ) = ( ( algSc ` P ) ` b ) /\ ( i x j ) = ( ( algSc ` P ) ` a ) ) ) -> E. c e. ( Base ` R ) ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` c ) )
62 61 exp32 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) -> ( ( i y j ) = ( ( algSc ` P ) ` b ) -> ( ( i x j ) = ( ( algSc ` P ) ` a ) -> E. c e. ( Base ` R ) ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` c ) ) ) )
63 62 anassrs 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) -> ( ( i y j ) = ( ( algSc ` P ) ` b ) -> ( ( i x j ) = ( ( algSc ` P ) ` a ) -> E. c e. ( Base ` R ) ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` c ) ) ) )
64 63 rexlimdva 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) /\ a e. ( Base ` R ) ) -> ( E. b e. ( Base ` R ) ( i y j ) = ( ( algSc ` P ) ` b ) -> ( ( i x j ) = ( ( algSc ` P ) ` a ) -> E. c e. ( Base ` R ) ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` c ) ) ) )
65 64 com23 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) /\ a e. ( Base ` R ) ) -> ( ( i x j ) = ( ( algSc ` P ) ` a ) -> ( E. b e. ( Base ` R ) ( i y j ) = ( ( algSc ` P ) ` b ) -> E. c e. ( Base ` R ) ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` c ) ) ) )
66 65 rexlimdva 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) -> ( E. a e. ( Base ` R ) ( i x j ) = ( ( algSc ` P ) ` a ) -> ( E. b e. ( Base ` R ) ( i y j ) = ( ( algSc ` P ) ` b ) -> E. c e. ( Base ` R ) ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` c ) ) ) )
67 66 impd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) /\ ( i e. N /\ j e. N ) ) -> ( ( E. a e. ( Base ` R ) ( i x j ) = ( ( algSc ` P ) ` a ) /\ E. b e. ( Base ` R ) ( i y j ) = ( ( algSc ` P ) ` b ) ) -> E. c e. ( Base ` R ) ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` c ) ) )
68 67 ralimdvva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) -> ( A. i e. N A. j e. N ( E. a e. ( Base ` R ) ( i x j ) = ( ( algSc ` P ) ` a ) /\ E. b e. ( Base ` R ) ( i y j ) = ( ( algSc ` P ) ` b ) ) -> A. i e. N A. j e. N E. c e. ( Base ` R ) ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` c ) ) )
69 9 68 syl5bir 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) -> ( ( A. i e. N A. j e. N E. a e. ( Base ` R ) ( i x j ) = ( ( algSc ` P ) ` a ) /\ A. i e. N A. j e. N E. b e. ( Base ` R ) ( i y j ) = ( ( algSc ` P ) ` b ) ) -> A. i e. N A. j e. N E. c e. ( Base ` R ) ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` c ) ) )
70 69 expd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) ) -> ( A. i e. N A. j e. N E. a e. ( Base ` R ) ( i x j ) = ( ( algSc ` P ) ` a ) -> ( A. i e. N A. j e. N E. b e. ( Base ` R ) ( i y j ) = ( ( algSc ` P ) ` b ) -> A. i e. N A. j e. N E. c e. ( Base ` R ) ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` c ) ) ) )
71 70 expr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ y e. ( Base ` C ) ) -> ( x e. ( Base ` C ) -> ( A. i e. N A. j e. N E. a e. ( Base ` R ) ( i x j ) = ( ( algSc ` P ) ` a ) -> ( A. i e. N A. j e. N E. b e. ( Base ` R ) ( i y j ) = ( ( algSc ` P ) ` b ) -> A. i e. N A. j e. N E. c e. ( Base ` R ) ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` c ) ) ) ) )
72 71 impd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ y e. ( Base ` C ) ) -> ( ( x e. ( Base ` C ) /\ A. i e. N A. j e. N E. a e. ( Base ` R ) ( i x j ) = ( ( algSc ` P ) ` a ) ) -> ( A. i e. N A. j e. N E. b e. ( Base ` R ) ( i y j ) = ( ( algSc ` P ) ` b ) -> A. i e. N A. j e. N E. c e. ( Base ` R ) ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` c ) ) ) )
73 72 ex 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( y e. ( Base ` C ) -> ( ( x e. ( Base ` C ) /\ A. i e. N A. j e. N E. a e. ( Base ` R ) ( i x j ) = ( ( algSc ` P ) ` a ) ) -> ( A. i e. N A. j e. N E. b e. ( Base ` R ) ( i y j ) = ( ( algSc ` P ) ` b ) -> A. i e. N A. j e. N E. c e. ( Base ` R ) ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` c ) ) ) ) )
74 73 com34 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( y e. ( Base ` C ) -> ( A. i e. N A. j e. N E. b e. ( Base ` R ) ( i y j ) = ( ( algSc ` P ) ` b ) -> ( ( x e. ( Base ` C ) /\ A. i e. N A. j e. N E. a e. ( Base ` R ) ( i x j ) = ( ( algSc ` P ) ` a ) ) -> A. i e. N A. j e. N E. c e. ( Base ` R ) ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` c ) ) ) ) )
75 74 impd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( y e. ( Base ` C ) /\ A. i e. N A. j e. N E. b e. ( Base ` R ) ( i y j ) = ( ( algSc ` P ) ` b ) ) -> ( ( x e. ( Base ` C ) /\ A. i e. N A. j e. N E. a e. ( Base ` R ) ( i x j ) = ( ( algSc ` P ) ` a ) ) -> A. i e. N A. j e. N E. c e. ( Base ` R ) ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` c ) ) ) )
76 8 75 syld 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( y e. S -> ( ( x e. ( Base ` C ) /\ A. i e. N A. j e. N E. a e. ( Base ` R ) ( i x j ) = ( ( algSc ` P ) ` a ) ) -> A. i e. N A. j e. N E. c e. ( Base ` R ) ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` c ) ) ) )
77 76 com23 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( x e. ( Base ` C ) /\ A. i e. N A. j e. N E. a e. ( Base ` R ) ( i x j ) = ( ( algSc ` P ) ` a ) ) -> ( y e. S -> A. i e. N A. j e. N E. c e. ( Base ` R ) ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` c ) ) ) )
78 7 77 syld 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( x e. S -> ( y e. S -> A. i e. N A. j e. N E. c e. ( Base ` R ) ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` c ) ) ) )
79 78 imp32 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> A. i e. N A. j e. N E. c e. ( Base ` R ) ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` c ) )
80 simpl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> N e. Fin )
81 80 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> N e. Fin )
82 simpr 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R e. Ring )
83 82 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> R e. Ring )
84 2 3 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )
85 84 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> C e. Ring )
86 simpl 
 |-  ( ( x e. S /\ y e. S ) -> x e. S )
87 86 anim2i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) )
88 df-3an 
 |-  ( ( N e. Fin /\ R e. Ring /\ x e. S ) <-> ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) )
89 87 88 sylibr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> ( N e. Fin /\ R e. Ring /\ x e. S ) )
90 1 2 3 4 cpmatpmat 
 |-  ( ( N e. Fin /\ R e. Ring /\ x e. S ) -> x e. ( Base ` C ) )
91 89 90 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> x e. ( Base ` C ) )
92 simpr 
 |-  ( ( x e. S /\ y e. S ) -> y e. S )
93 92 anim2i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ y e. S ) )
94 df-3an 
 |-  ( ( N e. Fin /\ R e. Ring /\ y e. S ) <-> ( ( N e. Fin /\ R e. Ring ) /\ y e. S ) )
95 93 94 sylibr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> ( N e. Fin /\ R e. Ring /\ y e. S ) )
96 1 2 3 4 cpmatpmat 
 |-  ( ( N e. Fin /\ R e. Ring /\ y e. S ) -> y e. ( Base ` C ) )
97 95 96 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> y e. ( Base ` C ) )
98 4 29 ringacl 
 |-  ( ( C e. Ring /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( x ( +g ` C ) y ) e. ( Base ` C ) )
99 85 91 97 98 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> ( x ( +g ` C ) y ) e. ( Base ` C ) )
100 1 2 3 4 5 6 cpmatel2 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( x ( +g ` C ) y ) e. ( Base ` C ) ) -> ( ( x ( +g ` C ) y ) e. S <-> A. i e. N A. j e. N E. c e. ( Base ` R ) ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` c ) ) )
101 81 83 99 100 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> ( ( x ( +g ` C ) y ) e. S <-> A. i e. N A. j e. N E. c e. ( Base ` R ) ( i ( x ( +g ` C ) y ) j ) = ( ( algSc ` P ) ` c ) ) )
102 79 101 mpbird 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> ( x ( +g ` C ) y ) e. S )
103 102 ralrimivva 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A. x e. S A. y e. S ( x ( +g ` C ) y ) e. S )