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)

	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		5re	⊢ 5 ∈ ℝ
5		5lt6	⊢ 5 < 6
6	4 5	ltneii	⊢ 5 ≠ 6
7		scandx	⊢ ( Scalar ‘ ndx ) = 5
8		vscandx	⊢ ( ·𝑠 ‘ ndx ) = 6
9	7 8	neeq12i	⊢ ( ( Scalar ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ↔ 5 ≠ 6 )
10	6 9	mpbir	⊢ ( Scalar ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
11	3 10	setsnid	⊢ ( Scalar ‘ ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) ) = ( Scalar ‘ ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
12		5lt8	⊢ 5 < 8
13	4 12	ltneii	⊢ 5 ≠ 8
14		ipndx	⊢ ( ·𝑖 ‘ ndx ) = 8
15	7 14	neeq12i	⊢ ( ( Scalar ‘ ndx ) ≠ ( ·𝑖 ‘ ndx ) ↔ 5 ≠ 8 )
16	13 15	mpbir	⊢ ( Scalar ‘ ndx ) ≠ ( ·𝑖 ‘ ndx )
17	3 16	setsnid	⊢ ( Scalar ‘ ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) ) = ( Scalar ‘ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
18	11 17	eqtri	⊢ ( Scalar ‘ ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) ) = ( Scalar ‘ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
19		ovexd	⊢ ( 𝜑 → ( 𝑊 ↾s 𝑆 ) ∈ V )
20	3	setsid	⊢ ( ( 𝑊 ∈ V ∧ ( 𝑊 ↾s 𝑆 ) ∈ V ) → ( 𝑊 ↾s 𝑆 ) = ( Scalar ‘ ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) ) )
21	19 20	sylan2	⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → ( 𝑊 ↾s 𝑆 ) = ( Scalar ‘ ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) ) )
22	1	adantl	⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
23		sraval	⊢ ( ( 𝑊 ∈ V ∧ 𝑆 ⊆ ( Base ‘ 𝑊 ) ) → ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
24	2 23	sylan2	⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
25	22 24	eqtrd	⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → 𝐴 = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
26	25	fveq2d	⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → ( Scalar ‘ 𝐴 ) = ( Scalar ‘ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) ) )
27	18 21 26	3eqtr4a	⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → ( 𝑊 ↾s 𝑆 ) = ( Scalar ‘ 𝐴 ) )
28	3	str0	⊢ ∅ = ( Scalar ‘ ∅ )
29		reldmress	⊢ Rel dom ↾s
30	29	ovprc1	⊢ ( ¬ 𝑊 ∈ V → ( 𝑊 ↾s 𝑆 ) = ∅ )
31	30	adantr	⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → ( 𝑊 ↾s 𝑆 ) = ∅ )
32		fv2prc	⊢ ( ¬ 𝑊 ∈ V → ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) = ∅ )
33	1 32	sylan9eqr	⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → 𝐴 = ∅ )
34	33	fveq2d	⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → ( Scalar ‘ 𝐴 ) = ( Scalar ‘ ∅ ) )
35	28 31 34	3eqtr4a	⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → ( 𝑊 ↾s 𝑆 ) = ( Scalar ‘ 𝐴 ) )
36	27 35	pm2.61ian	⊢ ( 𝜑 → ( 𝑊 ↾s 𝑆 ) = ( Scalar ‘ 𝐴 ) )