Theorem shsval2i

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	shsval2i	⊢ ( 𝐴 +ℋ 𝐵 ) = ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 }

Proof

Step	Hyp	Ref	Expression
1		shlesb1.1	⊢ 𝐴 ∈ Sℋ
2		shlesb1.2	⊢ 𝐵 ∈ Sℋ
3		ssun1	⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
4		ssintub	⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 }
5	3 4	sstri	⊢ 𝐴 ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 }
6		ssun2	⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
7	6 4	sstri	⊢ 𝐵 ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 }
8	5 7	pm3.2i	⊢ ( 𝐴 ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ∧ 𝐵 ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } )
9		ssrab2	⊢ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ⊆ Sℋ
10	1 2	shscli	⊢ ( 𝐴 +ℋ 𝐵 ) ∈ Sℋ
11	1 2	shunssi	⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 )
12		sseq2	⊢ ( 𝑥 = ( 𝐴 +ℋ 𝐵 ) → ( ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 ↔ ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) ) )
13	12	rspcev	⊢ ( ( ( 𝐴 +ℋ 𝐵 ) ∈ Sℋ ∧ ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) ) → ∃ 𝑥 ∈ Sℋ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 )
14	10 11 13	mp2an	⊢ ∃ 𝑥 ∈ Sℋ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥
15		rabn0	⊢ ( { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ≠ ∅ ↔ ∃ 𝑥 ∈ Sℋ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 )
16	14 15	mpbir	⊢ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ≠ ∅
17		shintcl	⊢ ( ( { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ⊆ Sℋ ∧ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ≠ ∅ ) → ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ∈ Sℋ )
18	9 16 17	mp2an	⊢ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ∈ Sℋ
19	1 2 18	shslubi	⊢ ( ( 𝐴 ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ∧ 𝐵 ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ) ↔ ( 𝐴 +ℋ 𝐵 ) ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } )
20	8 19	mpbi	⊢ ( 𝐴 +ℋ 𝐵 ) ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 }
21	12	elrab	⊢ ( ( 𝐴 +ℋ 𝐵 ) ∈ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ↔ ( ( 𝐴 +ℋ 𝐵 ) ∈ Sℋ ∧ ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) ) )
22	10 11 21	mpbir2an	⊢ ( 𝐴 +ℋ 𝐵 ) ∈ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 }
23		intss1	⊢ ( ( 𝐴 +ℋ 𝐵 ) ∈ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } → ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ⊆ ( 𝐴 +ℋ 𝐵 ) )
24	22 23	ax-mp	⊢ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ⊆ ( 𝐴 +ℋ 𝐵 )
25	20 24	eqssi	⊢ ( 𝐴 +ℋ 𝐵 ) = ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 }