| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ghomdiv.1 |
⊢ 𝑋 = ran 𝐺 |
| 2 |
|
ghomdiv.2 |
⊢ 𝐷 = ( /𝑔 ‘ 𝐺 ) |
| 3 |
|
ghomdiv.3 |
⊢ 𝐶 = ( /𝑔 ‘ 𝐻 ) |
| 4 |
|
simpl2 |
⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐻 ∈ GrpOp ) |
| 5 |
|
eqid |
⊢ ran 𝐻 = ran 𝐻 |
| 6 |
1 5
|
ghomf |
⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → 𝐹 : 𝑋 ⟶ ran 𝐻 ) |
| 7 |
6
|
ffvelcdmda |
⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐻 ) |
| 8 |
7
|
adantrr |
⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐻 ) |
| 9 |
6
|
ffvelcdmda |
⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐵 ) ∈ ran 𝐻 ) |
| 10 |
9
|
adantrl |
⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ran 𝐻 ) |
| 11 |
5 3
|
grponpcan |
⊢ ( ( 𝐻 ∈ GrpOp ∧ ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐻 ∧ ( 𝐹 ‘ 𝐵 ) ∈ ran 𝐻 ) → ( ( ( 𝐹 ‘ 𝐴 ) 𝐶 ( 𝐹 ‘ 𝐵 ) ) 𝐻 ( 𝐹 ‘ 𝐵 ) ) = ( 𝐹 ‘ 𝐴 ) ) |
| 12 |
4 8 10 11
|
syl3anc |
⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) 𝐶 ( 𝐹 ‘ 𝐵 ) ) 𝐻 ( 𝐹 ‘ 𝐵 ) ) = ( 𝐹 ‘ 𝐴 ) ) |
| 13 |
1 2
|
grponpcan |
⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐷 𝐵 ) 𝐺 𝐵 ) = 𝐴 ) |
| 14 |
13
|
3expb |
⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐵 ) 𝐺 𝐵 ) = 𝐴 ) |
| 15 |
14
|
3ad2antl1 |
⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐵 ) 𝐺 𝐵 ) = 𝐴 ) |
| 16 |
15
|
fveq2d |
⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( ( 𝐴 𝐷 𝐵 ) 𝐺 𝐵 ) ) = ( 𝐹 ‘ 𝐴 ) ) |
| 17 |
1 2
|
grpodivcl |
⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) ∈ 𝑋 ) |
| 18 |
17
|
3expb |
⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) ∈ 𝑋 ) |
| 19 |
|
simprr |
⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 ) |
| 20 |
18 19
|
jca |
⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐵 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) |
| 21 |
20
|
3ad2antl1 |
⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐵 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) |
| 22 |
1
|
ghomlinOLD |
⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ ( 𝐴 𝐷 𝐵 ) ) 𝐻 ( 𝐹 ‘ 𝐵 ) ) = ( 𝐹 ‘ ( ( 𝐴 𝐷 𝐵 ) 𝐺 𝐵 ) ) ) |
| 23 |
22
|
eqcomd |
⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( ( 𝐴 𝐷 𝐵 ) 𝐺 𝐵 ) ) = ( ( 𝐹 ‘ ( 𝐴 𝐷 𝐵 ) ) 𝐻 ( 𝐹 ‘ 𝐵 ) ) ) |
| 24 |
21 23
|
syldan |
⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( ( 𝐴 𝐷 𝐵 ) 𝐺 𝐵 ) ) = ( ( 𝐹 ‘ ( 𝐴 𝐷 𝐵 ) ) 𝐻 ( 𝐹 ‘ 𝐵 ) ) ) |
| 25 |
12 16 24
|
3eqtr2rd |
⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ ( 𝐴 𝐷 𝐵 ) ) 𝐻 ( 𝐹 ‘ 𝐵 ) ) = ( ( ( 𝐹 ‘ 𝐴 ) 𝐶 ( 𝐹 ‘ 𝐵 ) ) 𝐻 ( 𝐹 ‘ 𝐵 ) ) ) |
| 26 |
18
|
3ad2antl1 |
⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) ∈ 𝑋 ) |
| 27 |
6
|
ffvelcdmda |
⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝐴 𝐷 𝐵 ) ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝐴 𝐷 𝐵 ) ) ∈ ran 𝐻 ) |
| 28 |
26 27
|
syldan |
⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝐴 𝐷 𝐵 ) ) ∈ ran 𝐻 ) |
| 29 |
5 3
|
grpodivcl |
⊢ ( ( 𝐻 ∈ GrpOp ∧ ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐻 ∧ ( 𝐹 ‘ 𝐵 ) ∈ ran 𝐻 ) → ( ( 𝐹 ‘ 𝐴 ) 𝐶 ( 𝐹 ‘ 𝐵 ) ) ∈ ran 𝐻 ) |
| 30 |
4 8 10 29
|
syl3anc |
⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) 𝐶 ( 𝐹 ‘ 𝐵 ) ) ∈ ran 𝐻 ) |
| 31 |
5
|
grporcan |
⊢ ( ( 𝐻 ∈ GrpOp ∧ ( ( 𝐹 ‘ ( 𝐴 𝐷 𝐵 ) ) ∈ ran 𝐻 ∧ ( ( 𝐹 ‘ 𝐴 ) 𝐶 ( 𝐹 ‘ 𝐵 ) ) ∈ ran 𝐻 ∧ ( 𝐹 ‘ 𝐵 ) ∈ ran 𝐻 ) ) → ( ( ( 𝐹 ‘ ( 𝐴 𝐷 𝐵 ) ) 𝐻 ( 𝐹 ‘ 𝐵 ) ) = ( ( ( 𝐹 ‘ 𝐴 ) 𝐶 ( 𝐹 ‘ 𝐵 ) ) 𝐻 ( 𝐹 ‘ 𝐵 ) ) ↔ ( 𝐹 ‘ ( 𝐴 𝐷 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) 𝐶 ( 𝐹 ‘ 𝐵 ) ) ) ) |
| 32 |
4 28 30 10 31
|
syl13anc |
⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( ( 𝐹 ‘ ( 𝐴 𝐷 𝐵 ) ) 𝐻 ( 𝐹 ‘ 𝐵 ) ) = ( ( ( 𝐹 ‘ 𝐴 ) 𝐶 ( 𝐹 ‘ 𝐵 ) ) 𝐻 ( 𝐹 ‘ 𝐵 ) ) ↔ ( 𝐹 ‘ ( 𝐴 𝐷 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) 𝐶 ( 𝐹 ‘ 𝐵 ) ) ) ) |
| 33 |
25 32
|
mpbid |
⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝐴 𝐷 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) 𝐶 ( 𝐹 ‘ 𝐵 ) ) ) |