xpsmul

Description: Value of the multiplication operation in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015)

	Ref	Expression
Hypotheses	xpsval.t	$⊢ T = R \times_{𝑠} S$
	xpsval.x	$⊢ X = {Base}_{R}$
	xpsval.y	$⊢ Y = {Base}_{S}$
	xpsval.1	$⊢ φ \to R \in V$
	xpsval.2	$⊢ φ \to S \in W$
	xpsadd.3	$⊢ φ \to A \in X$
	xpsadd.4	$⊢ φ \to B \in Y$
	xpsadd.5	$⊢ φ \to C \in X$
	xpsadd.6	$⊢ φ \to D \in Y$
	xpsadd.7	$⊢ φ \to A \underset{˙}{\cdot} C \in X$
	xpsadd.8	$⊢ φ \to B \underset{˙}{\times} D \in Y$
	xpsmul.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	xpsmul.n	$⊢ \underset{˙}{\times} = \cdot_{S}$
	xpsmul.p	$⊢ \underset{˙}{∙} = \cdot_{T}$
Assertion	xpsmul	$⊢ φ \to ⟨A, B⟩ \underset{˙}{∙} ⟨C, D⟩ = ⟨A \underset{˙}{\cdot} C, B \underset{˙}{\times} D⟩$

Proof

Step	Hyp	Ref	Expression
1		xpsval.t	$⊢ T = R \times_{𝑠} S$
2		xpsval.x	$⊢ X = {Base}_{R}$
3		xpsval.y	$⊢ Y = {Base}_{S}$
4		xpsval.1	$⊢ φ \to R \in V$
5		xpsval.2	$⊢ φ \to S \in W$
6		xpsadd.3	$⊢ φ \to A \in X$
7		xpsadd.4	$⊢ φ \to B \in Y$
8		xpsadd.5	$⊢ φ \to C \in X$
9		xpsadd.6	$⊢ φ \to D \in Y$
10		xpsadd.7	$⊢ φ \to A \underset{˙}{\cdot} C \in X$
11		xpsadd.8	$⊢ φ \to B \underset{˙}{\times} D \in Y$
12		xpsmul.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
13		xpsmul.n	$⊢ \underset{˙}{\times} = \cdot_{S}$
14		xpsmul.p	$⊢ \underset{˙}{∙} = \cdot_{T}$
15		eqid	$⊢ (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) = (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
16		eqid	$⊢ Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} = Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}$
17	15	xpsff1o2	$⊢ (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) : X \times Y \underset{1-1 onto}{⟶} ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
18		f1ocnv	$⊢ (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) : X \times Y \underset{1-1 onto}{⟶} ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) \to {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} : ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) \underset{1-1 onto}{⟶} X \times Y$
19	17 18	mp1i	$⊢ φ \to {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} : ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) \underset{1-1 onto}{⟶} X \times Y$
20		f1ofo	$⊢ {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} : ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) \underset{1-1 onto}{⟶} X \times Y \to {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} : ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) \underset{onto}{⟶} X \times Y$
21	19 20	syl	$⊢ φ \to {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} : ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) \underset{onto}{⟶} X \times Y$
22	19	f1ocpbl	$⊢ (φ \land (a \in ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) \land b \in ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})) \land (c \in ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) \land d \in ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}))) \to (({(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (a) = {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (c) \land {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (b) = {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (d)) \to {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (a \cdot_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})} b) = {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (c \cdot_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})} d))$
23		eqid	$⊢ Scalar (R) = Scalar (R)$
24	1 2 3 4 5 15 23 16	xpsval	$⊢ φ \to T = {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} “_{𝑠} (Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})$
25	1 2 3 4 5 15 23 16	xpsrnbas	$⊢ φ \to ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) = {Base}_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})}$
26		ovexd	$⊢ φ \to Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} \in V$
27		eqid	$⊢ \cdot_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})} = \cdot_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})}$
28	21 22 24 25 26 27 14	imasmulval	$⊢ (φ \land \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \in ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) \land \{⟨\emptyset, C⟩, ⟨1_{𝑜}, D⟩\} \in ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})) \to {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (\{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\}) \underset{˙}{∙} {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (\{⟨\emptyset, C⟩, ⟨1_{𝑜}, D⟩\}) = {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (\{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \cdot_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})} \{⟨\emptyset, C⟩, ⟨1_{𝑜}, D⟩\})$
29		eqid	$⊢ {Base}_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})} = {Base}_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})}$
30		fvexd	$⊢ (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} Fn 2_{𝑜} \land \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \in {Base}_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})} \land \{⟨\emptyset, C⟩, ⟨1_{𝑜}, D⟩\} \in {Base}_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})}) \to Scalar (R) \in V$
31		2on	$⊢ 2_{𝑜} \in On$
32	31	a1i	$⊢ (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} Fn 2_{𝑜} \land \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \in {Base}_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})} \land \{⟨\emptyset, C⟩, ⟨1_{𝑜}, D⟩\} \in {Base}_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})}) \to 2_{𝑜} \in On$
33		simp1	$⊢ (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} Fn 2_{𝑜} \land \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \in {Base}_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})} \land \{⟨\emptyset, C⟩, ⟨1_{𝑜}, D⟩\} \in {Base}_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})}) \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} Fn 2_{𝑜}$
34		simp2	$⊢ (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} Fn 2_{𝑜} \land \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \in {Base}_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})} \land \{⟨\emptyset, C⟩, ⟨1_{𝑜}, D⟩\} \in {Base}_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})}) \to \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \in {Base}_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})}$
35		simp3	$⊢ (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} Fn 2_{𝑜} \land \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \in {Base}_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})} \land \{⟨\emptyset, C⟩, ⟨1_{𝑜}, D⟩\} \in {Base}_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})}) \to \{⟨\emptyset, C⟩, ⟨1_{𝑜}, D⟩\} \in {Base}_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})}$
36	16 29 30 32 33 34 35 27	prdsmulrval	$⊢ (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} Fn 2_{𝑜} \land \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \in {Base}_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})} \land \{⟨\emptyset, C⟩, ⟨1_{𝑜}, D⟩\} \in {Base}_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})}) \to \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \cdot_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})} \{⟨\emptyset, C⟩, ⟨1_{𝑜}, D⟩\} = (k \in 2_{𝑜} ⟼ \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} (k) \cdot_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} \{⟨\emptyset, C⟩, ⟨1_{𝑜}, D⟩\} (k))$
37	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 28 36	xpsaddlem	$⊢ φ \to ⟨A, B⟩ \underset{˙}{∙} ⟨C, D⟩ = ⟨A \underset{˙}{\cdot} C, B \underset{˙}{\times} D⟩$

Metamath Proof Explorer

Theorem xpsmul

Proof