Metamath Proof Explorer

Theorem pj3si

Description: Stronger projection triplet theorem. (Contributed by NM, 2-Dec-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjadj2co.1 ⊢F∈Cℋ
pjadj2co.2 ⊢G∈Cℋ
pjadj2co.3 ⊢H∈Cℋ
Assertion pj3si ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G→projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡F∩G∩H

Proof

Step Hyp Ref Expression
1 pjadj2co.1 ⊢F∈Cℋ
2 pjadj2co.2 ⊢G∈Cℋ
3 pjadj2co.3 ⊢H∈Cℋ
4 1 2 3 pj2cocli ⊢x∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈F
5 4 adantl ⊢ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G∧x∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈F
6 1 pjfi ⊢projℎ⁡F:ℋ⟶ℋ
7 2 pjfi ⊢projℎ⁡G:ℋ⟶ℋ
8 6 7 hocofi ⊢projℎ⁡F∘projℎ⁡G:ℋ⟶ℋ
9 3 pjfi ⊢projℎ⁡H:ℋ⟶ℋ
10 8 9 hocofni ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡HFnℋ
11 fnfvelrn ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡HFnℋ∧x∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H
12 10 11 mpan ⊢x∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H
13 ssel ⊢ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈G
14 12 13 syl5 ⊢ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G→x∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈G
15 14 imp ⊢ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G∧x∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈G
16 5 15 elind ⊢ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G∧x∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈F∩G
17 16 adantll ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G∧x∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈F∩G
18 3 2 1 pj2cocli ⊢x∈ℋ→projℎ⁡H∘projℎ⁡G∘projℎ⁡F⁡x∈H
19 fveq1 ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x=projℎ⁡H∘projℎ⁡G∘projℎ⁡F⁡x
20 19 eleq1d ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈H↔projℎ⁡H∘projℎ⁡G∘projℎ⁡F⁡x∈H
21 18 20 imbitrrid ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F→x∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈H
22 21 imp ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧x∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈H
23 22 adantlr ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G∧x∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈H
24 17 23 elind ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G∧x∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈F∩G∩H
25 8 9 hococli ⊢x∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈ℋ
26 hvsubcl ⊢x∈ℋ∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈ℋ→x-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈ℋ
27 25 26 mpdan ⊢x∈ℋ→x-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈ℋ
28 27 adantl ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G∧x∈ℋ→x-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈ℋ
29 simpl ⊢x∈ℋ∧y∈F∩G∩H→x∈ℋ
30 25 adantr ⊢x∈ℋ∧y∈F∩G∩H→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈ℋ
31 1 2 chincli ⊢F∩G∈Cℋ
32 31 3 chincli ⊢F∩G∩H∈Cℋ
33 32 cheli ⊢y∈F∩G∩H→y∈ℋ
34 33 adantl ⊢x∈ℋ∧y∈F∩G∩H→y∈ℋ
35 29 30 34 3jca ⊢x∈ℋ∧y∈F∩G∩H→x∈ℋ∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈ℋ∧y∈ℋ
36 35 adantl ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G∧x∈ℋ∧y∈F∩G∩H→x∈ℋ∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈ℋ∧y∈ℋ
37 his2sub ⊢x∈ℋ∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈ℋ∧y∈ℋ→x-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy=x⋅ihy−projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy
38 36 37 syl ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G∧x∈ℋ∧y∈F∩G∩H→x-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy=x⋅ihy−projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy
39 19 adantr ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x=projℎ⁡H∘projℎ⁡G∘projℎ⁡F⁡x
40 39 oveq1d ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy=projℎ⁡H∘projℎ⁡G∘projℎ⁡F⁡x⋅ihy
41 3 2 1 pjadj2coi ⊢x∈ℋ∧y∈ℋ→projℎ⁡H∘projℎ⁡G∘projℎ⁡F⁡x⋅ihy=x⋅ihprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡y
42 33 41 sylan2 ⊢x∈ℋ∧y∈F∩G∩H→projℎ⁡H∘projℎ⁡G∘projℎ⁡F⁡x⋅ihy=x⋅ihprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡y
43 1 2 3 pj3lem1 ⊢y∈F∩G∩H→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡y=y
44 43 oveq2d ⊢y∈F∩G∩H→x⋅ihprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡y=x⋅ihy
45 44 adantl ⊢x∈ℋ∧y∈F∩G∩H→x⋅ihprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡y=x⋅ihy
46 42 45 eqtrd ⊢x∈ℋ∧y∈F∩G∩H→projℎ⁡H∘projℎ⁡G∘projℎ⁡F⁡x⋅ihy=x⋅ihy
47 40 46 sylan9eq ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G∧x∈ℋ∧y∈F∩G∩H→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy=x⋅ihy
48 47 oveq1d ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G∧x∈ℋ∧y∈F∩G∩H→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy−projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy=x⋅ihy−projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy
49 25 33 anim12i ⊢x∈ℋ∧y∈F∩G∩H→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈ℋ∧y∈ℋ
50 49 adantl ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G∧x∈ℋ∧y∈F∩G∩H→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈ℋ∧y∈ℋ
51 hicl ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈ℋ∧y∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy∈ℂ
52 50 51 syl ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G∧x∈ℋ∧y∈F∩G∩H→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy∈ℂ
53 52 subidd ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G∧x∈ℋ∧y∈F∩G∩H→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy−projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy=0
54 38 48 53 3eqtr2d ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G∧x∈ℋ∧y∈F∩G∩H→x-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy=0
55 54 expr ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G∧x∈ℋ→y∈F∩G∩H→x-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy=0
56 55 ralrimiv ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G∧x∈ℋ→∀y∈F∩G∩Hx-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy=0
57 32 chshii ⊢F∩G∩H∈Sℋ
58 shocel ⊢F∩G∩H∈Sℋ→x-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈⊥⁡F∩G∩H↔x-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈ℋ∧∀y∈F∩G∩Hx-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy=0
59 57 58 ax-mp ⊢x-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈⊥⁡F∩G∩H↔x-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈ℋ∧∀y∈F∩G∩Hx-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy=0
60 28 56 59 sylanbrc ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G∧x∈ℋ→x-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈⊥⁡F∩G∩H
61 32 pjvi ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈F∩G∩H∧x-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈⊥⁡F∩G∩H→projℎ⁡F∩G∩H⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x+ℎx-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x=projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x
62 24 60 61 syl2anc ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G∧x∈ℋ→projℎ⁡F∩G∩H⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x+ℎx-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x=projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x
63 id ⊢x∈ℋ→x∈ℋ
64 hvaddsub12 ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈ℋ∧x∈ℋ∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x+ℎx-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x=x+ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x
65 25 63 25 64 syl3anc ⊢x∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x+ℎx-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x=x+ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x
66 hvsubid ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x=0ℎ
67 25 66 syl ⊢x∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x=0ℎ
68 67 oveq2d ⊢x∈ℋ→x+ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x=x+ℎ0ℎ
69 ax-hvaddid ⊢x∈ℋ→x+ℎ0ℎ=x
70 68 69 eqtrd ⊢x∈ℋ→x+ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x=x
71 65 70 eqtrd ⊢x∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x+ℎx-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x=x
72 71 fveq2d ⊢x∈ℋ→projℎ⁡F∩G∩H⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x+ℎx-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x=projℎ⁡F∩G∩H⁡x
73 72 adantl ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G∧x∈ℋ→projℎ⁡F∩G∩H⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x+ℎx-ℎprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x=projℎ⁡F∩G∩H⁡x
74 62 73 eqtr3d ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G∧x∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x=projℎ⁡F∩G∩H⁡x
75 74 ralrimiva ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G→∀x∈ℋprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x=projℎ⁡F∩G∩H⁡x
76 8 9 hocofi ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H:ℋ⟶ℋ
77 32 pjfi ⊢projℎ⁡F∩G∩H:ℋ⟶ℋ
78 76 77 hoeqi ⊢∀x∈ℋprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x=projℎ⁡F∩G∩H⁡x↔projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡F∩G∩H
79 75 78 sylib ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧ran⁡projℎ⁡F∘projℎ⁡G∘projℎ⁡H⊆G→projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡F∩G∩H