Metamath Proof Explorer

Theorem pj3cor1i

Description: Projection triplet corollary. (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 pj3cor1i ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡G∘projℎ⁡F∘projℎ⁡H→projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡F∘projℎ⁡G

Proof

Step Hyp Ref Expression
1 pjadj2co.1 ⊢F∈Cℋ
2 pjadj2co.2 ⊢G∈Cℋ
3 pjadj2co.3 ⊢H∈Cℋ
4 fveq1 ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡G∘projℎ⁡F∘projℎ⁡H→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡y=projℎ⁡G∘projℎ⁡F∘projℎ⁡H⁡y
5 4 oveq2d ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡G∘projℎ⁡F∘projℎ⁡H→x⋅ihprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡y=x⋅ihprojℎ⁡G∘projℎ⁡F∘projℎ⁡H⁡y
6 5 adantl ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡G∘projℎ⁡F∘projℎ⁡H→x⋅ihprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡y=x⋅ihprojℎ⁡G∘projℎ⁡F∘projℎ⁡H⁡y
7 6 ad2antlr ⊢x∈ℋ∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡G∘projℎ⁡F∘projℎ⁡H∧y∈ℋ→x⋅ihprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡y=x⋅ihprojℎ⁡G∘projℎ⁡F∘projℎ⁡H⁡y
8 1 2 chincli ⊢F∩G∈Cℋ
9 8 3 chincli ⊢F∩G∩H∈Cℋ
10 9 pjadji ⊢x∈ℋ∧y∈ℋ→projℎ⁡F∩G∩H⁡x⋅ihy=x⋅ihprojℎ⁡F∩G∩H⁡y
11 10 adantlr ⊢x∈ℋ∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡G∘projℎ⁡F∘projℎ⁡H∧y∈ℋ→projℎ⁡F∩G∩H⁡x⋅ihy=x⋅ihprojℎ⁡F∩G∩H⁡y
12 1 2 3 pj3i ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡G∘projℎ⁡F∘projℎ⁡H→projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡F∩G∩H
13 12 fveq1d ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡G∘projℎ⁡F∘projℎ⁡H→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x=projℎ⁡F∩G∩H⁡x
14 13 oveq1d ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡G∘projℎ⁡F∘projℎ⁡H→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy=projℎ⁡F∩G∩H⁡x⋅ihy
15 14 ad2antlr ⊢x∈ℋ∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡G∘projℎ⁡F∘projℎ⁡H∧y∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy=projℎ⁡F∩G∩H⁡x⋅ihy
16 12 fveq1d ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡G∘projℎ⁡F∘projℎ⁡H→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡y=projℎ⁡F∩G∩H⁡y
17 16 oveq2d ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡G∘projℎ⁡F∘projℎ⁡H→x⋅ihprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡y=x⋅ihprojℎ⁡F∩G∩H⁡y
18 17 ad2antlr ⊢x∈ℋ∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡G∘projℎ⁡F∘projℎ⁡H∧y∈ℋ→x⋅ihprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡y=x⋅ihprojℎ⁡F∩G∩H⁡y
19 11 15 18 3eqtr4d ⊢x∈ℋ∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡G∘projℎ⁡F∘projℎ⁡H∧y∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy=x⋅ihprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡y
20 3 1 2 pjadj2coi ⊢x∈ℋ∧y∈ℋ→projℎ⁡H∘projℎ⁡F∘projℎ⁡G⁡x⋅ihy=x⋅ihprojℎ⁡G∘projℎ⁡F∘projℎ⁡H⁡y
21 20 adantlr ⊢x∈ℋ∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡G∘projℎ⁡F∘projℎ⁡H∧y∈ℋ→projℎ⁡H∘projℎ⁡F∘projℎ⁡G⁡x⋅ihy=x⋅ihprojℎ⁡G∘projℎ⁡F∘projℎ⁡H⁡y
22 7 19 21 3eqtr4d ⊢x∈ℋ∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡G∘projℎ⁡F∘projℎ⁡H∧y∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy=projℎ⁡H∘projℎ⁡F∘projℎ⁡G⁡x⋅ihy
23 22 exp31 ⊢x∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡G∘projℎ⁡F∘projℎ⁡H→y∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy=projℎ⁡H∘projℎ⁡F∘projℎ⁡G⁡x⋅ihy
24 23 ralrimdv ⊢x∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡G∘projℎ⁡F∘projℎ⁡H→∀y∈ℋprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy=projℎ⁡H∘projℎ⁡F∘projℎ⁡G⁡x⋅ihy
25 1 pjfi ⊢projℎ⁡F:ℋ⟶ℋ
26 2 pjfi ⊢projℎ⁡G:ℋ⟶ℋ
27 25 26 hocofi ⊢projℎ⁡F∘projℎ⁡G:ℋ⟶ℋ
28 3 pjfi ⊢projℎ⁡H:ℋ⟶ℋ
29 27 28 hococli ⊢x∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈ℋ
30 28 25 hocofi ⊢projℎ⁡H∘projℎ⁡F:ℋ⟶ℋ
31 30 26 hococli ⊢x∈ℋ→projℎ⁡H∘projℎ⁡F∘projℎ⁡G⁡x∈ℋ
32 hial2eq ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x∈ℋ∧projℎ⁡H∘projℎ⁡F∘projℎ⁡G⁡x∈ℋ→∀y∈ℋprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy=projℎ⁡H∘projℎ⁡F∘projℎ⁡G⁡x⋅ihy↔projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x=projℎ⁡H∘projℎ⁡F∘projℎ⁡G⁡x
33 29 31 32 syl2anc ⊢x∈ℋ→∀y∈ℋprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x⋅ihy=projℎ⁡H∘projℎ⁡F∘projℎ⁡G⁡x⋅ihy↔projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x=projℎ⁡H∘projℎ⁡F∘projℎ⁡G⁡x
34 24 33 sylibd ⊢x∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡G∘projℎ⁡F∘projℎ⁡H→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x=projℎ⁡H∘projℎ⁡F∘projℎ⁡G⁡x
35 34 com12 ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡G∘projℎ⁡F∘projℎ⁡H→x∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x=projℎ⁡H∘projℎ⁡F∘projℎ⁡G⁡x
36 35 ralrimiv ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡G∘projℎ⁡F∘projℎ⁡H→∀x∈ℋprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x=projℎ⁡H∘projℎ⁡F∘projℎ⁡G⁡x
37 27 28 hocofi ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H:ℋ⟶ℋ
38 30 26 hocofi ⊢projℎ⁡H∘projℎ⁡F∘projℎ⁡G:ℋ⟶ℋ
39 37 38 hoeqi ⊢∀x∈ℋprojℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡x=projℎ⁡H∘projℎ⁡F∘projℎ⁡G⁡x↔projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡F∘projℎ⁡G
40 36 39 sylib ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G∘projℎ⁡F∧projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡G∘projℎ⁡F∘projℎ⁡H→projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡F∘projℎ⁡G