prdssca

Description: Scalar ring of a structure product. (Contributed by Stefan O'Rear, 5-Jan-2015) (Revised by Mario Carneiro, 15-Aug-2015) (Revised by Thierry Arnoux, 16-Jun-2019)

	Ref	Expression
Hypotheses	prdsbas.p	$⊢ P = S ⨉_{𝑠} R$
	prdsbas.s	$⊢ φ \to S \in V$
	prdsbas.r	$⊢ φ \to R \in W$
Assertion	prdssca	$⊢ φ \to S = Scalar (P)$

Proof

Step	Hyp	Ref	Expression
1		prdsbas.p	$⊢ P = S ⨉_{𝑠} R$
2		prdsbas.s	$⊢ φ \to S \in V$
3		prdsbas.r	$⊢ φ \to R \in W$
4		eqid	$⊢ {Base}_{S} = {Base}_{S}$
5		eqidd	$⊢ φ \to dom R = dom R$
6		eqidd	$⊢ φ \to \underset{x \in dom R}{⨉} {Base}_{R (x)} = \underset{x \in dom R}{⨉} {Base}_{R (x)}$
7		eqidd	$⊢ φ \to (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f (x) +_{R (x)} g (x))) = (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f (x) +_{R (x)} g (x)))$
8		eqidd	$⊢ φ \to (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f (x) \cdot_{R (x)} g (x))) = (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f (x) \cdot_{R (x)} g (x)))$
9		eqidd	$⊢ φ \to (f \in {Base}_{S}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f \cdot_{R (x)} g (x))) = (f \in {Base}_{S}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f \cdot_{R (x)} g (x)))$
10		eqidd	$⊢ φ \to (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x))) = (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))$
11		eqidd	$⊢ φ \to \prod_{𝑡} (TopOpen \circ R) = \prod_{𝑡} (TopOpen \circ R)$
12		eqidd	$⊢ φ \to \{⟨f, g⟩ \| (\{f, g\} \subseteq \underset{x \in dom R}{⨉} {Base}_{R (x)} \land \forall x \in dom R f (x) \leq_{R (x)} g (x))\} = \{⟨f, g⟩ \| (\{f, g\} \subseteq \underset{x \in dom R}{⨉} {Base}_{R (x)} \land \forall x \in dom R f (x) \leq_{R (x)} g (x))\}$
13		eqidd	$⊢ φ \to (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ sup (ran (x \in dom R ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{} <)) = (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ sup (ran (x \in dom R ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{} <))$
14		eqidd	$⊢ φ \to (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{⨉} (f (x) Hom (R (x)) g (x))) = (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{⨉} (f (x) Hom (R (x)) g (x)))$
15		eqidd	$⊢ φ \to (a \in (\underset{x \in dom R}{⨉} {Base}_{R (x)} \times \underset{x \in dom R}{⨉} {Base}_{R (x)}), c \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (d \in (c (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{⨉} (f (x) Hom (R (x)) g (x))) 2^{nd} (a)), e \in (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{⨉} (f (x) Hom (R (x)) g (x))) (a) ⟼ (x \in dom R ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x)))) = (a \in (\underset{x \in dom R}{⨉} {Base}_{R (x)} \times \underset{x \in dom R}{⨉} {Base}_{R (x)}), c \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (d \in (c (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{⨉} (f (x) Hom (R (x)) g (x))) 2^{nd} (a)), e \in (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{⨉} (f (x) Hom (R (x)) g (x))) (a) ⟼ (x \in dom R ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))$
16	1 4 5 6 7 8 9 10 11 12 13 14 15 2 3	prdsval	$⊢ φ \to P = (\{⟨{Base}_{ndx}, \underset{x \in dom R}{⨉} {Base}_{R (x)}⟩, ⟨+_{ndx}, (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f (x) +_{R (x)} g (x)))⟩, ⟨\cdot_{ndx}, (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f (x) \cdot_{R (x)} g (x)))⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, (f \in {Base}_{S}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f \cdot_{R (x)} g (x)))⟩, ⟨\cdot_{𝑖} (ndx), (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))⟩\}) \cup (\{⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ R)⟩, ⟨\leq_{ndx}, \{⟨f, g⟩ \| (\{f, g\} \subseteq \underset{x \in dom R}{⨉} {Base}_{R (x)} \land \forall x \in dom R f (x) \leq_{R (x)} g (x))\}⟩, ⟨dist (ndx), (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ sup (ran (x \in dom R ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{*} <))⟩\} \cup \{⟨Hom (ndx), (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{⨉} (f (x) Hom (R (x)) g (x)))⟩, ⟨comp (ndx), (a \in (\underset{x \in dom R}{⨉} {Base}_{R (x)} \times \underset{x \in dom R}{⨉} {Base}_{R (x)}), c \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (d \in (c (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{⨉} (f (x) Hom (R (x)) g (x))) 2^{nd} (a)), e \in (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{⨉} (f (x) Hom (R (x)) g (x))) (a) ⟼ (x \in dom R ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))⟩\})$
17		eqid	$⊢ Scalar (P) = Scalar (P)$
18		scaid	$⊢ Scalar = Slot Scalar (ndx)$
19		snsstp1	$⊢ \{⟨Scalar (ndx), S⟩\} \subseteq \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, (f \in {Base}_{S}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f \cdot_{R (x)} g (x)))⟩, ⟨\cdot_{𝑖} (ndx), (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))⟩\}$
20		ssun2	$⊢ \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, (f \in {Base}_{S}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f \cdot_{R (x)} g (x)))⟩, ⟨\cdot_{𝑖} (ndx), (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))⟩\} \subseteq \{⟨{Base}_{ndx}, \underset{x \in dom R}{⨉} {Base}_{R (x)}⟩, ⟨+_{ndx}, (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f (x) +_{R (x)} g (x)))⟩, ⟨\cdot_{ndx}, (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f (x) \cdot_{R (x)} g (x)))⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, (f \in {Base}_{S}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f \cdot_{R (x)} g (x)))⟩, ⟨\cdot_{𝑖} (ndx), (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))⟩\}$
21	19 20	sstri	$⊢ \{⟨Scalar (ndx), S⟩\} \subseteq \{⟨{Base}_{ndx}, \underset{x \in dom R}{⨉} {Base}_{R (x)}⟩, ⟨+_{ndx}, (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f (x) +_{R (x)} g (x)))⟩, ⟨\cdot_{ndx}, (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f (x) \cdot_{R (x)} g (x)))⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, (f \in {Base}_{S}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f \cdot_{R (x)} g (x)))⟩, ⟨\cdot_{𝑖} (ndx), (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))⟩\}$
22		ssun1	$⊢ \{⟨{Base}_{ndx}, \underset{x \in dom R}{⨉} {Base}_{R (x)}⟩, ⟨+_{ndx}, (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f (x) +_{R (x)} g (x)))⟩, ⟨\cdot_{ndx}, (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f (x) \cdot_{R (x)} g (x)))⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, (f \in {Base}_{S}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f \cdot_{R (x)} g (x)))⟩, ⟨\cdot_{𝑖} (ndx), (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))⟩\} \subseteq (\{⟨{Base}_{ndx}, \underset{x \in dom R}{⨉} {Base}_{R (x)}⟩, ⟨+_{ndx}, (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f (x) +_{R (x)} g (x)))⟩, ⟨\cdot_{ndx}, (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f (x) \cdot_{R (x)} g (x)))⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, (f \in {Base}_{S}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f \cdot_{R (x)} g (x)))⟩, ⟨\cdot_{𝑖} (ndx), (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))⟩\}) \cup (\{⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ R)⟩, ⟨\leq_{ndx}, \{⟨f, g⟩ \| (\{f, g\} \subseteq \underset{x \in dom R}{⨉} {Base}_{R (x)} \land \forall x \in dom R f (x) \leq_{R (x)} g (x))\}⟩, ⟨dist (ndx), (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ sup (ran (x \in dom R ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{*} <))⟩\} \cup \{⟨Hom (ndx), (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{⨉} (f (x) Hom (R (x)) g (x)))⟩, ⟨comp (ndx), (a \in (\underset{x \in dom R}{⨉} {Base}_{R (x)} \times \underset{x \in dom R}{⨉} {Base}_{R (x)}), c \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (d \in (c (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{⨉} (f (x) Hom (R (x)) g (x))) 2^{nd} (a)), e \in (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{⨉} (f (x) Hom (R (x)) g (x))) (a) ⟼ (x \in dom R ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))⟩\})$
23	21 22	sstri	$⊢ \{⟨Scalar (ndx), S⟩\} \subseteq (\{⟨{Base}_{ndx}, \underset{x \in dom R}{⨉} {Base}_{R (x)}⟩, ⟨+_{ndx}, (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f (x) +_{R (x)} g (x)))⟩, ⟨\cdot_{ndx}, (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f (x) \cdot_{R (x)} g (x)))⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, (f \in {Base}_{S}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (x \in dom R ⟼ f \cdot_{R (x)} g (x)))⟩, ⟨\cdot_{𝑖} (ndx), (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))⟩\}) \cup (\{⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ R)⟩, ⟨\leq_{ndx}, \{⟨f, g⟩ \| (\{f, g\} \subseteq \underset{x \in dom R}{⨉} {Base}_{R (x)} \land \forall x \in dom R f (x) \leq_{R (x)} g (x))\}⟩, ⟨dist (ndx), (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ sup (ran (x \in dom R ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{*} <))⟩\} \cup \{⟨Hom (ndx), (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{⨉} (f (x) Hom (R (x)) g (x)))⟩, ⟨comp (ndx), (a \in (\underset{x \in dom R}{⨉} {Base}_{R (x)} \times \underset{x \in dom R}{⨉} {Base}_{R (x)}), c \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ (d \in (c (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{⨉} (f (x) Hom (R (x)) g (x))) 2^{nd} (a)), e \in (f \in \underset{x \in dom R}{⨉} {Base}_{R (x)}, g \in \underset{x \in dom R}{⨉} {Base}_{R (x)} ⟼ \underset{x \in dom R}{⨉} (f (x) Hom (R (x)) g (x))) (a) ⟼ (x \in dom R ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))⟩\})$
24	16 17 18 2 23	prdsvallem	$⊢ φ \to Scalar (P) = S$
25	24	eqcomd	$⊢ φ \to S = Scalar (P)$

Metamath Proof Explorer

Theorem prdssca

Proof