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

Metamath Proof Explorer

Theorem lsmvalx

Description: Subspace sum value (for a group or vector space). Extended domain version of lsmval . (Contributed by NM, 28-Jan-2014) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses lsmfval.v ⊢ 𝐵 = ( Base ‘ 𝐺 )
lsmfval.a ⊢ + = ( +g ‘ 𝐺 )
lsmfval.s ⊢ ⊕ = ( LSSum ‘ 𝐺 )
Assertion lsmvalx ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑇 ⊕ 𝑈 ) = ran ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 + 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 lsmfval.v ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 lsmfval.a ⊢ + = ( +g ‘ 𝐺 )
3 lsmfval.s ⊢ ⊕ = ( LSSum ‘ 𝐺 )
4 1 2 3 lsmfval ⊢ ( 𝐺 ∈ 𝑉 → ⊕ = ( 𝑡 ∈ 𝒫 𝐵 , 𝑢 ∈ 𝒫 𝐵 ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 + 𝑦 ) ) ) )
5 4 oveqd ⊢ ( 𝐺 ∈ 𝑉 → ( 𝑇 ⊕ 𝑈 ) = ( 𝑇 ( 𝑡 ∈ 𝒫 𝐵 , 𝑢 ∈ 𝒫 𝐵 ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 + 𝑦 ) ) ) 𝑈 ) )
6 1 fvexi ⊢ 𝐵 ∈ V
7 6 elpw2 ⊢ ( 𝑇 ∈ 𝒫 𝐵 ↔ 𝑇 ⊆ 𝐵 )
8 6 elpw2 ⊢ ( 𝑈 ∈ 𝒫 𝐵 ↔ 𝑈 ⊆ 𝐵 )
9 mpoexga ⊢ ( ( 𝑇 ∈ 𝒫 𝐵 ∧ 𝑈 ∈ 𝒫 𝐵 ) → ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 + 𝑦 ) ) ∈ V )
10 rnexg ⊢ ( ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 + 𝑦 ) ) ∈ V → ran ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 + 𝑦 ) ) ∈ V )
11 9 10 syl ⊢ ( ( 𝑇 ∈ 𝒫 𝐵 ∧ 𝑈 ∈ 𝒫 𝐵 ) → ran ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 + 𝑦 ) ) ∈ V )
12 mpoeq12 ⊢ ( ( 𝑡 = 𝑇 ∧ 𝑢 = 𝑈 ) → ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 + 𝑦 ) ) = ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 + 𝑦 ) ) )
13 12 rneqd ⊢ ( ( 𝑡 = 𝑇 ∧ 𝑢 = 𝑈 ) → ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 + 𝑦 ) ) = ran ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 + 𝑦 ) ) )
14 eqid ⊢ ( 𝑡 ∈ 𝒫 𝐵 , 𝑢 ∈ 𝒫 𝐵 ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 + 𝑦 ) ) ) = ( 𝑡 ∈ 𝒫 𝐵 , 𝑢 ∈ 𝒫 𝐵 ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 + 𝑦 ) ) )
15 13 14 ovmpoga ⊢ ( ( 𝑇 ∈ 𝒫 𝐵 ∧ 𝑈 ∈ 𝒫 𝐵 ∧ ran ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 + 𝑦 ) ) ∈ V ) → ( 𝑇 ( 𝑡 ∈ 𝒫 𝐵 , 𝑢 ∈ 𝒫 𝐵 ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 + 𝑦 ) ) ) 𝑈 ) = ran ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 + 𝑦 ) ) )
16 11 15 mpd3an3 ⊢ ( ( 𝑇 ∈ 𝒫 𝐵 ∧ 𝑈 ∈ 𝒫 𝐵 ) → ( 𝑇 ( 𝑡 ∈ 𝒫 𝐵 , 𝑢 ∈ 𝒫 𝐵 ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 + 𝑦 ) ) ) 𝑈 ) = ran ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 + 𝑦 ) ) )
17 7 8 16 syl2anbr ⊢ ( ( 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑇 ( 𝑡 ∈ 𝒫 𝐵 , 𝑢 ∈ 𝒫 𝐵 ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 + 𝑦 ) ) ) 𝑈 ) = ran ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 + 𝑦 ) ) )
18 5 17 sylan9eq ⊢ ( ( 𝐺 ∈ 𝑉 ∧ ( 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ) → ( 𝑇 ⊕ 𝑈 ) = ran ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 + 𝑦 ) ) )
19 18 3impb ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑇 ⊕ 𝑈 ) = ran ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 + 𝑦 ) ) )