srasca

Description: The set of scalars of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 4-Oct-2015) (Revised by Thierry Arnoux, 16-Jun-2019) (Proof shortened by AV, 12-Nov-2024)

	Ref	Expression
Hypotheses	srapart.a	$⊢ φ \to A = subringAlg (W) (S)$
	srapart.s	$⊢ φ \to S \subseteq {Base}_{W}$
Assertion	srasca	$⊢ φ \to W ↾_{𝑠} S = Scalar (A)$

Proof

Step	Hyp	Ref	Expression
1		srapart.a	$⊢ φ \to A = subringAlg (W) (S)$
2		srapart.s	$⊢ φ \to S \subseteq {Base}_{W}$
3		scaid	$⊢ Scalar = Slot Scalar (ndx)$
4		vscandxnscandx	$⊢ \cdot_{ndx} \neq Scalar (ndx)$
5	4	necomi	$⊢ Scalar (ndx) \neq \cdot_{ndx}$
6	3 5	setsnid	$⊢ Scalar (W sSet ⟨Scalar (ndx), W ↾_{𝑠} S⟩) = Scalar ((W sSet ⟨Scalar (ndx), W ↾_{𝑠} S⟩) sSet ⟨\cdot_{ndx}, \cdot_{W}⟩)$
7		slotsdifipndx	$⊢ (\cdot_{ndx} \neq \cdot_{𝑖} (ndx) \land Scalar (ndx) \neq \cdot_{𝑖} (ndx))$
8	7	simpri	$⊢ Scalar (ndx) \neq \cdot_{𝑖} (ndx)$
9	3 8	setsnid	$⊢ Scalar ((W sSet ⟨Scalar (ndx), W ↾_{𝑠} S⟩) sSet ⟨\cdot_{ndx}, \cdot_{W}⟩) = Scalar (((W sSet ⟨Scalar (ndx), W ↾_{𝑠} S⟩) sSet ⟨\cdot_{ndx}, \cdot_{W}⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{W}⟩)$
10	6 9	eqtri	$⊢ Scalar (W sSet ⟨Scalar (ndx), W ↾_{𝑠} S⟩) = Scalar (((W sSet ⟨Scalar (ndx), W ↾_{𝑠} S⟩) sSet ⟨\cdot_{ndx}, \cdot_{W}⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{W}⟩)$
11		ovexd	$⊢ φ \to W ↾_{𝑠} S \in V$
12	3	setsid	$⊢ (W \in V \land W ↾_{𝑠} S \in V) \to W ↾_{𝑠} S = Scalar (W sSet ⟨Scalar (ndx), W ↾_{𝑠} S⟩)$
13	11 12	sylan2	$⊢ (W \in V \land φ) \to W ↾_{𝑠} S = Scalar (W sSet ⟨Scalar (ndx), W ↾_{𝑠} S⟩)$
14	1	adantl	$⊢ (W \in V \land φ) \to A = subringAlg (W) (S)$
15		sraval	$⊢ (W \in V \land S \subseteq {Base}_{W}) \to subringAlg (W) (S) = ((W sSet ⟨Scalar (ndx), W ↾_{𝑠} S⟩) sSet ⟨\cdot_{ndx}, \cdot_{W}⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{W}⟩$
16	2 15	sylan2	$⊢ (W \in V \land φ) \to subringAlg (W) (S) = ((W sSet ⟨Scalar (ndx), W ↾_{𝑠} S⟩) sSet ⟨\cdot_{ndx}, \cdot_{W}⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{W}⟩$
17	14 16	eqtrd	$⊢ (W \in V \land φ) \to A = ((W sSet ⟨Scalar (ndx), W ↾_{𝑠} S⟩) sSet ⟨\cdot_{ndx}, \cdot_{W}⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{W}⟩$
18	17	fveq2d	$⊢ (W \in V \land φ) \to Scalar (A) = Scalar (((W sSet ⟨Scalar (ndx), W ↾_{𝑠} S⟩) sSet ⟨\cdot_{ndx}, \cdot_{W}⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{W}⟩)$
19	10 13 18	3eqtr4a	$⊢ (W \in V \land φ) \to W ↾_{𝑠} S = Scalar (A)$
20	3	str0	$⊢ \emptyset = Scalar (\emptyset)$
21		reldmress	$⊢ Rel dom ↾_{𝑠}$
22	21	ovprc1	$⊢ \neg W \in V \to W ↾_{𝑠} S = \emptyset$
23	22	adantr	$⊢ (\neg W \in V \land φ) \to W ↾_{𝑠} S = \emptyset$
24		fv2prc	$⊢ \neg W \in V \to subringAlg (W) (S) = \emptyset$
25	1 24	sylan9eqr	$⊢ (\neg W \in V \land φ) \to A = \emptyset$
26	25	fveq2d	$⊢ (\neg W \in V \land φ) \to Scalar (A) = Scalar (\emptyset)$
27	20 23 26	3eqtr4a	$⊢ (\neg W \in V \land φ) \to W ↾_{𝑠} S = Scalar (A)$
28	19 27	pm2.61ian	$⊢ φ \to W ↾_{𝑠} S = Scalar (A)$

Metamath Proof Explorer

Theorem srasca

Proof