Metamath Proof Explorer

Theorem pjin3i

Description: Lemma for Theorem 1.22 of Mittelstaedt, p. 20. (Contributed by NM, 22-Apr-2001) (New usage is discouraged.)

Ref Expression
Hypotheses pjin3.1 
|- F e. CH
pjin3.2 
|- G e. CH
pjin3.3 
|- H e. CH
Assertion pjin3i 
|- ( ( ( projh ` F ) = ( ( projh ` F ) o. ( projh ` G ) ) /\ ( projh ` F ) = ( ( projh ` F ) o. ( projh ` H ) ) ) <-> ( projh ` F ) = ( ( projh ` F ) o. ( projh ` ( G i^i H ) ) ) )

Proof

Step Hyp Ref Expression
1 pjin3.1 
 |-  F e. CH
2 pjin3.2 
 |-  G e. CH
3 pjin3.3 
 |-  H e. CH
4 ssin 
 |-  ( ( F C_ G /\ F C_ H ) <-> F C_ ( G i^i H ) )
5 1 2 pjss2coi 
 |-  ( F C_ G <-> ( ( projh ` F ) o. ( projh ` G ) ) = ( projh ` F ) )
6 eqcom 
 |-  ( ( ( projh ` F ) o. ( projh ` G ) ) = ( projh ` F ) <-> ( projh ` F ) = ( ( projh ` F ) o. ( projh ` G ) ) )
7 5 6 bitri 
 |-  ( F C_ G <-> ( projh ` F ) = ( ( projh ` F ) o. ( projh ` G ) ) )
8 1 3 pjss2coi 
 |-  ( F C_ H <-> ( ( projh ` F ) o. ( projh ` H ) ) = ( projh ` F ) )
9 eqcom 
 |-  ( ( ( projh ` F ) o. ( projh ` H ) ) = ( projh ` F ) <-> ( projh ` F ) = ( ( projh ` F ) o. ( projh ` H ) ) )
10 8 9 bitri 
 |-  ( F C_ H <-> ( projh ` F ) = ( ( projh ` F ) o. ( projh ` H ) ) )
11 7 10 anbi12i 
 |-  ( ( F C_ G /\ F C_ H ) <-> ( ( projh ` F ) = ( ( projh ` F ) o. ( projh ` G ) ) /\ ( projh ` F ) = ( ( projh ` F ) o. ( projh ` H ) ) ) )
12 2 3 chincli 
 |-  ( G i^i H ) e. CH
13 1 12 pjss2coi 
 |-  ( F C_ ( G i^i H ) <-> ( ( projh ` F ) o. ( projh ` ( G i^i H ) ) ) = ( projh ` F ) )
14 eqcom 
 |-  ( ( ( projh ` F ) o. ( projh ` ( G i^i H ) ) ) = ( projh ` F ) <-> ( projh ` F ) = ( ( projh ` F ) o. ( projh ` ( G i^i H ) ) ) )
15 13 14 bitri 
 |-  ( F C_ ( G i^i H ) <-> ( projh ` F ) = ( ( projh ` F ) o. ( projh ` ( G i^i H ) ) ) )
16 4 11 15 3bitr3i 
 |-  ( ( ( projh ` F ) = ( ( projh ` F ) o. ( projh ` G ) ) /\ ( projh ` F ) = ( ( projh ` F ) o. ( projh ` H ) ) ) <-> ( projh ` F ) = ( ( projh ` F ) o. ( projh ` ( G i^i H ) ) ) )