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 ⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
srapart.s ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
sralem.1 ⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
sralem.2 ⊢ ( Scalar ‘ ndx ) ≠ ( 𝐸 ‘ ndx )
sralem.3 ⊢ ( ·𝑠 ‘ ndx ) ≠ ( 𝐸 ‘ ndx )
sralem.4 ⊢ ( ·𝑖 ‘ ndx ) ≠ ( 𝐸 ‘ ndx )
Assertion sralem ( 𝜑 → ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 srapart.a ⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
2 srapart.s ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
3 sralem.1 ⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
4 sralem.2 ⊢ ( Scalar ‘ ndx ) ≠ ( 𝐸 ‘ ndx )
5 sralem.3 ⊢ ( ·𝑠 ‘ ndx ) ≠ ( 𝐸 ‘ ndx )
6 sralem.4 ⊢ ( ·𝑖 ‘ ndx ) ≠ ( 𝐸 ‘ ndx )
7 4 necomi ⊢ ( 𝐸 ‘ ndx ) ≠ ( Scalar ‘ ndx )
8 3 7 setsnid ⊢ ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) )
9 5 necomi ⊢ ( 𝐸 ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
10 3 9 setsnid ⊢ ( 𝐸 ‘ ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) ) = ( 𝐸 ‘ ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
11 6 necomi ⊢ ( 𝐸 ‘ ndx ) ≠ ( ·𝑖 ‘ ndx )
12 3 11 setsnid ⊢ ( 𝐸 ‘ ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) ) = ( 𝐸 ‘ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
13 8 10 12 3eqtri ⊢ ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
14 1 adantl ⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
15 sraval ⊢ ( ( 𝑊 ∈ V ∧ 𝑆 ⊆ ( Base ‘ 𝑊 ) ) → ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
16 2 15 sylan2 ⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
17 14 16 eqtrd ⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → 𝐴 = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
18 17 fveq2d ⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → ( 𝐸 ‘ 𝐴 ) = ( 𝐸 ‘ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) ) )
19 13 18 eqtr4id ⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ 𝐴 ) )
20 3 str0 ⊢ ∅ = ( 𝐸 ‘ ∅ )
21 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑊 ) = ∅ )
22 21 adantr ⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → ( 𝐸 ‘ 𝑊 ) = ∅ )
23 fv2prc ⊢ ( ¬ 𝑊 ∈ V → ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) = ∅ )
24 1 23 sylan9eqr ⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → 𝐴 = ∅ )
25 24 fveq2d ⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → ( 𝐸 ‘ 𝐴 ) = ( 𝐸 ‘ ∅ ) )
26 20 22 25 3eqtr4a ⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ 𝐴 ) )
27 19 26 pm2.61ian ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ 𝐴 ) )