Theorem shuni

Description: Two subspaces with trivial intersection have a unique decomposition of the elements of the subspace sum. (Contributed by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	shuni.1	$$⊢\phi \to H\in {\mathbf{S}}_{\mathscr{H}}$$
	shuni.2	$$⊢\phi \to K\in {\mathbf{S}}_{\mathscr{H}}$$
	shuni.3	$$⊢\phi \to H\cap K=0_{\mathscr{H}}$$
	shuni.4	$$⊢\phi \to A\in H$$
	shuni.5	$$⊢\phi \to B\in K$$
	shuni.6	$$⊢\phi \to C\in H$$
	shuni.7	$$⊢\phi \to D\in K$$
	shuni.8	$$⊢\phi \to A{+}_{ℎ}B=C{+}_{ℎ}D$$
Assertion	shuni	$$⊢\phi \to \left(A=C\wedge B=D\right)$$

Proof

Step	Hyp	Ref	Expression
1		shuni.1	$$⊢\phi \to H\in {\mathbf{S}}_{\mathscr{H}}$$
2		shuni.2	$$⊢\phi \to K\in {\mathbf{S}}_{\mathscr{H}}$$
3		shuni.3	$$⊢\phi \to H\cap K=0_{\mathscr{H}}$$
4		shuni.4	$$⊢\phi \to A\in H$$
5		shuni.5	$$⊢\phi \to B\in K$$
6		shuni.6	$$⊢\phi \to C\in H$$
7		shuni.7	$$⊢\phi \to D\in K$$
8		shuni.8	$$⊢\phi \to A{+}_{ℎ}B=C{+}_{ℎ}D$$
9		shsubcl	$$⊢\left(H\in {\mathbf{S}}_{\mathscr{H}}\wedge A\in H\wedge C\in H\right)\to A{-}_{ℎ}C\in H$$
10	1 4 6 9	syl3anc	$$⊢\phi \to A{-}_{ℎ}C\in H$$
11		shel	$$⊢\left(H\in {\mathbf{S}}_{\mathscr{H}}\wedge A\in H\right)\to A\in \mathscr{H}$$
12	1 4 11	syl2anc	$$⊢\phi \to A\in \mathscr{H}$$
13		shel	$$⊢\left(K\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in K\right)\to B\in \mathscr{H}$$
14	2 5 13	syl2anc	$$⊢\phi \to B\in \mathscr{H}$$
15		shel	$$⊢\left(H\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in H\right)\to C\in \mathscr{H}$$
16	1 6 15	syl2anc	$$⊢\phi \to C\in \mathscr{H}$$
17		shel	$$⊢\left(K\in {\mathbf{S}}_{\mathscr{H}}\wedge D\in K\right)\to D\in \mathscr{H}$$
18	2 7 17	syl2anc	$$⊢\phi \to D\in \mathscr{H}$$
19		hvaddsub4	$$⊢\left(\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\wedge \left(C\in \mathscr{H}\wedge D\in \mathscr{H}\right)\right)\to \left(A{+}_{ℎ}B=C{+}_{ℎ}D\leftrightarrow A{-}_{ℎ}C=D{-}_{ℎ}B\right)$$
20	12 14 16 18 19	syl22anc	$$⊢\phi \to \left(A{+}_{ℎ}B=C{+}_{ℎ}D\leftrightarrow A{-}_{ℎ}C=D{-}_{ℎ}B\right)$$
21	8 20	mpbid	$$⊢\phi \to A{-}_{ℎ}C=D{-}_{ℎ}B$$
22		shsubcl	$$⊢\left(K\in {\mathbf{S}}_{\mathscr{H}}\wedge D\in K\wedge B\in K\right)\to D{-}_{ℎ}B\in K$$
23	2 7 5 22	syl3anc	$$⊢\phi \to D{-}_{ℎ}B\in K$$
24	21 23	eqeltrd	$$⊢\phi \to A{-}_{ℎ}C\in K$$
25	10 24	elind	$$⊢\phi \to A{-}_{ℎ}C\in \left(H\cap K\right)$$
26	25 3	eleqtrd	$$⊢\phi \to A{-}_{ℎ}C\in 0_{\mathscr{H}}$$
27		elch0	$$⊢A{-}_{ℎ}C\in 0_{\mathscr{H}}\leftrightarrow A{-}_{ℎ}C=0_{ℎ}$$
28	26 27	sylib	$$⊢\phi \to A{-}_{ℎ}C=0_{ℎ}$$
29		hvsubeq0	$$⊢\left(A\in \mathscr{H}\wedge C\in \mathscr{H}\right)\to \left(A{-}_{ℎ}C=0_{ℎ}\leftrightarrow A=C\right)$$
30	12 16 29	syl2anc	$$⊢\phi \to \left(A{-}_{ℎ}C=0_{ℎ}\leftrightarrow A=C\right)$$
31	28 30	mpbid	$$⊢\phi \to A=C$$
32	21 28	eqtr3d	$$⊢\phi \to D{-}_{ℎ}B=0_{ℎ}$$
33		hvsubeq0	$$⊢\left(D\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to \left(D{-}_{ℎ}B=0_{ℎ}\leftrightarrow D=B\right)$$
34	18 14 33	syl2anc	$$⊢\phi \to \left(D{-}_{ℎ}B=0_{ℎ}\leftrightarrow D=B\right)$$
35	32 34	mpbid	$$⊢\phi \to D=B$$
36	35	eqcomd	$$⊢\phi \to B=D$$
37	31 36	jca	$$⊢\phi \to \left(A=C\wedge B=D\right)$$