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 ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 + 𝑦 ) ) )