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 ⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
cpmatsrngpmat.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
cpmatsrngpmat.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
Assertion cpmatacl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐶 ) 𝑦 ) ∈ 𝑆 )

Proof

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