Theorem shsval3i

Description: An alternate way to express subspace sum. (Contributed by NM, 25-Nov-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	shlesb1.1	⊢ 𝐴 ∈ Sℋ
	shlesb1.2	⊢ 𝐵 ∈ Sℋ
Assertion	shsval3i	⊢ ( 𝐴 +ℋ 𝐵 ) = ( span ‘ ( 𝐴 ∪ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		shlesb1.1	⊢ 𝐴 ∈ Sℋ
2		shlesb1.2	⊢ 𝐵 ∈ Sℋ
3	1 2	shsval2i	⊢ ( 𝐴 +ℋ 𝐵 ) = ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 }
4	1	shssii	⊢ 𝐴 ⊆ ℋ
5	2	shssii	⊢ 𝐵 ⊆ ℋ
6	4 5	unssi	⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ℋ
7		spanval	⊢ ( ( 𝐴 ∪ 𝐵 ) ⊆ ℋ → ( span ‘ ( 𝐴 ∪ 𝐵 ) ) = ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } )
8	6 7	ax-mp	⊢ ( span ‘ ( 𝐴 ∪ 𝐵 ) ) = ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 }
9	3 8	eqtr4i	⊢ ( 𝐴 +ℋ 𝐵 ) = ( span ‘ ( 𝐴 ∪ 𝐵 ) )