sralem

Description: Lemma for srabase and similar theorems. (Contributed by Mario Carneiro, 4-Oct-2015) (Revised by Thierry Arnoux, 16-Jun-2019) (Revised by AV, 29-Oct-2024)

	Ref	Expression
Hypotheses	srapart.a	$⊢ φ \to A = subringAlg (W) (S)$
	srapart.s	$⊢ φ \to S \subseteq {Base}_{W}$
	sralem.1	$⊢ E = Slot E (ndx)$
	sralem.2	$⊢ Scalar (ndx) \neq E (ndx)$
	sralem.3	$⊢ \cdot_{ndx} \neq E (ndx)$
	sralem.4	$⊢ \cdot_{𝑖} (ndx) \neq E (ndx)$
Assertion	sralem	$⊢ φ \to E (W) = E (A)$

Proof

Step	Hyp	Ref	Expression
1		srapart.a	$⊢ φ \to A = subringAlg (W) (S)$
2		srapart.s	$⊢ φ \to S \subseteq {Base}_{W}$
3		sralem.1	$⊢ E = Slot E (ndx)$
4		sralem.2	$⊢ Scalar (ndx) \neq E (ndx)$
5		sralem.3	$⊢ \cdot_{ndx} \neq E (ndx)$
6		sralem.4	$⊢ \cdot_{𝑖} (ndx) \neq E (ndx)$
7	4	necomi	$⊢ E (ndx) \neq Scalar (ndx)$
8	3 7	setsnid	$⊢ E (W) = E (W sSet ⟨Scalar (ndx), W ↾_{𝑠} S⟩)$
9	5	necomi	$⊢ E (ndx) \neq \cdot_{ndx}$
10	3 9	setsnid	$⊢ E (W sSet ⟨Scalar (ndx), W ↾_{𝑠} S⟩) = E ((W sSet ⟨Scalar (ndx), W ↾_{𝑠} S⟩) sSet ⟨\cdot_{ndx}, \cdot_{W}⟩)$
11	6	necomi	$⊢ E (ndx) \neq \cdot_{𝑖} (ndx)$
12	3 11	setsnid	$⊢ E ((W sSet ⟨Scalar (ndx), W ↾_{𝑠} S⟩) sSet ⟨\cdot_{ndx}, \cdot_{W}⟩) = E (((W sSet ⟨Scalar (ndx), W ↾_{𝑠} S⟩) sSet ⟨\cdot_{ndx}, \cdot_{W}⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{W}⟩)$
13	8 10 12	3eqtri	$⊢ E (W) = E (((W sSet ⟨Scalar (ndx), W ↾_{𝑠} S⟩) sSet ⟨\cdot_{ndx}, \cdot_{W}⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{W}⟩)$
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 E (A) = E (((W sSet ⟨Scalar (ndx), W ↾_{𝑠} S⟩) sSet ⟨\cdot_{ndx}, \cdot_{W}⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{W}⟩)$
19	13 18	eqtr4id	$⊢ (W \in V \land φ) \to E (W) = E (A)$
20	3	str0	$⊢ \emptyset = E (\emptyset)$
21		fvprc	$⊢ \neg W \in V \to E (W) = \emptyset$
22	21	adantr	$⊢ (\neg W \in V \land φ) \to E (W) = \emptyset$
23		fv2prc	$⊢ \neg W \in V \to subringAlg (W) (S) = \emptyset$
24	1 23	sylan9eqr	$⊢ (\neg W \in V \land φ) \to A = \emptyset$
25	24	fveq2d	$⊢ (\neg W \in V \land φ) \to E (A) = E (\emptyset)$
26	20 22 25	3eqtr4a	$⊢ (\neg W \in V \land φ) \to E (W) = E (A)$
27	19 26	pm2.61ian	$⊢ φ \to E (W) = E (A)$

Metamath Proof Explorer

Theorem sralem

Proof