Step | Hyp | Ref
| Expression |
1 | | fco 5971 |
. . . . . . 7
⊢ ((𝑇:ran 𝐻⟶ran 𝐾 ∧ 𝑆:ran 𝐺⟶ran 𝐻) → (𝑇 ∘ 𝑆):ran 𝐺⟶ran 𝐾) |
2 | 1 | ancoms 468 |
. . . . . 6
⊢ ((𝑆:ran 𝐺⟶ran 𝐻 ∧ 𝑇:ran 𝐻⟶ran 𝐾) → (𝑇 ∘ 𝑆):ran 𝐺⟶ran 𝐾) |
3 | 2 | ad2ant2r 779 |
. . . . 5
⊢ (((𝑆:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑆‘𝑥)𝐻(𝑆‘𝑦)) = (𝑆‘(𝑥𝐺𝑦))) ∧ (𝑇:ran 𝐻⟶ran 𝐾 ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣)))) → (𝑇 ∘ 𝑆):ran 𝐺⟶ran 𝐾) |
4 | 3 | a1i 11 |
. . . 4
⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp) → (((𝑆:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑆‘𝑥)𝐻(𝑆‘𝑦)) = (𝑆‘(𝑥𝐺𝑦))) ∧ (𝑇:ran 𝐻⟶ran 𝐾 ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣)))) → (𝑇 ∘ 𝑆):ran 𝐺⟶ran 𝐾)) |
5 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑆:ran 𝐺⟶ran 𝐻 ∧ 𝑥 ∈ ran 𝐺) → (𝑆‘𝑥) ∈ ran 𝐻) |
6 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑆:ran 𝐺⟶ran 𝐻 ∧ 𝑦 ∈ ran 𝐺) → (𝑆‘𝑦) ∈ ran 𝐻) |
7 | 5, 6 | anim12da 32676 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑆:ran 𝐺⟶ran 𝐻 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺)) → ((𝑆‘𝑥) ∈ ran 𝐻 ∧ (𝑆‘𝑦) ∈ ran 𝐻)) |
8 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑢 = (𝑆‘𝑥) → (𝑇‘𝑢) = (𝑇‘(𝑆‘𝑥))) |
9 | 8 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 = (𝑆‘𝑥) → ((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = ((𝑇‘(𝑆‘𝑥))𝐾(𝑇‘𝑣))) |
10 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑢 = (𝑆‘𝑥) → (𝑢𝐻𝑣) = ((𝑆‘𝑥)𝐻𝑣)) |
11 | 10 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 = (𝑆‘𝑥) → (𝑇‘(𝑢𝐻𝑣)) = (𝑇‘((𝑆‘𝑥)𝐻𝑣))) |
12 | 9, 11 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 = (𝑆‘𝑥) → (((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣)) ↔ ((𝑇‘(𝑆‘𝑥))𝐾(𝑇‘𝑣)) = (𝑇‘((𝑆‘𝑥)𝐻𝑣)))) |
13 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑣 = (𝑆‘𝑦) → (𝑇‘𝑣) = (𝑇‘(𝑆‘𝑦))) |
14 | 13 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑣 = (𝑆‘𝑦) → ((𝑇‘(𝑆‘𝑥))𝐾(𝑇‘𝑣)) = ((𝑇‘(𝑆‘𝑥))𝐾(𝑇‘(𝑆‘𝑦)))) |
15 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑣 = (𝑆‘𝑦) → ((𝑆‘𝑥)𝐻𝑣) = ((𝑆‘𝑥)𝐻(𝑆‘𝑦))) |
16 | 15 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑣 = (𝑆‘𝑦) → (𝑇‘((𝑆‘𝑥)𝐻𝑣)) = (𝑇‘((𝑆‘𝑥)𝐻(𝑆‘𝑦)))) |
17 | 14, 16 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 = (𝑆‘𝑦) → (((𝑇‘(𝑆‘𝑥))𝐾(𝑇‘𝑣)) = (𝑇‘((𝑆‘𝑥)𝐻𝑣)) ↔ ((𝑇‘(𝑆‘𝑥))𝐾(𝑇‘(𝑆‘𝑦))) = (𝑇‘((𝑆‘𝑥)𝐻(𝑆‘𝑦))))) |
18 | 12, 17 | rspc2va 3294 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑆‘𝑥) ∈ ran 𝐻 ∧ (𝑆‘𝑦) ∈ ran 𝐻) ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣))) → ((𝑇‘(𝑆‘𝑥))𝐾(𝑇‘(𝑆‘𝑦))) = (𝑇‘((𝑆‘𝑥)𝐻(𝑆‘𝑦)))) |
19 | 7, 18 | sylan 487 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑆:ran 𝐺⟶ran 𝐻 ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺)) ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣))) → ((𝑇‘(𝑆‘𝑥))𝐾(𝑇‘(𝑆‘𝑦))) = (𝑇‘((𝑆‘𝑥)𝐻(𝑆‘𝑦)))) |
20 | 19 | an32s 842 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑆:ran 𝐺⟶ran 𝐻 ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣))) ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺)) → ((𝑇‘(𝑆‘𝑥))𝐾(𝑇‘(𝑆‘𝑦))) = (𝑇‘((𝑆‘𝑥)𝐻(𝑆‘𝑦)))) |
21 | 20 | adantllr 751 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑆:ran 𝐺⟶ran 𝐻 ∧ 𝑇:ran 𝐻⟶ran 𝐾) ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣))) ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺)) → ((𝑇‘(𝑆‘𝑥))𝐾(𝑇‘(𝑆‘𝑦))) = (𝑇‘((𝑆‘𝑥)𝐻(𝑆‘𝑦)))) |
22 | 21 | adantllr 751 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑆:ran 𝐺⟶ran 𝐻 ∧ 𝑇:ran 𝐻⟶ran 𝐾) ∧ 𝐺 ∈ GrpOp) ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣))) ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺)) → ((𝑇‘(𝑆‘𝑥))𝐾(𝑇‘(𝑆‘𝑦))) = (𝑇‘((𝑆‘𝑥)𝐻(𝑆‘𝑦)))) |
23 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑆‘𝑥)𝐻(𝑆‘𝑦)) = (𝑆‘(𝑥𝐺𝑦)) → (𝑇‘((𝑆‘𝑥)𝐻(𝑆‘𝑦))) = (𝑇‘(𝑆‘(𝑥𝐺𝑦)))) |
24 | 22, 23 | sylan9eq 2664 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑆:ran 𝐺⟶ran 𝐻 ∧ 𝑇:ran 𝐻⟶ran 𝐾) ∧ 𝐺 ∈ GrpOp) ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣))) ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺)) ∧ ((𝑆‘𝑥)𝐻(𝑆‘𝑦)) = (𝑆‘(𝑥𝐺𝑦))) → ((𝑇‘(𝑆‘𝑥))𝐾(𝑇‘(𝑆‘𝑦))) = (𝑇‘(𝑆‘(𝑥𝐺𝑦)))) |
25 | 24 | anasss 677 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑆:ran 𝐺⟶ran 𝐻 ∧ 𝑇:ran 𝐻⟶ran 𝐾) ∧ 𝐺 ∈ GrpOp) ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣))) ∧ ((𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺) ∧ ((𝑆‘𝑥)𝐻(𝑆‘𝑦)) = (𝑆‘(𝑥𝐺𝑦)))) → ((𝑇‘(𝑆‘𝑥))𝐾(𝑇‘(𝑆‘𝑦))) = (𝑇‘(𝑆‘(𝑥𝐺𝑦)))) |
26 | | fvco3 6185 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆:ran 𝐺⟶ran 𝐻 ∧ 𝑥 ∈ ran 𝐺) → ((𝑇 ∘ 𝑆)‘𝑥) = (𝑇‘(𝑆‘𝑥))) |
27 | 26 | ad2ant2r 779 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑆:ran 𝐺⟶ran 𝐻 ∧ 𝑇:ran 𝐻⟶ran 𝐾) ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺)) → ((𝑇 ∘ 𝑆)‘𝑥) = (𝑇‘(𝑆‘𝑥))) |
28 | | fvco3 6185 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆:ran 𝐺⟶ran 𝐻 ∧ 𝑦 ∈ ran 𝐺) → ((𝑇 ∘ 𝑆)‘𝑦) = (𝑇‘(𝑆‘𝑦))) |
29 | 28 | ad2ant2rl 781 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑆:ran 𝐺⟶ran 𝐻 ∧ 𝑇:ran 𝐻⟶ran 𝐾) ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺)) → ((𝑇 ∘ 𝑆)‘𝑦) = (𝑇‘(𝑆‘𝑦))) |
30 | 27, 29 | oveq12d 6567 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑆:ran 𝐺⟶ran 𝐻 ∧ 𝑇:ran 𝐻⟶ran 𝐾) ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺)) → (((𝑇 ∘ 𝑆)‘𝑥)𝐾((𝑇 ∘ 𝑆)‘𝑦)) = ((𝑇‘(𝑆‘𝑥))𝐾(𝑇‘(𝑆‘𝑦)))) |
31 | 30 | adantlr 747 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆:ran 𝐺⟶ran 𝐻 ∧ 𝑇:ran 𝐻⟶ran 𝐾) ∧ 𝐺 ∈ GrpOp) ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺)) → (((𝑇 ∘ 𝑆)‘𝑥)𝐾((𝑇 ∘ 𝑆)‘𝑦)) = ((𝑇‘(𝑆‘𝑥))𝐾(𝑇‘(𝑆‘𝑦)))) |
32 | 31 | ad2ant2r 779 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑆:ran 𝐺⟶ran 𝐻 ∧ 𝑇:ran 𝐻⟶ran 𝐾) ∧ 𝐺 ∈ GrpOp) ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣))) ∧ ((𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺) ∧ ((𝑆‘𝑥)𝐻(𝑆‘𝑦)) = (𝑆‘(𝑥𝐺𝑦)))) → (((𝑇 ∘ 𝑆)‘𝑥)𝐾((𝑇 ∘ 𝑆)‘𝑦)) = ((𝑇‘(𝑆‘𝑥))𝐾(𝑇‘(𝑆‘𝑦)))) |
33 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ran 𝐺 = ran 𝐺 |
34 | 33 | grpocl 26738 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 ∈ GrpOp ∧ 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺) → (𝑥𝐺𝑦) ∈ ran 𝐺) |
35 | 34 | 3expb 1258 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ GrpOp ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺)) → (𝑥𝐺𝑦) ∈ ran 𝐺) |
36 | | fvco3 6185 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆:ran 𝐺⟶ran 𝐻 ∧ (𝑥𝐺𝑦) ∈ ran 𝐺) → ((𝑇 ∘ 𝑆)‘(𝑥𝐺𝑦)) = (𝑇‘(𝑆‘(𝑥𝐺𝑦)))) |
37 | 36 | adantlr 747 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑆:ran 𝐺⟶ran 𝐻 ∧ 𝑇:ran 𝐻⟶ran 𝐾) ∧ (𝑥𝐺𝑦) ∈ ran 𝐺) → ((𝑇 ∘ 𝑆)‘(𝑥𝐺𝑦)) = (𝑇‘(𝑆‘(𝑥𝐺𝑦)))) |
38 | 35, 37 | sylan2 490 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑆:ran 𝐺⟶ran 𝐻 ∧ 𝑇:ran 𝐻⟶ran 𝐾) ∧ (𝐺 ∈ GrpOp ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺))) → ((𝑇 ∘ 𝑆)‘(𝑥𝐺𝑦)) = (𝑇‘(𝑆‘(𝑥𝐺𝑦)))) |
39 | 38 | anassrs 678 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆:ran 𝐺⟶ran 𝐻 ∧ 𝑇:ran 𝐻⟶ran 𝐾) ∧ 𝐺 ∈ GrpOp) ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺)) → ((𝑇 ∘ 𝑆)‘(𝑥𝐺𝑦)) = (𝑇‘(𝑆‘(𝑥𝐺𝑦)))) |
40 | 39 | ad2ant2r 779 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑆:ran 𝐺⟶ran 𝐻 ∧ 𝑇:ran 𝐻⟶ran 𝐾) ∧ 𝐺 ∈ GrpOp) ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣))) ∧ ((𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺) ∧ ((𝑆‘𝑥)𝐻(𝑆‘𝑦)) = (𝑆‘(𝑥𝐺𝑦)))) → ((𝑇 ∘ 𝑆)‘(𝑥𝐺𝑦)) = (𝑇‘(𝑆‘(𝑥𝐺𝑦)))) |
41 | 25, 32, 40 | 3eqtr4d 2654 |
. . . . . . . . . . . . . 14
⊢
(((((𝑆:ran 𝐺⟶ran 𝐻 ∧ 𝑇:ran 𝐻⟶ran 𝐾) ∧ 𝐺 ∈ GrpOp) ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣))) ∧ ((𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺) ∧ ((𝑆‘𝑥)𝐻(𝑆‘𝑦)) = (𝑆‘(𝑥𝐺𝑦)))) → (((𝑇 ∘ 𝑆)‘𝑥)𝐾((𝑇 ∘ 𝑆)‘𝑦)) = ((𝑇 ∘ 𝑆)‘(𝑥𝐺𝑦))) |
42 | 41 | expr 641 |
. . . . . . . . . . . . 13
⊢
(((((𝑆:ran 𝐺⟶ran 𝐻 ∧ 𝑇:ran 𝐻⟶ran 𝐾) ∧ 𝐺 ∈ GrpOp) ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣))) ∧ (𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺)) → (((𝑆‘𝑥)𝐻(𝑆‘𝑦)) = (𝑆‘(𝑥𝐺𝑦)) → (((𝑇 ∘ 𝑆)‘𝑥)𝐾((𝑇 ∘ 𝑆)‘𝑦)) = ((𝑇 ∘ 𝑆)‘(𝑥𝐺𝑦)))) |
43 | 42 | ralimdvva 2947 |
. . . . . . . . . . . 12
⊢ ((((𝑆:ran 𝐺⟶ran 𝐻 ∧ 𝑇:ran 𝐻⟶ran 𝐾) ∧ 𝐺 ∈ GrpOp) ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣))) → (∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑆‘𝑥)𝐻(𝑆‘𝑦)) = (𝑆‘(𝑥𝐺𝑦)) → ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺(((𝑇 ∘ 𝑆)‘𝑥)𝐾((𝑇 ∘ 𝑆)‘𝑦)) = ((𝑇 ∘ 𝑆)‘(𝑥𝐺𝑦)))) |
44 | 43 | an32s 842 |
. . . . . . . . . . 11
⊢ ((((𝑆:ran 𝐺⟶ran 𝐻 ∧ 𝑇:ran 𝐻⟶ran 𝐾) ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣))) ∧ 𝐺 ∈ GrpOp) → (∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑆‘𝑥)𝐻(𝑆‘𝑦)) = (𝑆‘(𝑥𝐺𝑦)) → ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺(((𝑇 ∘ 𝑆)‘𝑥)𝐾((𝑇 ∘ 𝑆)‘𝑦)) = ((𝑇 ∘ 𝑆)‘(𝑥𝐺𝑦)))) |
45 | 44 | ex 449 |
. . . . . . . . . 10
⊢ (((𝑆:ran 𝐺⟶ran 𝐻 ∧ 𝑇:ran 𝐻⟶ran 𝐾) ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣))) → (𝐺 ∈ GrpOp → (∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑆‘𝑥)𝐻(𝑆‘𝑦)) = (𝑆‘(𝑥𝐺𝑦)) → ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺(((𝑇 ∘ 𝑆)‘𝑥)𝐾((𝑇 ∘ 𝑆)‘𝑦)) = ((𝑇 ∘ 𝑆)‘(𝑥𝐺𝑦))))) |
46 | 45 | com23 84 |
. . . . . . . . 9
⊢ (((𝑆:ran 𝐺⟶ran 𝐻 ∧ 𝑇:ran 𝐻⟶ran 𝐾) ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣))) → (∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑆‘𝑥)𝐻(𝑆‘𝑦)) = (𝑆‘(𝑥𝐺𝑦)) → (𝐺 ∈ GrpOp → ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺(((𝑇 ∘ 𝑆)‘𝑥)𝐾((𝑇 ∘ 𝑆)‘𝑦)) = ((𝑇 ∘ 𝑆)‘(𝑥𝐺𝑦))))) |
47 | 46 | anasss 677 |
. . . . . . . 8
⊢ ((𝑆:ran 𝐺⟶ran 𝐻 ∧ (𝑇:ran 𝐻⟶ran 𝐾 ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣)))) → (∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑆‘𝑥)𝐻(𝑆‘𝑦)) = (𝑆‘(𝑥𝐺𝑦)) → (𝐺 ∈ GrpOp → ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺(((𝑇 ∘ 𝑆)‘𝑥)𝐾((𝑇 ∘ 𝑆)‘𝑦)) = ((𝑇 ∘ 𝑆)‘(𝑥𝐺𝑦))))) |
48 | 47 | imp 444 |
. . . . . . 7
⊢ (((𝑆:ran 𝐺⟶ran 𝐻 ∧ (𝑇:ran 𝐻⟶ran 𝐾 ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣)))) ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑆‘𝑥)𝐻(𝑆‘𝑦)) = (𝑆‘(𝑥𝐺𝑦))) → (𝐺 ∈ GrpOp → ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺(((𝑇 ∘ 𝑆)‘𝑥)𝐾((𝑇 ∘ 𝑆)‘𝑦)) = ((𝑇 ∘ 𝑆)‘(𝑥𝐺𝑦)))) |
49 | 48 | an32s 842 |
. . . . . 6
⊢ (((𝑆:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑆‘𝑥)𝐻(𝑆‘𝑦)) = (𝑆‘(𝑥𝐺𝑦))) ∧ (𝑇:ran 𝐻⟶ran 𝐾 ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣)))) → (𝐺 ∈ GrpOp → ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺(((𝑇 ∘ 𝑆)‘𝑥)𝐾((𝑇 ∘ 𝑆)‘𝑦)) = ((𝑇 ∘ 𝑆)‘(𝑥𝐺𝑦)))) |
50 | 49 | com12 32 |
. . . . 5
⊢ (𝐺 ∈ GrpOp → (((𝑆:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑆‘𝑥)𝐻(𝑆‘𝑦)) = (𝑆‘(𝑥𝐺𝑦))) ∧ (𝑇:ran 𝐻⟶ran 𝐾 ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣)))) → ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺(((𝑇 ∘ 𝑆)‘𝑥)𝐾((𝑇 ∘ 𝑆)‘𝑦)) = ((𝑇 ∘ 𝑆)‘(𝑥𝐺𝑦)))) |
51 | 50 | 3ad2ant1 1075 |
. . . 4
⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp) → (((𝑆:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑆‘𝑥)𝐻(𝑆‘𝑦)) = (𝑆‘(𝑥𝐺𝑦))) ∧ (𝑇:ran 𝐻⟶ran 𝐾 ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣)))) → ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺(((𝑇 ∘ 𝑆)‘𝑥)𝐾((𝑇 ∘ 𝑆)‘𝑦)) = ((𝑇 ∘ 𝑆)‘(𝑥𝐺𝑦)))) |
52 | 4, 51 | jcad 554 |
. . 3
⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp) → (((𝑆:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑆‘𝑥)𝐻(𝑆‘𝑦)) = (𝑆‘(𝑥𝐺𝑦))) ∧ (𝑇:ran 𝐻⟶ran 𝐾 ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣)))) → ((𝑇 ∘ 𝑆):ran 𝐺⟶ran 𝐾 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺(((𝑇 ∘ 𝑆)‘𝑥)𝐾((𝑇 ∘ 𝑆)‘𝑦)) = ((𝑇 ∘ 𝑆)‘(𝑥𝐺𝑦))))) |
53 | | eqid 2610 |
. . . . . 6
⊢ ran 𝐻 = ran 𝐻 |
54 | 33, 53 | elghomOLD 32856 |
. . . . 5
⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp) → (𝑆 ∈ (𝐺 GrpOpHom 𝐻) ↔ (𝑆:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑆‘𝑥)𝐻(𝑆‘𝑦)) = (𝑆‘(𝑥𝐺𝑦))))) |
55 | 54 | 3adant3 1074 |
. . . 4
⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp) → (𝑆 ∈ (𝐺 GrpOpHom 𝐻) ↔ (𝑆:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑆‘𝑥)𝐻(𝑆‘𝑦)) = (𝑆‘(𝑥𝐺𝑦))))) |
56 | | eqid 2610 |
. . . . . 6
⊢ ran 𝐾 = ran 𝐾 |
57 | 53, 56 | elghomOLD 32856 |
. . . . 5
⊢ ((𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp) → (𝑇 ∈ (𝐻 GrpOpHom 𝐾) ↔ (𝑇:ran 𝐻⟶ran 𝐾 ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣))))) |
58 | 57 | 3adant1 1072 |
. . . 4
⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp) → (𝑇 ∈ (𝐻 GrpOpHom 𝐾) ↔ (𝑇:ran 𝐻⟶ran 𝐾 ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣))))) |
59 | 55, 58 | anbi12d 743 |
. . 3
⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp) → ((𝑆 ∈ (𝐺 GrpOpHom 𝐻) ∧ 𝑇 ∈ (𝐻 GrpOpHom 𝐾)) ↔ ((𝑆:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑆‘𝑥)𝐻(𝑆‘𝑦)) = (𝑆‘(𝑥𝐺𝑦))) ∧ (𝑇:ran 𝐻⟶ran 𝐾 ∧ ∀𝑢 ∈ ran 𝐻∀𝑣 ∈ ran 𝐻((𝑇‘𝑢)𝐾(𝑇‘𝑣)) = (𝑇‘(𝑢𝐻𝑣)))))) |
60 | 33, 56 | elghomOLD 32856 |
. . . 4
⊢ ((𝐺 ∈ GrpOp ∧ 𝐾 ∈ GrpOp) → ((𝑇 ∘ 𝑆) ∈ (𝐺 GrpOpHom 𝐾) ↔ ((𝑇 ∘ 𝑆):ran 𝐺⟶ran 𝐾 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺(((𝑇 ∘ 𝑆)‘𝑥)𝐾((𝑇 ∘ 𝑆)‘𝑦)) = ((𝑇 ∘ 𝑆)‘(𝑥𝐺𝑦))))) |
61 | 60 | 3adant2 1073 |
. . 3
⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp) → ((𝑇 ∘ 𝑆) ∈ (𝐺 GrpOpHom 𝐾) ↔ ((𝑇 ∘ 𝑆):ran 𝐺⟶ran 𝐾 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺(((𝑇 ∘ 𝑆)‘𝑥)𝐾((𝑇 ∘ 𝑆)‘𝑦)) = ((𝑇 ∘ 𝑆)‘(𝑥𝐺𝑦))))) |
62 | 52, 59, 61 | 3imtr4d 282 |
. 2
⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp) → ((𝑆 ∈ (𝐺 GrpOpHom 𝐻) ∧ 𝑇 ∈ (𝐻 GrpOpHom 𝐾)) → (𝑇 ∘ 𝑆) ∈ (𝐺 GrpOpHom 𝐾))) |
63 | 62 | imp 444 |
1
⊢ (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp) ∧ (𝑆 ∈ (𝐺 GrpOpHom 𝐻) ∧ 𝑇 ∈ (𝐻 GrpOpHom 𝐾))) → (𝑇 ∘ 𝑆) ∈ (𝐺 GrpOpHom 𝐾)) |