xpsvsca

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

	Ref	Expression
Hypotheses	xpssca.t	$⊢ T = R \times_{𝑠} S$
	xpssca.g	$⊢ G = Scalar (R)$
	xpssca.1	$⊢ φ \to R \in V$
	xpssca.2	$⊢ φ \to S \in W$
	xpsvsca.x	$⊢ X = {Base}_{R}$
	xpsvsca.y	$⊢ Y = {Base}_{S}$
	xpsvsca.k	$⊢ K = {Base}_{G}$
	xpsvsca.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	xpsvsca.n	$⊢ \underset{˙}{\times} = \cdot_{S}$
	xpsvsca.p	$⊢ \underset{˙}{∙} = \cdot_{T}$
	xpsvsca.3	$⊢ φ \to A \in K$
	xpsvsca.4	$⊢ φ \to B \in X$
	xpsvsca.5	$⊢ φ \to C \in Y$
	xpsvsca.6	$⊢ φ \to A \underset{˙}{\cdot} B \in X$
	xpsvsca.7	$⊢ φ \to A \underset{˙}{\times} C \in Y$
Assertion	xpsvsca	$⊢ φ \to A \underset{˙}{∙} ⟨B, C⟩ = ⟨A \underset{˙}{\cdot} B, A \underset{˙}{\times} C⟩$

Proof

