xpsgrp

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

		Ref	Expression
	Hypothesis	xpsgrp.t	$⊢ T = R \times_{𝑠} S$
	Assertion	xpsgrp	$⊢ (R \in Grp \land S \in Grp) \to T \in Grp$

Proof

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

Metamath Proof Explorer

Theorem xpsgrp

Proof