Theorem drgextgsum

Description: Group sum in a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023)

	Ref	Expression
Hypotheses	drgext.b	⊢ 𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 )
	drgext.1	⊢ ( 𝜑 → 𝐸 ∈ DivRing )
	drgext.2	⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝐸 ) )
	drgext.f	⊢ 𝐹 = ( 𝐸 ↾s 𝑈 )
	drgext.3	⊢ ( 𝜑 → 𝐹 ∈ DivRing )
	drgextgsum.1	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	drgextgsum	⊢ ( 𝜑 → ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ 𝑌 ) ) = ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		drgext.b	⊢ 𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 )
2		drgext.1	⊢ ( 𝜑 → 𝐸 ∈ DivRing )
3		drgext.2	⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝐸 ) )
4		drgext.f	⊢ 𝐹 = ( 𝐸 ↾s 𝑈 )
5		drgext.3	⊢ ( 𝜑 → 𝐹 ∈ DivRing )
6		drgextgsum.1	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
7	6	mptexd	⊢ ( 𝜑 → ( 𝑖 ∈ 𝑋 ↦ 𝑌 ) ∈ V )
8	1 4	sralvec	⊢ ( ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ ( SubRing ‘ 𝐸 ) ) → 𝐵 ∈ LVec )
9	2 5 3 8	syl3anc	⊢ ( 𝜑 → 𝐵 ∈ LVec )
10		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
11	10	subrgss	⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → 𝑈 ⊆ ( Base ‘ 𝐸 ) )
12	3 11	syl	⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ 𝐸 ) )
13	1 7 2 9 12	gsumsra	⊢ ( 𝜑 → ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ 𝑌 ) ) = ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ 𝑌 ) ) )