Step |
Hyp |
Ref |
Expression |
1 |
|
pjoml2.1 |
|- A e. CH |
2 |
|
pjoml2.2 |
|- B e. CH |
3 |
1 2
|
cmcmi |
|- ( A C_H B <-> B C_H A ) |
4 |
2 1
|
cmbr2i |
|- ( B C_H A <-> B = ( ( B vH A ) i^i ( B vH ( _|_ ` A ) ) ) ) |
5 |
3 4
|
bitri |
|- ( A C_H B <-> B = ( ( B vH A ) i^i ( B vH ( _|_ ` A ) ) ) ) |
6 |
|
ineq2 |
|- ( B = ( ( B vH A ) i^i ( B vH ( _|_ ` A ) ) ) -> ( A i^i B ) = ( A i^i ( ( B vH A ) i^i ( B vH ( _|_ ` A ) ) ) ) ) |
7 |
|
inass |
|- ( ( A i^i ( B vH A ) ) i^i ( B vH ( _|_ ` A ) ) ) = ( A i^i ( ( B vH A ) i^i ( B vH ( _|_ ` A ) ) ) ) |
8 |
2 1
|
chjcomi |
|- ( B vH A ) = ( A vH B ) |
9 |
8
|
ineq2i |
|- ( A i^i ( B vH A ) ) = ( A i^i ( A vH B ) ) |
10 |
1 2
|
chabs2i |
|- ( A i^i ( A vH B ) ) = A |
11 |
9 10
|
eqtri |
|- ( A i^i ( B vH A ) ) = A |
12 |
1
|
choccli |
|- ( _|_ ` A ) e. CH |
13 |
2 12
|
chjcomi |
|- ( B vH ( _|_ ` A ) ) = ( ( _|_ ` A ) vH B ) |
14 |
11 13
|
ineq12i |
|- ( ( A i^i ( B vH A ) ) i^i ( B vH ( _|_ ` A ) ) ) = ( A i^i ( ( _|_ ` A ) vH B ) ) |
15 |
7 14
|
eqtr3i |
|- ( A i^i ( ( B vH A ) i^i ( B vH ( _|_ ` A ) ) ) ) = ( A i^i ( ( _|_ ` A ) vH B ) ) |
16 |
6 15
|
eqtr2di |
|- ( B = ( ( B vH A ) i^i ( B vH ( _|_ ` A ) ) ) -> ( A i^i ( ( _|_ ` A ) vH B ) ) = ( A i^i B ) ) |
17 |
5 16
|
sylbi |
|- ( A C_H B -> ( A i^i ( ( _|_ ` A ) vH B ) ) = ( A i^i B ) ) |
18 |
|
inss1 |
|- ( A i^i ( _|_ ` B ) ) C_ A |
19 |
2
|
choccli |
|- ( _|_ ` B ) e. CH |
20 |
1 19
|
chincli |
|- ( A i^i ( _|_ ` B ) ) e. CH |
21 |
20 1
|
pjoml2i |
|- ( ( A i^i ( _|_ ` B ) ) C_ A -> ( ( A i^i ( _|_ ` B ) ) vH ( ( _|_ ` ( A i^i ( _|_ ` B ) ) ) i^i A ) ) = A ) |
22 |
18 21
|
ax-mp |
|- ( ( A i^i ( _|_ ` B ) ) vH ( ( _|_ ` ( A i^i ( _|_ ` B ) ) ) i^i A ) ) = A |
23 |
20
|
choccli |
|- ( _|_ ` ( A i^i ( _|_ ` B ) ) ) e. CH |
24 |
23 1
|
chincli |
|- ( ( _|_ ` ( A i^i ( _|_ ` B ) ) ) i^i A ) e. CH |
25 |
20 24
|
chjcomi |
|- ( ( A i^i ( _|_ ` B ) ) vH ( ( _|_ ` ( A i^i ( _|_ ` B ) ) ) i^i A ) ) = ( ( ( _|_ ` ( A i^i ( _|_ ` B ) ) ) i^i A ) vH ( A i^i ( _|_ ` B ) ) ) |
26 |
22 25
|
eqtr3i |
|- A = ( ( ( _|_ ` ( A i^i ( _|_ ` B ) ) ) i^i A ) vH ( A i^i ( _|_ ` B ) ) ) |
27 |
1 2
|
chdmm3i |
|- ( _|_ ` ( A i^i ( _|_ ` B ) ) ) = ( ( _|_ ` A ) vH B ) |
28 |
27
|
ineq2i |
|- ( A i^i ( _|_ ` ( A i^i ( _|_ ` B ) ) ) ) = ( A i^i ( ( _|_ ` A ) vH B ) ) |
29 |
|
incom |
|- ( A i^i ( _|_ ` ( A i^i ( _|_ ` B ) ) ) ) = ( ( _|_ ` ( A i^i ( _|_ ` B ) ) ) i^i A ) |
30 |
28 29
|
eqtr3i |
|- ( A i^i ( ( _|_ ` A ) vH B ) ) = ( ( _|_ ` ( A i^i ( _|_ ` B ) ) ) i^i A ) |
31 |
30
|
eqeq1i |
|- ( ( A i^i ( ( _|_ ` A ) vH B ) ) = ( A i^i B ) <-> ( ( _|_ ` ( A i^i ( _|_ ` B ) ) ) i^i A ) = ( A i^i B ) ) |
32 |
|
oveq1 |
|- ( ( ( _|_ ` ( A i^i ( _|_ ` B ) ) ) i^i A ) = ( A i^i B ) -> ( ( ( _|_ ` ( A i^i ( _|_ ` B ) ) ) i^i A ) vH ( A i^i ( _|_ ` B ) ) ) = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) ) |
33 |
31 32
|
sylbi |
|- ( ( A i^i ( ( _|_ ` A ) vH B ) ) = ( A i^i B ) -> ( ( ( _|_ ` ( A i^i ( _|_ ` B ) ) ) i^i A ) vH ( A i^i ( _|_ ` B ) ) ) = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) ) |
34 |
26 33
|
syl5eq |
|- ( ( A i^i ( ( _|_ ` A ) vH B ) ) = ( A i^i B ) -> A = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) ) |
35 |
1 2
|
cmbri |
|- ( A C_H B <-> A = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) ) |
36 |
34 35
|
sylibr |
|- ( ( A i^i ( ( _|_ ` A ) vH B ) ) = ( A i^i B ) -> A C_H B ) |
37 |
17 36
|
impbii |
|- ( A C_H B <-> ( A i^i ( ( _|_ ` A ) vH B ) ) = ( A i^i B ) ) |