Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
srapart.s ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
Assertion srasca ( 𝜑 → ( 𝑊 ↾s 𝑆 ) = ( Scalar ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 srapart.a ⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
2 srapart.s ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
3 scaid ⊢ Scalar = Slot ( Scalar ‘ ndx )
4 vscandxnscandx ⊢ ( ·𝑠 ‘ ndx ) ≠ ( Scalar ‘ ndx )
5 4 necomi ⊢ ( Scalar ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
6 3 5 setsnid ⊢ ( Scalar ‘ ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) ) = ( Scalar ‘ ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
7 slotsdifipndx ⊢ ( ( ·𝑠 ‘ ndx ) ≠ ( ·𝑖 ‘ ndx ) ∧ ( Scalar ‘ ndx ) ≠ ( ·𝑖 ‘ ndx ) )
8 7 simpri ⊢ ( Scalar ‘ ndx ) ≠ ( ·𝑖 ‘ ndx )
9 3 8 setsnid ⊢ ( Scalar ‘ ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) ) = ( Scalar ‘ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
10 6 9 eqtri ⊢ ( Scalar ‘ ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) ) = ( Scalar ‘ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
11 ovexd ⊢ ( 𝜑 → ( 𝑊 ↾s 𝑆 ) ∈ V )
12 3 setsid ⊢ ( ( 𝑊 ∈ V ∧ ( 𝑊 ↾s 𝑆 ) ∈ V ) → ( 𝑊 ↾s 𝑆 ) = ( Scalar ‘ ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) ) )
13 11 12 sylan2 ⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → ( 𝑊 ↾s 𝑆 ) = ( Scalar ‘ ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) ) )
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 ∧ 𝜑 ) → ( Scalar ‘ 𝐴 ) = ( Scalar ‘ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) ) )
19 10 13 18 3eqtr4a ⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → ( 𝑊 ↾s 𝑆 ) = ( Scalar ‘ 𝐴 ) )
20 3 str0 ⊢ ∅ = ( Scalar ‘ ∅ )
21 reldmress ⊢ Rel dom ↾s
22 21 ovprc1 ⊢ ( ¬ 𝑊 ∈ V → ( 𝑊 ↾s 𝑆 ) = ∅ )
23 22 adantr ⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → ( 𝑊 ↾s 𝑆 ) = ∅ )
24 fv2prc ⊢ ( ¬ 𝑊 ∈ V → ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) = ∅ )
25 1 24 sylan9eqr ⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → 𝐴 = ∅ )
26 25 fveq2d ⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → ( Scalar ‘ 𝐴 ) = ( Scalar ‘ ∅ ) )
27 20 23 26 3eqtr4a ⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → ( 𝑊 ↾s 𝑆 ) = ( Scalar ‘ 𝐴 ) )
28 19 27 pm2.61ian ⊢ ( 𝜑 → ( 𝑊 ↾s 𝑆 ) = ( Scalar ‘ 𝐴 ) )