Theorem shscom

Description: Commutative law for subspace sum. (Contributed by NM, 15-Dec-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	shscom	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 +ℋ 𝐵 ) = ( 𝐵 +ℋ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		shel	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℋ )
2		shel	⊢ ( ( 𝐵 ∈ Sℋ ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ ℋ )
3	1 2	anim12i	⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐵 ∈ Sℋ ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) )
4	3	an4s	⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) )
5		ax-hvcom	⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑦 +ℎ 𝑧 ) = ( 𝑧 +ℎ 𝑦 ) )
6	4 5	syl	⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 +ℎ 𝑧 ) = ( 𝑧 +ℎ 𝑦 ) )
7	6	eqeq2d	⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) ↔ 𝑥 = ( 𝑧 +ℎ 𝑦 ) ) )
8	7	2rexbidva	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 +ℎ 𝑧 ) ↔ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑧 +ℎ 𝑦 ) ) )
9		rexcom	⊢ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑧 +ℎ 𝑦 ) ↔ ∃ 𝑧 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝑧 +ℎ 𝑦 ) )
10	8 9	bitrdi	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 +ℎ 𝑧 ) ↔ ∃ 𝑧 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝑧 +ℎ 𝑦 ) ) )
11		shsel	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 +ℎ 𝑧 ) ) )
12		shsel	⊢ ( ( 𝐵 ∈ Sℋ ∧ 𝐴 ∈ Sℋ ) → ( 𝑥 ∈ ( 𝐵 +ℋ 𝐴 ) ↔ ∃ 𝑧 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝑧 +ℎ 𝑦 ) ) )
13	12	ancoms	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝑥 ∈ ( 𝐵 +ℋ 𝐴 ) ↔ ∃ 𝑧 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝑧 +ℎ 𝑦 ) ) )
14	10 11 13	3bitr4d	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ↔ 𝑥 ∈ ( 𝐵 +ℋ 𝐴 ) ) )
15	14	eqrdv	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 +ℋ 𝐵 ) = ( 𝐵 +ℋ 𝐴 ) )