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 ) ) ) ) |