Metamath Proof Explorer
Description: Lemma for Theorem 1.22 of Mittelstaedt, p. 20. (Contributed by NM, 22-Apr-2001) (New usage is discouraged.)
|
|
Ref |
Expression |
|
Hypotheses |
pjin1.1 |
⊢ 𝐺 ∈ Cℋ |
|
|
pjin1.2 |
⊢ 𝐻 ∈ Cℋ |
|
Assertion |
pjin1i |
⊢ ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) = ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
pjin1.1 |
⊢ 𝐺 ∈ Cℋ |
| 2 |
|
pjin1.2 |
⊢ 𝐻 ∈ Cℋ |
| 3 |
|
inss1 |
⊢ ( 𝐺 ∩ 𝐻 ) ⊆ 𝐺 |
| 4 |
1 2
|
chincli |
⊢ ( 𝐺 ∩ 𝐻 ) ∈ Cℋ |
| 5 |
4 1
|
pjss1coi |
⊢ ( ( 𝐺 ∩ 𝐻 ) ⊆ 𝐺 ↔ ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) ) = ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) ) |
| 6 |
3 5
|
mpbi |
⊢ ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) ) = ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) |
| 7 |
6
|
eqcomi |
⊢ ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) = ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) ) |