Theorem pjaddii 30855

Description: Projection of vector sum is sum of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)

Hypotheses

Ref	Expression
pjidm.1	⊢ 𝐻 ∈ Cℋ
pjidm.2	⊢ 𝐴 ∈ ℋ
pjadj.3	⊢ 𝐵 ∈ ℋ

Assertion

Ref	Expression
pjaddii	⊢ ((projℎ‘𝐻)‘(𝐴 +ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵))

Proof of Theorem pjaddii

Step	Hyp	Ref	Expression
1		pjidm.1	. . . . . 6 ⊢ 𝐻 ∈ Cℋ
2		pjidm.2	. . . . . 6 ⊢ 𝐴 ∈ ℋ
3	1, 2	pjpji 30604	. . . . 5 ⊢ 𝐴 = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐴))
4		pjadj.3	. . . . . 6 ⊢ 𝐵 ∈ ℋ
5	1, 4	pjpji 30604	. . . . 5 ⊢ 𝐵 = (((projℎ‘𝐻)‘𝐵) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐵))
6	3, 5	oveq12i 7406	. . . 4 ⊢ (𝐴 +ℎ 𝐵) = ((((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐴)) +ℎ (((projℎ‘𝐻)‘𝐵) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐵)))
7	1, 2	pjhclii 30602	. . . . 5 ⊢ ((projℎ‘𝐻)‘𝐴) ∈ ℋ
8	1	choccli 30487	. . . . . 6 ⊢ (⊥‘𝐻) ∈ Cℋ
9	8, 2	pjhclii 30602	. . . . 5 ⊢ ((projℎ‘(⊥‘𝐻))‘𝐴) ∈ ℋ
10	1, 4	pjhclii 30602	. . . . 5 ⊢ ((projℎ‘𝐻)‘𝐵) ∈ ℋ
11	8, 4	pjhclii 30602	. . . . 5 ⊢ ((projℎ‘(⊥‘𝐻))‘𝐵) ∈ ℋ
12	7, 9, 10, 11	hvadd4i 30238	. . . 4 ⊢ ((((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐴)) +ℎ (((projℎ‘𝐻)‘𝐵) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐵))) = ((((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵)) +ℎ (((projℎ‘(⊥‘𝐻))‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐵)))
13	6, 12	eqtri 2760	. . 3 ⊢ (𝐴 +ℎ 𝐵) = ((((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵)) +ℎ (((projℎ‘(⊥‘𝐻))‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐵)))
14	13	fveq2i 6882	. 2 ⊢ ((projℎ‘𝐻)‘(𝐴 +ℎ 𝐵)) = ((projℎ‘𝐻)‘((((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵)) +ℎ (((projℎ‘(⊥‘𝐻))‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐵))))
15	1	chshii 30407	. . . 4 ⊢ 𝐻 ∈ Sℋ
16	1, 2	pjclii 30601	. . . 4 ⊢ ((projℎ‘𝐻)‘𝐴) ∈ 𝐻
17	1, 4	pjclii 30601	. . . 4 ⊢ ((projℎ‘𝐻)‘𝐵) ∈ 𝐻
18		shaddcl 30397	. . . 4 ⊢ ((𝐻 ∈ Sℋ ∧ ((projℎ‘𝐻)‘𝐴) ∈ 𝐻 ∧ ((projℎ‘𝐻)‘𝐵) ∈ 𝐻) → (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵)) ∈ 𝐻)
19	15, 16, 17, 18	mp3an 1461	. . 3 ⊢ (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵)) ∈ 𝐻
20	8	chshii 30407	. . . 4 ⊢ (⊥‘𝐻) ∈ Sℋ
21	8, 2	pjclii 30601	. . . 4 ⊢ ((projℎ‘(⊥‘𝐻))‘𝐴) ∈ (⊥‘𝐻)
22	8, 4	pjclii 30601	. . . 4 ⊢ ((projℎ‘(⊥‘𝐻))‘𝐵) ∈ (⊥‘𝐻)
23		shaddcl 30397	. . . 4 ⊢ (((⊥‘𝐻) ∈ Sℋ ∧ ((projℎ‘(⊥‘𝐻))‘𝐴) ∈ (⊥‘𝐻) ∧ ((projℎ‘(⊥‘𝐻))‘𝐵) ∈ (⊥‘𝐻)) → (((projℎ‘(⊥‘𝐻))‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐵)) ∈ (⊥‘𝐻))
24	20, 21, 22, 23	mp3an 1461	. . 3 ⊢ (((projℎ‘(⊥‘𝐻))‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐵)) ∈ (⊥‘𝐻)
25	1	pjcompi 30852	. . 3 ⊢ (((((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵)) ∈ 𝐻 ∧ (((projℎ‘(⊥‘𝐻))‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐵)) ∈ (⊥‘𝐻)) → ((projℎ‘𝐻)‘((((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵)) +ℎ (((projℎ‘(⊥‘𝐻))‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐵)))) = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵)))
26	19, 24, 25	mp2an 690	. 2 ⊢ ((projℎ‘𝐻)‘((((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵)) +ℎ (((projℎ‘(⊥‘𝐻))‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐵)))) = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵))
27	14, 26	eqtri 2760	1 ⊢ ((projℎ‘𝐻)‘(𝐴 +ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵))

