Metamath Proof Explorer

Theorem 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 ⊢ φ → A = subringAlg ⁡ W ⁡ S
srapart.s ⊢ φ → S ⊆ Base W
sralem.1 ⊢ E = Slot E ⁡ ndx
sralem.2 ⊢ Scalar ⁡ ndx ≠ E ⁡ ndx
sralem.3 ⊢ ⋅ ndx ≠ E ⁡ ndx
sralem.4 ⊢ ⋅ 𝑖 ⁡ ndx ≠ E ⁡ ndx
Assertion sralem ⊢ φ → E ⁡ W = E ⁡ A

Proof

Step Hyp Ref Expression
1 srapart.a ⊢ φ → A = subringAlg ⁡ W ⁡ S
2 srapart.s ⊢ φ → S ⊆ Base W
3 sralem.1 ⊢ E = Slot E ⁡ ndx
4 sralem.2 ⊢ Scalar ⁡ ndx ≠ E ⁡ ndx
5 sralem.3 ⊢ ⋅ ndx ≠ E ⁡ ndx
6 sralem.4 ⊢ ⋅ 𝑖 ⁡ ndx ≠ E ⁡ ndx
7 4 necomi ⊢ E ⁡ ndx ≠ Scalar ⁡ ndx
8 3 7 setsnid ⊢ E ⁡ W = E ⁡ W sSet Scalar ⁡ ndx W ↾ 𝑠 S
9 5 necomi ⊢ E ⁡ ndx ≠ ⋅ ndx
10 3 9 setsnid ⊢ E ⁡ W sSet Scalar ⁡ ndx W ↾ 𝑠 S = E ⁡ W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W
11 6 necomi ⊢ E ⁡ ndx ≠ ⋅ 𝑖 ⁡ ndx
12 3 11 setsnid ⊢ E ⁡ W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W = E ⁡ W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
13 8 10 12 3eqtri ⊢ E ⁡ W = E ⁡ W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
14 1 adantl ⊢ W ∈ V ∧ φ → A = subringAlg ⁡ W ⁡ S
15 sraval ⊢ W ∈ V ∧ S ⊆ Base W → subringAlg ⁡ W ⁡ S = W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
16 2 15 sylan2 ⊢ W ∈ V ∧ φ → subringAlg ⁡ W ⁡ S = W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
17 14 16 eqtrd ⊢ W ∈ V ∧ φ → A = W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
18 17 fveq2d ⊢ W ∈ V ∧ φ → E ⁡ A = E ⁡ W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
19 13 18 eqtr4id ⊢ W ∈ V ∧ φ → E ⁡ W = E ⁡ A
20 3 str0 ⊢ ∅ = E ⁡ ∅
21 fvprc ⊢ ¬ W ∈ V → E ⁡ W = ∅
22 21 adantr ⊢ ¬ W ∈ V ∧ φ → E ⁡ W = ∅
23 fv2prc ⊢ ¬ W ∈ V → subringAlg ⁡ W ⁡ S = ∅
24 1 23 sylan9eqr ⊢ ¬ W ∈ V ∧ φ → A = ∅
25 24 fveq2d ⊢ ¬ W ∈ V ∧ φ → E ⁡ A = E ⁡ ∅
26 20 22 25 3eqtr4a ⊢ ¬ W ∈ V ∧ φ → E ⁡ W = E ⁡ A
27 19 26 pm2.61ian ⊢ φ → E ⁡ W = E ⁡ A