Step |
Hyp |
Ref |
Expression |
1 |
|
pjin1.1 |
|- G e. CH |
2 |
|
pjin1.2 |
|- H e. CH |
3 |
|
eqss |
|- ( G = H <-> ( G C_ H /\ H C_ G ) ) |
4 |
1 2
|
pjss2coi |
|- ( G C_ H <-> ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` G ) ) |
5 |
|
eqcom |
|- ( ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` G ) <-> ( projh ` G ) = ( ( projh ` G ) o. ( projh ` H ) ) ) |
6 |
4 5
|
bitri |
|- ( G C_ H <-> ( projh ` G ) = ( ( projh ` G ) o. ( projh ` H ) ) ) |
7 |
2 1
|
pjss2coi |
|- ( H C_ G <-> ( ( projh ` H ) o. ( projh ` G ) ) = ( projh ` H ) ) |
8 |
|
eqcom |
|- ( ( ( projh ` H ) o. ( projh ` G ) ) = ( projh ` H ) <-> ( projh ` H ) = ( ( projh ` H ) o. ( projh ` G ) ) ) |
9 |
7 8
|
bitri |
|- ( H C_ G <-> ( projh ` H ) = ( ( projh ` H ) o. ( projh ` G ) ) ) |
10 |
6 9
|
anbi12i |
|- ( ( G C_ H /\ H C_ G ) <-> ( ( projh ` G ) = ( ( projh ` G ) o. ( projh ` H ) ) /\ ( projh ` H ) = ( ( projh ` H ) o. ( projh ` G ) ) ) ) |
11 |
3 10
|
bitr2i |
|- ( ( ( projh ` G ) = ( ( projh ` G ) o. ( projh ` H ) ) /\ ( projh ` H ) = ( ( projh ` H ) o. ( projh ` G ) ) ) <-> G = H ) |
12 |
|
fveq2 |
|- ( G = H -> ( projh ` G ) = ( projh ` H ) ) |
13 |
11 12
|
sylbi |
|- ( ( ( projh ` G ) = ( ( projh ` G ) o. ( projh ` H ) ) /\ ( projh ` H ) = ( ( projh ` H ) o. ( projh ` G ) ) ) -> ( projh ` G ) = ( projh ` H ) ) |
14 |
1
|
pjidmcoi |
|- ( ( projh ` G ) o. ( projh ` G ) ) = ( projh ` G ) |
15 |
|
coeq2 |
|- ( ( projh ` G ) = ( projh ` H ) -> ( ( projh ` G ) o. ( projh ` G ) ) = ( ( projh ` G ) o. ( projh ` H ) ) ) |
16 |
14 15
|
syl5eqr |
|- ( ( projh ` G ) = ( projh ` H ) -> ( projh ` G ) = ( ( projh ` G ) o. ( projh ` H ) ) ) |
17 |
|
coeq2 |
|- ( ( projh ` G ) = ( projh ` H ) -> ( ( projh ` H ) o. ( projh ` G ) ) = ( ( projh ` H ) o. ( projh ` H ) ) ) |
18 |
2
|
pjidmcoi |
|- ( ( projh ` H ) o. ( projh ` H ) ) = ( projh ` H ) |
19 |
17 18
|
eqtr2di |
|- ( ( projh ` G ) = ( projh ` H ) -> ( projh ` H ) = ( ( projh ` H ) o. ( projh ` G ) ) ) |
20 |
16 19
|
jca |
|- ( ( projh ` G ) = ( projh ` H ) -> ( ( projh ` G ) = ( ( projh ` G ) o. ( projh ` H ) ) /\ ( projh ` H ) = ( ( projh ` H ) o. ( projh ` G ) ) ) ) |
21 |
13 20
|
impbii |
|- ( ( ( projh ` G ) = ( ( projh ` G ) o. ( projh ` H ) ) /\ ( projh ` H ) = ( ( projh ` H ) o. ( projh ` G ) ) ) <-> ( projh ` G ) = ( projh ` H ) ) |