Step	Hyp	Ref	Expression
1		xpssca.t	$⊢ T = R \times_{𝑠} S$
2		xpssca.g	$⊢ G = Scalar (R)$
3		xpssca.1	$⊢ φ \to R \in V$
4		xpssca.2	$⊢ φ \to S \in W$
5		xpsvsca.x	$⊢ X = {Base}_{R}$
6		xpsvsca.y	$⊢ Y = {Base}_{S}$
7		xpsvsca.k	$⊢ K = {Base}_{G}$
8		xpsvsca.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
9		xpsvsca.n	$⊢ \underset{˙}{\times} = \cdot_{S}$
10		xpsvsca.p	$⊢ \underset{˙}{∙} = \cdot_{T}$
11		xpsvsca.3	$⊢ φ \to A \in K$
12		xpsvsca.4	$⊢ φ \to B \in X$
13		xpsvsca.5	$⊢ φ \to C \in Y$
14		xpsvsca.6	$⊢ φ \to A \underset{˙}{\cdot} B \in X$
15		xpsvsca.7	$⊢ φ \to A \underset{˙}{\times} C \in Y$
16		df-ov	$⊢ B (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) C = (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) (⟨B, C⟩)$
17		eqid	$⊢ (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) = (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
18	17	xpsfval	$⊢ (B \in X \land C \in Y) \to B (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) C = \{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\}$
19	12 13 18	syl2anc	$⊢ φ \to B (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) C = \{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\}$
20	16 19	eqtr3id	$⊢ φ \to (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) (⟨B, C⟩) = \{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\}$
21	12 13	opelxpd	$⊢ φ \to ⟨B, C⟩ \in (X \times Y)$
22	17	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⟩\})$
23		f1of	$⊢ (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⟩\}) : X \times Y ⟶ ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
24	22 23	ax-mp	$⊢ (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) : X \times Y ⟶ ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
25	24	ffvelcdmi	$⊢ ⟨B, C⟩ \in (X \times Y) \to (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) (⟨B, C⟩) \in ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
26	21 25	syl	$⊢ φ \to (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) (⟨B, C⟩) \in ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
27	20 26	eqeltrrd	$⊢ φ \to \{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\} \in ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
28		eqid	$⊢ G ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} = G ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}$
29	1 5 6 3 4 17 2 28	xpsval	$⊢ φ \to T = {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} “_{𝑠} (G ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})$
30	1 5 6 3 4 17 2 28	xpsrnbas	$⊢ φ \to ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) = {Base}_{(G ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})}$
31		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$
32	22 31	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$
33		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$
34	32 33	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$
35		ovexd	$⊢ φ \to G ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} \in V$
36	2	fvexi	$⊢ G \in V$
37	36	a1i	$⊢ ⊤ \to G \in V$
38		prex	$⊢ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} \in V$
39	38	a1i	$⊢ ⊤ \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} \in V$
40	28 37 39	prdssca	$⊢ ⊤ \to G = Scalar (G ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})$
41	40	mptru	$⊢ G = Scalar (G ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})$
42		eqid	$⊢ \cdot_{(G ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})} = \cdot_{(G ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})}$
43	32	f1ovscpbl	$⊢ (φ \land (a \in K \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⟩\}))) \to ({(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (b) = {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (c) \to {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (a \cdot_{(G ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})} b) = {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (a \cdot_{(G ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})} c))$
44	29 30 34 35 41 7 42 10 43	imasvscaval	$⊢ (φ \land A \in K \land \{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\} \in ran (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})) \to A \underset{˙}{∙} {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (\{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\}) = {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (A \cdot_{(G ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})} \{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\})$
45	11 27 44	mpd3an23	$⊢ φ \to A \underset{˙}{∙} {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (\{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\}) = {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (A \cdot_{(G ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})} \{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\})$
46		f1ocnvfv	$⊢ ((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⟩\}) \land ⟨B, C⟩ \in (X \times Y)) \to ((x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) (⟨B, C⟩) = \{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\} \to {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (\{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\}) = ⟨B, C⟩)$
47	22 21 46	sylancr	$⊢ φ \to ((x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) (⟨B, C⟩) = \{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\} \to {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (\{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\}) = ⟨B, C⟩)$
48	20 47	mpd	$⊢ φ \to {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (\{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\}) = ⟨B, C⟩$
49	48	oveq2d	$⊢ φ \to A \underset{˙}{∙} {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (\{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\}) = A \underset{˙}{∙} ⟨B, C⟩$
50		iftrue	$⊢ k = \emptyset \to if (k = \emptyset, R, S) = R$
51	50	fveq2d	$⊢ k = \emptyset \to \cdot_{if (k = \emptyset, R, S)} = \cdot_{R}$
52	51 8	eqtr4di	$⊢ k = \emptyset \to \cdot_{if (k = \emptyset, R, S)} = \underset{˙}{\cdot}$
53		eqidd	$⊢ k = \emptyset \to A = A$
54		iftrue	$⊢ k = \emptyset \to if (k = \emptyset, B, C) = B$
55	52 53 54	oveq123d	$⊢ k = \emptyset \to A \cdot_{if (k = \emptyset, R, S)} if (k = \emptyset, B, C) = A \underset{˙}{\cdot} B$
56		iftrue	$⊢ k = \emptyset \to if (k = \emptyset, A \underset{˙}{\cdot} B, A \underset{˙}{\times} C) = A \underset{˙}{\cdot} B$
57	55 56	eqtr4d	$⊢ k = \emptyset \to A \cdot_{if (k = \emptyset, R, S)} if (k = \emptyset, B, C) = if (k = \emptyset, A \underset{˙}{\cdot} B, A \underset{˙}{\times} C)$
58		iffalse	$⊢ \neg k = \emptyset \to if (k = \emptyset, R, S) = S$
59	58	fveq2d	$⊢ \neg k = \emptyset \to \cdot_{if (k = \emptyset, R, S)} = \cdot_{S}$
60	59 9	eqtr4di	$⊢ \neg k = \emptyset \to \cdot_{if (k = \emptyset, R, S)} = \underset{˙}{\times}$
61		eqidd	$⊢ \neg k = \emptyset \to A = A$
62		iffalse	$⊢ \neg k = \emptyset \to if (k = \emptyset, B, C) = C$
63	60 61 62	oveq123d	$⊢ \neg k = \emptyset \to A \cdot_{if (k = \emptyset, R, S)} if (k = \emptyset, B, C) = A \underset{˙}{\times} C$
64		iffalse	$⊢ \neg k = \emptyset \to if (k = \emptyset, A \underset{˙}{\cdot} B, A \underset{˙}{\times} C) = A \underset{˙}{\times} C$
65	63 64	eqtr4d	$⊢ \neg k = \emptyset \to A \cdot_{if (k = \emptyset, R, S)} if (k = \emptyset, B, C) = if (k = \emptyset, A \underset{˙}{\cdot} B, A \underset{˙}{\times} C)$
66	57 65	pm2.61i	$⊢ A \cdot_{if (k = \emptyset, R, S)} if (k = \emptyset, B, C) = if (k = \emptyset, A \underset{˙}{\cdot} B, A \underset{˙}{\times} C)$
67	3	adantr	$⊢ (φ \land k \in 2_{𝑜}) \to R \in V$
68	4	adantr	$⊢ (φ \land k \in 2_{𝑜}) \to S \in W$
69		simpr	$⊢ (φ \land k \in 2_{𝑜}) \to k \in 2_{𝑜}$
70		fvprif	$⊢ (R \in V \land S \in W \land k \in 2_{𝑜}) \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k) = if (k = \emptyset, R, S)$
71	67 68 69 70	syl3anc	$⊢ (φ \land k \in 2_{𝑜}) \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k) = if (k = \emptyset, R, S)$
72	71	fveq2d	$⊢ (φ \land k \in 2_{𝑜}) \to \cdot_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} = \cdot_{if (k = \emptyset, R, S)}$
73		eqidd	$⊢ (φ \land k \in 2_{𝑜}) \to A = A$
74	12	adantr	$⊢ (φ \land k \in 2_{𝑜}) \to B \in X$
75	13	adantr	$⊢ (φ \land k \in 2_{𝑜}) \to C \in Y$
76		fvprif	$⊢ (B \in X \land C \in Y \land k \in 2_{𝑜}) \to \{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\} (k) = if (k = \emptyset, B, C)$
77	74 75 69 76	syl3anc	$⊢ (φ \land k \in 2_{𝑜}) \to \{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\} (k) = if (k = \emptyset, B, C)$
78	72 73 77	oveq123d	$⊢ (φ \land k \in 2_{𝑜}) \to A \cdot_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} \{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\} (k) = A \cdot_{if (k = \emptyset, R, S)} if (k = \emptyset, B, C)$
79	14	adantr	$⊢ (φ \land k \in 2_{𝑜}) \to A \underset{˙}{\cdot} B \in X$
80	15	adantr	$⊢ (φ \land k \in 2_{𝑜}) \to A \underset{˙}{\times} C \in Y$
81		fvprif	$⊢ (A \underset{˙}{\cdot} B \in X \land A \underset{˙}{\times} C \in Y \land k \in 2_{𝑜}) \to \{⟨\emptyset, A \underset{˙}{\cdot} B⟩, ⟨1_{𝑜}, A \underset{˙}{\times} C⟩\} (k) = if (k = \emptyset, A \underset{˙}{\cdot} B, A \underset{˙}{\times} C)$
82	79 80 69 81	syl3anc	$⊢ (φ \land k \in 2_{𝑜}) \to \{⟨\emptyset, A \underset{˙}{\cdot} B⟩, ⟨1_{𝑜}, A \underset{˙}{\times} C⟩\} (k) = if (k = \emptyset, A \underset{˙}{\cdot} B, A \underset{˙}{\times} C)$
83	66 78 82	3eqtr4a	$⊢ (φ \land k \in 2_{𝑜}) \to A \cdot_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} \{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\} (k) = \{⟨\emptyset, A \underset{˙}{\cdot} B⟩, ⟨1_{𝑜}, A \underset{˙}{\times} C⟩\} (k)$
84	83	mpteq2dva	$⊢ φ \to (k \in 2_{𝑜} ⟼ A \cdot_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} \{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\} (k)) = (k \in 2_{𝑜} ⟼ \{⟨\emptyset, A \underset{˙}{\cdot} B⟩, ⟨1_{𝑜}, A \underset{˙}{\times} C⟩\} (k))$
85		eqid	$⊢ {Base}_{(G ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})} = {Base}_{(G ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})}$
86	36	a1i	$⊢ φ \to G \in V$
87		2on	$⊢ 2_{𝑜} \in On$
88	87	a1i	$⊢ φ \to 2_{𝑜} \in On$
89		fnpr2o	$⊢ (R \in V \land S \in W) \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} Fn 2_{𝑜}$
90	3 4 89	syl2anc	$⊢ φ \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} Fn 2_{𝑜}$
91	27 30	eleqtrd	$⊢ φ \to \{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\} \in {Base}_{(G ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})}$
92	28 85 42 7 86 88 90 11 91	prdsvscaval	$⊢ φ \to A \cdot_{(G ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})} \{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\} = (k \in 2_{𝑜} ⟼ A \cdot_{\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (k)} \{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\} (k))$
93		fnpr2o	$⊢ (A \underset{˙}{\cdot} B \in X \land A \underset{˙}{\times} C \in Y) \to \{⟨\emptyset, A \underset{˙}{\cdot} B⟩, ⟨1_{𝑜}, A \underset{˙}{\times} C⟩\} Fn 2_{𝑜}$
94	14 15 93	syl2anc	$⊢ φ \to \{⟨\emptyset, A \underset{˙}{\cdot} B⟩, ⟨1_{𝑜}, A \underset{˙}{\times} C⟩\} Fn 2_{𝑜}$
95		dffn5	$⊢ \{⟨\emptyset, A \underset{˙}{\cdot} B⟩, ⟨1_{𝑜}, A \underset{˙}{\times} C⟩\} Fn 2_{𝑜} \leftrightarrow \{⟨\emptyset, A \underset{˙}{\cdot} B⟩, ⟨1_{𝑜}, A \underset{˙}{\times} C⟩\} = (k \in 2_{𝑜} ⟼ \{⟨\emptyset, A \underset{˙}{\cdot} B⟩, ⟨1_{𝑜}, A \underset{˙}{\times} C⟩\} (k))$
96	94 95	sylib	$⊢ φ \to \{⟨\emptyset, A \underset{˙}{\cdot} B⟩, ⟨1_{𝑜}, A \underset{˙}{\times} C⟩\} = (k \in 2_{𝑜} ⟼ \{⟨\emptyset, A \underset{˙}{\cdot} B⟩, ⟨1_{𝑜}, A \underset{˙}{\times} C⟩\} (k))$
97	84 92 96	3eqtr4d	$⊢ φ \to A \cdot_{(G ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})} \{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\} = \{⟨\emptyset, A \underset{˙}{\cdot} B⟩, ⟨1_{𝑜}, A \underset{˙}{\times} C⟩\}$
98	97	fveq2d	$⊢ φ \to {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (A \cdot_{(G ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})} \{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\}) = {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (\{⟨\emptyset, A \underset{˙}{\cdot} B⟩, ⟨1_{𝑜}, A \underset{˙}{\times} C⟩\})$
99		df-ov	$⊢ (A \underset{˙}{\cdot} B) (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) (A \underset{˙}{\times} C) = (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) (⟨A \underset{˙}{\cdot} B, A \underset{˙}{\times} C⟩)$
100	17	xpsfval	$⊢ (A \underset{˙}{\cdot} B \in X \land A \underset{˙}{\times} C \in Y) \to (A \underset{˙}{\cdot} B) (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) (A \underset{˙}{\times} C) = \{⟨\emptyset, A \underset{˙}{\cdot} B⟩, ⟨1_{𝑜}, A \underset{˙}{\times} C⟩\}$
101	14 15 100	syl2anc	$⊢ φ \to (A \underset{˙}{\cdot} B) (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) (A \underset{˙}{\times} C) = \{⟨\emptyset, A \underset{˙}{\cdot} B⟩, ⟨1_{𝑜}, A \underset{˙}{\times} C⟩\}$
102	99 101	eqtr3id	$⊢ φ \to (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) (⟨A \underset{˙}{\cdot} B, A \underset{˙}{\times} C⟩) = \{⟨\emptyset, A \underset{˙}{\cdot} B⟩, ⟨1_{𝑜}, A \underset{˙}{\times} C⟩\}$
103	14 15	opelxpd	$⊢ φ \to ⟨A \underset{˙}{\cdot} B, A \underset{˙}{\times} C⟩ \in (X \times Y)$
104		f1ocnvfv	$⊢ ((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⟩\}) \land ⟨A \underset{˙}{\cdot} B, A \underset{˙}{\times} C⟩ \in (X \times Y)) \to ((x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) (⟨A \underset{˙}{\cdot} B, A \underset{˙}{\times} C⟩) = \{⟨\emptyset, A \underset{˙}{\cdot} B⟩, ⟨1_{𝑜}, A \underset{˙}{\times} C⟩\} \to {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (\{⟨\emptyset, A \underset{˙}{\cdot} B⟩, ⟨1_{𝑜}, A \underset{˙}{\times} C⟩\}) = ⟨A \underset{˙}{\cdot} B, A \underset{˙}{\times} C⟩)$
105	22 103 104	sylancr	$⊢ φ \to ((x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) (⟨A \underset{˙}{\cdot} B, A \underset{˙}{\times} C⟩) = \{⟨\emptyset, A \underset{˙}{\cdot} B⟩, ⟨1_{𝑜}, A \underset{˙}{\times} C⟩\} \to {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (\{⟨\emptyset, A \underset{˙}{\cdot} B⟩, ⟨1_{𝑜}, A \underset{˙}{\times} C⟩\}) = ⟨A \underset{˙}{\cdot} B, A \underset{˙}{\times} C⟩)$
106	102 105	mpd	$⊢ φ \to {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (\{⟨\emptyset, A \underset{˙}{\cdot} B⟩, ⟨1_{𝑜}, A \underset{˙}{\times} C⟩\}) = ⟨A \underset{˙}{\cdot} B, A \underset{˙}{\times} C⟩$
107	98 106	eqtrd	$⊢ φ \to {(x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} (A \cdot_{(G ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})} \{⟨\emptyset, B⟩, ⟨1_{𝑜}, C⟩\}) = ⟨A \underset{˙}{\cdot} B, A \underset{˙}{\times} C⟩$
108	45 49 107	3eqtr3d	$⊢ φ \to A \underset{˙}{∙} ⟨B, C⟩ = ⟨A \underset{˙}{\cdot} B, A \underset{˙}{\times} C⟩$

Metamath Proof Explorer

Theorem xpsvsca

Proof