Metamath Proof Explorer

Theorem pj3lem1

Description: Lemma for 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 pj3lem1 ⊢A∈F∩G∩H→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡A=A

Proof

Step Hyp Ref Expression
1 pjadj2co.1 ⊢F∈Cℋ
2 pjadj2co.2 ⊢G∈Cℋ
3 pjadj2co.3 ⊢H∈Cℋ
4 coass ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H=projℎ⁡F∘projℎ⁡G∘projℎ⁡H
5 4 fveq1i ⊢projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡A=projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡A
6 elin ⊢A∈F∩G∩H↔A∈F∧A∈G∩H
7 1 cheli ⊢A∈F→A∈ℋ
8 7 adantr ⊢A∈F∧A∈G∩H→A∈ℋ
9 1 pjfi ⊢projℎ⁡F:ℋ⟶ℋ
10 2 pjfi ⊢projℎ⁡G:ℋ⟶ℋ
11 3 pjfi ⊢projℎ⁡H:ℋ⟶ℋ
12 10 11 hocofi ⊢projℎ⁡G∘projℎ⁡H:ℋ⟶ℋ
13 9 12 hocoi ⊢A∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡A=projℎ⁡F⁡projℎ⁡G∘projℎ⁡H⁡A
14 8 13 syl ⊢A∈F∧A∈G∩H→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡A=projℎ⁡F⁡projℎ⁡G∘projℎ⁡H⁡A
15 2 3 pjclem4a ⊢A∈G∩H→projℎ⁡G∘projℎ⁡H⁡A=A
16 eleq1 ⊢projℎ⁡G∘projℎ⁡H⁡A=A→projℎ⁡G∘projℎ⁡H⁡A∈F↔A∈F
17 pjid ⊢F∈Cℋ∧projℎ⁡G∘projℎ⁡H⁡A∈F→projℎ⁡F⁡projℎ⁡G∘projℎ⁡H⁡A=projℎ⁡G∘projℎ⁡H⁡A
18 1 17 mpan ⊢projℎ⁡G∘projℎ⁡H⁡A∈F→projℎ⁡F⁡projℎ⁡G∘projℎ⁡H⁡A=projℎ⁡G∘projℎ⁡H⁡A
19 16 18 syl6bir ⊢projℎ⁡G∘projℎ⁡H⁡A=A→A∈F→projℎ⁡F⁡projℎ⁡G∘projℎ⁡H⁡A=projℎ⁡G∘projℎ⁡H⁡A
20 eqeq2 ⊢projℎ⁡G∘projℎ⁡H⁡A=A→projℎ⁡F⁡projℎ⁡G∘projℎ⁡H⁡A=projℎ⁡G∘projℎ⁡H⁡A↔projℎ⁡F⁡projℎ⁡G∘projℎ⁡H⁡A=A
21 19 20 sylibd ⊢projℎ⁡G∘projℎ⁡H⁡A=A→A∈F→projℎ⁡F⁡projℎ⁡G∘projℎ⁡H⁡A=A
22 15 21 syl ⊢A∈G∩H→A∈F→projℎ⁡F⁡projℎ⁡G∘projℎ⁡H⁡A=A
23 22 impcom ⊢A∈F∧A∈G∩H→projℎ⁡F⁡projℎ⁡G∘projℎ⁡H⁡A=A
24 14 23 eqtrd ⊢A∈F∧A∈G∩H→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡A=A
25 6 24 sylbi ⊢A∈F∩G∩H→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡A=A
26 inass ⊢F∩G∩H=F∩G∩H
27 25 26 eleq2s ⊢A∈F∩G∩H→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡A=A
28 5 27 eqtrid ⊢A∈F∩G∩H→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡A=A