# Metamath Proof Explorer

## Theorem xpsmnd

Description: The binary product of monoids is a monoid. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypothesis xpsmnd.t ${⊢}{T}={R}{×}_{𝑠}{S}$
Assertion xpsmnd ${⊢}\left({R}\in \mathrm{Mnd}\wedge {S}\in \mathrm{Mnd}\right)\to {T}\in \mathrm{Mnd}$

### Proof

Step Hyp Ref Expression
1 xpsmnd.t ${⊢}{T}={R}{×}_{𝑠}{S}$
2 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
3 eqid ${⊢}{\mathrm{Base}}_{{S}}={\mathrm{Base}}_{{S}}$
4 simpl ${⊢}\left({R}\in \mathrm{Mnd}\wedge {S}\in \mathrm{Mnd}\right)\to {R}\in \mathrm{Mnd}$
5 simpr ${⊢}\left({R}\in \mathrm{Mnd}\wedge {S}\in \mathrm{Mnd}\right)\to {S}\in \mathrm{Mnd}$
6 eqid ${⊢}\left({x}\in {\mathrm{Base}}_{{R}},{y}\in {\mathrm{Base}}_{{S}}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)=\left({x}\in {\mathrm{Base}}_{{R}},{y}\in {\mathrm{Base}}_{{S}}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)$
7 eqid ${⊢}\mathrm{Scalar}\left({R}\right)=\mathrm{Scalar}\left({R}\right)$
8 eqid ${⊢}\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}=\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}$
9 1 2 3 4 5 6 7 8 xpsval ${⊢}\left({R}\in \mathrm{Mnd}\wedge {S}\in \mathrm{Mnd}\right)\to {T}={\left({x}\in {\mathrm{Base}}_{{R}},{y}\in {\mathrm{Base}}_{{S}}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)}^{-1}{“}_{𝑠}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)$
10 6 xpsff1o2 ${⊢}\left({x}\in {\mathrm{Base}}_{{R}},{y}\in {\mathrm{Base}}_{{S}}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right):{\mathrm{Base}}_{{R}}×{\mathrm{Base}}_{{S}}\underset{1-1 onto}{⟶}\mathrm{ran}\left({x}\in {\mathrm{Base}}_{{R}},{y}\in {\mathrm{Base}}_{{S}}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)$
11 1 2 3 4 5 6 7 8 xpsrnbas ${⊢}\left({R}\in \mathrm{Mnd}\wedge {S}\in \mathrm{Mnd}\right)\to \mathrm{ran}\left({x}\in {\mathrm{Base}}_{{R}},{y}\in {\mathrm{Base}}_{{S}}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)={\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)}$
12 11 f1oeq3d ${⊢}\left({R}\in \mathrm{Mnd}\wedge {S}\in \mathrm{Mnd}\right)\to \left(\left({x}\in {\mathrm{Base}}_{{R}},{y}\in {\mathrm{Base}}_{{S}}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right):{\mathrm{Base}}_{{R}}×{\mathrm{Base}}_{{S}}\underset{1-1 onto}{⟶}\mathrm{ran}\left({x}\in {\mathrm{Base}}_{{R}},{y}\in {\mathrm{Base}}_{{S}}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)↔\left({x}\in {\mathrm{Base}}_{{R}},{y}\in {\mathrm{Base}}_{{S}}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right):{\mathrm{Base}}_{{R}}×{\mathrm{Base}}_{{S}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)}\right)$
13 10 12 mpbii ${⊢}\left({R}\in \mathrm{Mnd}\wedge {S}\in \mathrm{Mnd}\right)\to \left({x}\in {\mathrm{Base}}_{{R}},{y}\in {\mathrm{Base}}_{{S}}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right):{\mathrm{Base}}_{{R}}×{\mathrm{Base}}_{{S}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)}$
14 f1ocnv ${⊢}\left({x}\in {\mathrm{Base}}_{{R}},{y}\in {\mathrm{Base}}_{{S}}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right):{\mathrm{Base}}_{{R}}×{\mathrm{Base}}_{{S}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)}\to {\left({x}\in {\mathrm{Base}}_{{R}},{y}\in {\mathrm{Base}}_{{S}}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)}^{-1}:{\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{R}}×{\mathrm{Base}}_{{S}}$
15 f1of1 ${⊢}{\left({x}\in {\mathrm{Base}}_{{R}},{y}\in {\mathrm{Base}}_{{S}}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)}^{-1}:{\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{R}}×{\mathrm{Base}}_{{S}}\to {\left({x}\in {\mathrm{Base}}_{{R}},{y}\in {\mathrm{Base}}_{{S}}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)}^{-1}:{\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)}\underset{1-1}{⟶}{\mathrm{Base}}_{{R}}×{\mathrm{Base}}_{{S}}$
16 13 14 15 3syl ${⊢}\left({R}\in \mathrm{Mnd}\wedge {S}\in \mathrm{Mnd}\right)\to {\left({x}\in {\mathrm{Base}}_{{R}},{y}\in {\mathrm{Base}}_{{S}}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)}^{-1}:{\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)}\underset{1-1}{⟶}{\mathrm{Base}}_{{R}}×{\mathrm{Base}}_{{S}}$
17 2on ${⊢}{2}_{𝑜}\in \mathrm{On}$
18 17 a1i ${⊢}\left({R}\in \mathrm{Mnd}\wedge {S}\in \mathrm{Mnd}\right)\to {2}_{𝑜}\in \mathrm{On}$
19 fvexd ${⊢}\left({R}\in \mathrm{Mnd}\wedge {S}\in \mathrm{Mnd}\right)\to \mathrm{Scalar}\left({R}\right)\in \mathrm{V}$
20 xpscf ${⊢}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}:{2}_{𝑜}⟶\mathrm{Mnd}↔\left({R}\in \mathrm{Mnd}\wedge {S}\in \mathrm{Mnd}\right)$
21 20 biimpri ${⊢}\left({R}\in \mathrm{Mnd}\wedge {S}\in \mathrm{Mnd}\right)\to \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}:{2}_{𝑜}⟶\mathrm{Mnd}$
22 8 18 19 21 prdsmndd ${⊢}\left({R}\in \mathrm{Mnd}\wedge {S}\in \mathrm{Mnd}\right)\to \mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\in \mathrm{Mnd}$
23 eqid ${⊢}{\left({x}\in {\mathrm{Base}}_{{R}},{y}\in {\mathrm{Base}}_{{S}}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)}^{-1}{“}_{𝑠}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)={\left({x}\in {\mathrm{Base}}_{{R}},{y}\in {\mathrm{Base}}_{{S}}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)}^{-1}{“}_{𝑠}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)$
24 eqid ${⊢}{\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)}={\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)}$
25 23 24 imasmndf1 ${⊢}\left({\left({x}\in {\mathrm{Base}}_{{R}},{y}\in {\mathrm{Base}}_{{S}}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)}^{-1}:{\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)}\underset{1-1}{⟶}{\mathrm{Base}}_{{R}}×{\mathrm{Base}}_{{S}}\wedge \mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\in \mathrm{Mnd}\right)\to {\left({x}\in {\mathrm{Base}}_{{R}},{y}\in {\mathrm{Base}}_{{S}}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)}^{-1}{“}_{𝑠}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)\in \mathrm{Mnd}$
26 16 22 25 syl2anc ${⊢}\left({R}\in \mathrm{Mnd}\wedge {S}\in \mathrm{Mnd}\right)\to {\left({x}\in {\mathrm{Base}}_{{R}},{y}\in {\mathrm{Base}}_{{S}}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)}^{-1}{“}_{𝑠}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)\in \mathrm{Mnd}$
27 9 26 eqeltrd ${⊢}\left({R}\in \mathrm{Mnd}\wedge {S}\in \mathrm{Mnd}\right)\to {T}\in \mathrm{Mnd}$