pjds3i

Description: Vector decomposition into sum of projections on orthogonal subspaces. (Contributed by NM, 22-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjds3.1	$⊢ F \in C_{ℋ}$
	pjds3.2	$⊢ G \in C_{ℋ}$
	pjds3.3	$⊢ H \in C_{ℋ}$
Assertion	pjds3i	$⊢ ((A \in ((F \lor_{ℋ} G) \lor_{ℋ} H) \land F \subseteq ⊥ (G)) \land (F \subseteq ⊥ (H) \land G \subseteq ⊥ (H))) \to A = ({proj}_{ℎ} (F) (A) +_{ℎ} {proj}_{ℎ} (G) (A)) +_{ℎ} {proj}_{ℎ} (H) (A)$

Proof

Step	Hyp	Ref	Expression
1		pjds3.1	$⊢ F \in C_{ℋ}$
2		pjds3.2	$⊢ G \in C_{ℋ}$
3		pjds3.3	$⊢ H \in C_{ℋ}$
4		simpl	$⊢ (A \in ((F \lor_{ℋ} G) \lor_{ℋ} H) \land F \subseteq ⊥ (G)) \to A \in ((F \lor_{ℋ} G) \lor_{ℋ} H)$
5	3	choccli	$⊢ ⊥ (H) \in C_{ℋ}$
6	1 2 5	chlubii	$⊢ (F \subseteq ⊥ (H) \land G \subseteq ⊥ (H)) \to F \lor_{ℋ} G \subseteq ⊥ (H)$
7	1 2	chjcli	$⊢ F \lor_{ℋ} G \in C_{ℋ}$
8	7 3	pjdsi	$⊢ (A \in ((F \lor_{ℋ} G) \lor_{ℋ} H) \land F \lor_{ℋ} G \subseteq ⊥ (H)) \to A = {proj}_{ℎ} (F \lor_{ℋ} G) (A) +_{ℎ} {proj}_{ℎ} (H) (A)$
9	4 6 8	syl2an	$⊢ ((A \in ((F \lor_{ℋ} G) \lor_{ℋ} H) \land F \subseteq ⊥ (G)) \land (F \subseteq ⊥ (H) \land G \subseteq ⊥ (H))) \to A = {proj}_{ℎ} (F \lor_{ℋ} G) (A) +_{ℎ} {proj}_{ℎ} (H) (A)$
10	1 2	osumi	$⊢ F \subseteq ⊥ (G) \to F +_{ℋ} G = F \lor_{ℋ} G$
11	10	fveq2d	$⊢ F \subseteq ⊥ (G) \to {proj}_{ℎ} (F +_{ℋ} G) = {proj}_{ℎ} (F \lor_{ℋ} G)$
12	11	fveq1d	$⊢ F \subseteq ⊥ (G) \to {proj}_{ℎ} (F +_{ℋ} G) (A) = {proj}_{ℎ} (F \lor_{ℋ} G) (A)$
13	12	oveq1d	$⊢ F \subseteq ⊥ (G) \to {proj}_{ℎ} (F +_{ℋ} G) (A) +_{ℎ} {proj}_{ℎ} (H) (A) = {proj}_{ℎ} (F \lor_{ℋ} G) (A) +_{ℎ} {proj}_{ℎ} (H) (A)$
14	13	ad2antlr	$⊢ ((A \in ((F \lor_{ℋ} G) \lor_{ℋ} H) \land F \subseteq ⊥ (G)) \land (F \subseteq ⊥ (H) \land G \subseteq ⊥ (H))) \to {proj}_{ℎ} (F +_{ℋ} G) (A) +_{ℎ} {proj}_{ℎ} (H) (A) = {proj}_{ℎ} (F \lor_{ℋ} G) (A) +_{ℎ} {proj}_{ℎ} (H) (A)$
15	7 3	chjcli	$⊢ (F \lor_{ℋ} G) \lor_{ℋ} H \in C_{ℋ}$
16	15	cheli	$⊢ A \in ((F \lor_{ℋ} G) \lor_{ℋ} H) \to A \in ℋ$
17	1 2	pjsumi	$⊢ A \in ℋ \to (F \subseteq ⊥ (G) \to {proj}_{ℎ} (F +_{ℋ} G) (A) = {proj}_{ℎ} (F) (A) +_{ℎ} {proj}_{ℎ} (G) (A))$
18	17	imp	$⊢ (A \in ℋ \land F \subseteq ⊥ (G)) \to {proj}_{ℎ} (F +_{ℋ} G) (A) = {proj}_{ℎ} (F) (A) +_{ℎ} {proj}_{ℎ} (G) (A)$
19	16 18	sylan	$⊢ (A \in ((F \lor_{ℋ} G) \lor_{ℋ} H) \land F \subseteq ⊥ (G)) \to {proj}_{ℎ} (F +_{ℋ} G) (A) = {proj}_{ℎ} (F) (A) +_{ℎ} {proj}_{ℎ} (G) (A)$
20	19	oveq1d	$⊢ (A \in ((F \lor_{ℋ} G) \lor_{ℋ} H) \land F \subseteq ⊥ (G)) \to {proj}_{ℎ} (F +_{ℋ} G) (A) +_{ℎ} {proj}_{ℎ} (H) (A) = ({proj}_{ℎ} (F) (A) +_{ℎ} {proj}_{ℎ} (G) (A)) +_{ℎ} {proj}_{ℎ} (H) (A)$
21	20	adantr	$⊢ ((A \in ((F \lor_{ℋ} G) \lor_{ℋ} H) \land F \subseteq ⊥ (G)) \land (F \subseteq ⊥ (H) \land G \subseteq ⊥ (H))) \to {proj}_{ℎ} (F +_{ℋ} G) (A) +_{ℎ} {proj}_{ℎ} (H) (A) = ({proj}_{ℎ} (F) (A) +_{ℎ} {proj}_{ℎ} (G) (A)) +_{ℎ} {proj}_{ℎ} (H) (A)$
22	9 14 21	3eqtr2d	$⊢ ((A \in ((F \lor_{ℋ} G) \lor_{ℋ} H) \land F \subseteq ⊥ (G)) \land (F \subseteq ⊥ (H) \land G \subseteq ⊥ (H))) \to A = ({proj}_{ℎ} (F) (A) +_{ℎ} {proj}_{ℎ} (G) (A)) +_{ℎ} {proj}_{ℎ} (H) (A)$

Metamath Proof Explorer

Theorem pjds3i

Proof