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 ⊢ 𝐹 ∈ Cℋ
pjadj2co.2 ⊢ 𝐺 ∈ Cℋ
pjadj2co.3 ⊢ 𝐻 ∈ Cℋ
Assertion pj3lem1 ( 𝐴 ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝐴 ) = 𝐴 )

Proof

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