Syntax hints:   = wceq 1541   ∈ wcel 2106  ‘cfv 6533  (class class class)co 7394   ℋchba 30099   +_ℎ cva 30100   S_ℋ csh 30108   C_ℋ cch 30109  ⊥cort 30110  proj_ℎcpjh 30117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5357  ax-pr 5421  ax-un 7709  ax-inf2 9620  ax-cc 10414  ax-cnex 11150  ax-resscn 11151  ax-1cn 11152  ax-icn 11153  ax-addcl 11154  ax-addrcl 11155  ax-mulcl 11156  ax-mulrcl 11157  ax-mulcom 11158  ax-addass 11159  ax-mulass 11160  ax-distr 11161  ax-i2m1 11162  ax-1ne0 11163  ax-1rid 11164  ax-rnegex 11165  ax-rrecex 11166  ax-cnre 11167  ax-pre-lttri 11168  ax-pre-lttrn 11169  ax-pre-ltadd 11170  ax-pre-mulgt0 11171  ax-pre-sup 11172  ax-addf 11173  ax-mulf 11174  ax-hilex 30179  ax-hfvadd 30180  ax-hvcom 30181  ax-hvass 30182  ax-hv0cl 30183  ax-hvaddid 30184  ax-hfvmul 30185  ax-hvmulid 30186  ax-hvmulass 30187  ax-hvdistr1 30188  ax-hvdistr2 30189  ax-hvmul0 30190  ax-hfi 30259  ax-his1 30262  ax-his2 30263  ax-his3 30264  ax-his4 30265  ax-hcompl 30382

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4320  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-int 4945  df-iun 4993  df-iin 4994  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5568  df-eprel 5574  df-po 5582  df-so 5583  df-fr 5625  df-se 5626  df-we 5627  df-xp 5676  df-rel 5677  df-cnv 5678  df-co 5679  df-dm 5680  df-rn 5681  df-res 5682  df-ima 5683  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7350  df-ov 7397  df-oprab 7398  df-mpo 7399  df-of 7654  df-om 7840  df-1st 7959  df-2nd 7960  df-supp 8131  df-frecs 8250  df-wrecs 8281  df-recs 8355  df-rdg 8394  df-1o 8450  df-2o 8451  df-oadd 8454  df-omul 8455  df-er 8688  df-map 8807  df-pm 8808  df-ixp 8877  df-en 8925  df-dom 8926  df-sdom 8927  df-fin 8928  df-fsupp 9347  df-fi 9390  df-sup 9421  df-inf 9422  df-oi 9489  df-card 9918  df-acn 9921  df-pnf 11234  df-mnf 11235  df-xr 11236  df-ltxr 11237  df-le 11238  df-sub 11430  df-neg 11431  df-div 11856  df-nn 12197  df-2 12259  df-3 12260  df-4 12261  df-5 12262  df-6 12263  df-7 12264  df-8 12265  df-9 12266  df-n0 12457  df-z 12543  df-dec 12662  df-uz 12807  df-q 12917  df-rp 12959  df-xneg 13076  df-xadd 13077  df-xmul 13078  df-ioo 13312  df-ico 13314  df-icc 13315  df-fz 13469  df-fzo 13612  df-fl 13741  df-seq 13951  df-exp 14012  df-hash 14275  df-cj 15030  df-re 15031  df-im 15032  df-sqrt 15166  df-abs 15167  df-clim 15416  df-rlim 15417  df-sum 15617  df-struct 17064  df-sets 17081  df-slot 17099  df-ndx 17111  df-base 17129  df-ress 17158  df-plusg 17194  df-mulr 17195  df-starv 17196  df-sca 17197  df-vsca 17198  df-ip 17199  df-tset 17200  df-ple 17201  df-ds 17203  df-unif 17204  df-hom 17205  df-cco 17206  df-rest 17352  df-topn 17353  df-0g 17371  df-gsum 17372  df-topgen 17373  df-pt 17374  df-prds 17377  df-xrs 17432  df-qtop 17437  df-imas 17438  df-xps 17440  df-mre 17514  df-mrc 17515  df-acs 17517  df-mgm 18545  df-sgrp 18594  df-mnd 18605  df-submnd 18650  df-mulg 18925  df-cntz 19149  df-cmn 19616  df-psmet 20872  df-xmet 20873  df-met 20874  df-bl 20875  df-mopn 20876  df-fbas 20877  df-fg 20878  df-cnfld 20881  df-top 22327  df-topon 22344  df-topsp 22366  df-bases 22380  df-cld 22454  df-ntr 22455  df-cls 22456  df-nei 22533  df-cn 22662  df-cnp 22663  df-lm 22664  df-haus 22750  df-tx 22997  df-hmeo 23190  df-fil 23281  df-fm 23373  df-flim 23374  df-flf 23375  df-xms 23757  df-ms 23758  df-tms 23759  df-cfil 24703  df-cau 24704  df-cmet 24705  df-grpo 29673  df-gid 29674  df-ginv 29675  df-gdiv 29676  df-ablo 29725  df-vc 29739  df-nv 29772  df-va 29775  df-ba 29776  df-sm 29777  df-0v 29778  df-vs 29779  df-nmcv 29780  df-ims 29781  df-dip 29881  df-ssp 29902  df-ph 29993  df-cbn 30043  df-hnorm 30148  df-hba 30149  df-hvsub 30151  df-hlim 30152  df-hcau 30153  df-sh 30387  df-ch 30401  df-oc 30432  df-ch0 30433  df-shs 30488  df-pjh 30575

This theorem is referenced by:  pjsubii  30858  pjaddi  30866