This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝑖 ∈ 𝑋 ↦ 𝑌 ) ) )