Step |
Hyp |
Ref |
Expression |
1 |
|
caovdig.1 |
|- ( ( ph /\ ( x e. K /\ y e. S /\ z e. S ) ) -> ( x G ( y F z ) ) = ( ( x G y ) H ( x G z ) ) ) |
2 |
1
|
ralrimivvva |
|- ( ph -> A. x e. K A. y e. S A. z e. S ( x G ( y F z ) ) = ( ( x G y ) H ( x G z ) ) ) |
3 |
|
oveq1 |
|- ( x = A -> ( x G ( y F z ) ) = ( A G ( y F z ) ) ) |
4 |
|
oveq1 |
|- ( x = A -> ( x G y ) = ( A G y ) ) |
5 |
|
oveq1 |
|- ( x = A -> ( x G z ) = ( A G z ) ) |
6 |
4 5
|
oveq12d |
|- ( x = A -> ( ( x G y ) H ( x G z ) ) = ( ( A G y ) H ( A G z ) ) ) |
7 |
3 6
|
eqeq12d |
|- ( x = A -> ( ( x G ( y F z ) ) = ( ( x G y ) H ( x G z ) ) <-> ( A G ( y F z ) ) = ( ( A G y ) H ( A G z ) ) ) ) |
8 |
|
oveq1 |
|- ( y = B -> ( y F z ) = ( B F z ) ) |
9 |
8
|
oveq2d |
|- ( y = B -> ( A G ( y F z ) ) = ( A G ( B F z ) ) ) |
10 |
|
oveq2 |
|- ( y = B -> ( A G y ) = ( A G B ) ) |
11 |
10
|
oveq1d |
|- ( y = B -> ( ( A G y ) H ( A G z ) ) = ( ( A G B ) H ( A G z ) ) ) |
12 |
9 11
|
eqeq12d |
|- ( y = B -> ( ( A G ( y F z ) ) = ( ( A G y ) H ( A G z ) ) <-> ( A G ( B F z ) ) = ( ( A G B ) H ( A G z ) ) ) ) |
13 |
|
oveq2 |
|- ( z = C -> ( B F z ) = ( B F C ) ) |
14 |
13
|
oveq2d |
|- ( z = C -> ( A G ( B F z ) ) = ( A G ( B F C ) ) ) |
15 |
|
oveq2 |
|- ( z = C -> ( A G z ) = ( A G C ) ) |
16 |
15
|
oveq2d |
|- ( z = C -> ( ( A G B ) H ( A G z ) ) = ( ( A G B ) H ( A G C ) ) ) |
17 |
14 16
|
eqeq12d |
|- ( z = C -> ( ( A G ( B F z ) ) = ( ( A G B ) H ( A G z ) ) <-> ( A G ( B F C ) ) = ( ( A G B ) H ( A G C ) ) ) ) |
18 |
7 12 17
|
rspc3v |
|- ( ( A e. K /\ B e. S /\ C e. S ) -> ( A. x e. K A. y e. S A. z e. S ( x G ( y F z ) ) = ( ( x G y ) H ( x G z ) ) -> ( A G ( B F C ) ) = ( ( A G B ) H ( A G C ) ) ) ) |
19 |
2 18
|
mpan9 |
|- ( ( ph /\ ( A e. K /\ B e. S /\ C e. S ) ) -> ( A G ( B F C ) ) = ( ( A G B ) H ( A G C ) ) ) |