Theorem spansnji

Description: The subspace sum of a closed subspace and a one-dimensional subspace equals their join. (Proof suggested by Eric Schechter 1-Jun-2004.) (Contributed by NM, 1-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	spansnj.1	⊢ 𝐴 ∈ Cℋ
	spansnj.2	⊢ 𝐵 ∈ ℋ
Assertion	spansnji	⊢ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) = ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) )

Proof

Step	Hyp	Ref	Expression
1		spansnj.1	⊢ 𝐴 ∈ Cℋ
2		spansnj.2	⊢ 𝐵 ∈ ℋ
3	1	chshii	⊢ 𝐴 ∈ Sℋ
4	2	spansnchi	⊢ ( span ‘ { 𝐵 } ) ∈ Cℋ
5	4	chshii	⊢ ( span ‘ { 𝐵 } ) ∈ Sℋ
6	3 5	shjshsi	⊢ ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) ) )
7	1	chssii	⊢ 𝐴 ⊆ ℋ
8	1	choccli	⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
9	8 2	pjhclii	⊢ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ∈ ℋ
10		snssi	⊢ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ∈ ℋ → { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ⊆ ℋ )
11	9 10	ax-mp	⊢ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ⊆ ℋ
12	7 11	spanuni	⊢ ( span ‘ ( 𝐴 ∪ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) = ( ( span ‘ 𝐴 ) +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )
13		spanid	⊢ ( 𝐴 ∈ Sℋ → ( span ‘ 𝐴 ) = 𝐴 )
14	3 13	ax-mp	⊢ ( span ‘ 𝐴 ) = 𝐴
15	14	oveq1i	⊢ ( ( span ‘ 𝐴 ) +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) = ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )
16	7 2	spansnpji	⊢ 𝐴 ⊆ ( ⊥ ‘ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )
17	9	spansnchi	⊢ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ∈ Cℋ
18	1 17	osumi	⊢ ( 𝐴 ⊆ ( ⊥ ‘ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) → ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) = ( 𝐴 ∨ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) )
19	16 18	ax-mp	⊢ ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) = ( 𝐴 ∨ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )
20	12 15 19	3eqtrri	⊢ ( 𝐴 ∨ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) = ( span ‘ ( 𝐴 ∪ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )
21	1 2	spanunsni	⊢ ( span ‘ ( 𝐴 ∪ { 𝐵 } ) ) = ( span ‘ ( 𝐴 ∪ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )
22	20 21	eqtr4i	⊢ ( 𝐴 ∨ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) = ( span ‘ ( 𝐴 ∪ { 𝐵 } ) )
23		snssi	⊢ ( 𝐵 ∈ ℋ → { 𝐵 } ⊆ ℋ )
24	2 23	ax-mp	⊢ { 𝐵 } ⊆ ℋ
25	7 24	spanuni	⊢ ( span ‘ ( 𝐴 ∪ { 𝐵 } ) ) = ( ( span ‘ 𝐴 ) +ℋ ( span ‘ { 𝐵 } ) )
26	14	oveq1i	⊢ ( ( span ‘ 𝐴 ) +ℋ ( span ‘ { 𝐵 } ) ) = ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) )
27	22 25 26	3eqtrri	⊢ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) = ( 𝐴 ∨ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )
28	1 17	chjcli	⊢ ( 𝐴 ∨ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) ∈ Cℋ
29	27 28	eqeltri	⊢ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) ∈ Cℋ
30	29	ococi	⊢ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) ) ) = ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) )
31	6 30	eqtr2i	⊢ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) = ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) )