Step |
Hyp |
Ref |
Expression |
1 |
|
gsumpropd.f |
⊢ ( 𝜑 → 𝐹 ∈ 𝑉 ) |
2 |
|
gsumpropd.g |
⊢ ( 𝜑 → 𝐺 ∈ 𝑊 ) |
3 |
|
gsumpropd.h |
⊢ ( 𝜑 → 𝐻 ∈ 𝑋 ) |
4 |
|
gsumpropd.b |
⊢ ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐻 ) ) |
5 |
|
gsumpropd.p |
⊢ ( 𝜑 → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) ) |
6 |
5
|
oveqd |
⊢ ( 𝜑 → ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) ) |
7 |
6
|
eqeq1d |
⊢ ( 𝜑 → ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ↔ ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ) ) |
8 |
5
|
oveqd |
⊢ ( 𝜑 → ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) ) |
9 |
8
|
eqeq1d |
⊢ ( 𝜑 → ( ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ↔ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) ) |
10 |
7 9
|
anbi12d |
⊢ ( 𝜑 → ( ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) ↔ ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) ) ) |
11 |
4 10
|
raleqbidv |
⊢ ( 𝜑 → ( ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) ↔ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) ) ) |
12 |
4 11
|
rabeqbidv |
⊢ ( 𝜑 → { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } = { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) |
13 |
12
|
sseq2d |
⊢ ( 𝜑 → ( ran 𝐹 ⊆ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ↔ ran 𝐹 ⊆ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) |
14 |
|
eqidd |
⊢ ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) ) |
15 |
5
|
oveqdr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) = ( 𝑎 ( +g ‘ 𝐻 ) 𝑏 ) ) |
16 |
14 4 15
|
grpidpropd |
⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐻 ) ) |
17 |
5
|
seqeq2d |
⊢ ( 𝜑 → seq 𝑚 ( ( +g ‘ 𝐺 ) , 𝐹 ) = seq 𝑚 ( ( +g ‘ 𝐻 ) , 𝐹 ) ) |
18 |
17
|
fveq1d |
⊢ ( 𝜑 → ( seq 𝑚 ( ( +g ‘ 𝐺 ) , 𝐹 ) ‘ 𝑛 ) = ( seq 𝑚 ( ( +g ‘ 𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) |
19 |
18
|
eqeq2d |
⊢ ( 𝜑 → ( 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐺 ) , 𝐹 ) ‘ 𝑛 ) ↔ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) |
20 |
19
|
anbi2d |
⊢ ( 𝜑 → ( ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐺 ) , 𝐹 ) ‘ 𝑛 ) ) ↔ ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) ) |
21 |
20
|
rexbidv |
⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐺 ) , 𝐹 ) ‘ 𝑛 ) ) ↔ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) ) |
22 |
21
|
exbidv |
⊢ ( 𝜑 → ( ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐺 ) , 𝐹 ) ‘ 𝑛 ) ) ↔ ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) ) |
23 |
22
|
iotabidv |
⊢ ( 𝜑 → ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐺 ) , 𝐹 ) ‘ 𝑛 ) ) ) = ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) ) |
24 |
12
|
difeq2d |
⊢ ( 𝜑 → ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) = ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) |
25 |
24
|
imaeq2d |
⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) = ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) |
26 |
25
|
fveq2d |
⊢ ( 𝜑 → ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) = ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) |
27 |
26
|
oveq2d |
⊢ ( 𝜑 → ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) = ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) |
28 |
27
|
f1oeq2d |
⊢ ( 𝜑 → ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ↔ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) |
29 |
25
|
f1oeq3d |
⊢ ( 𝜑 → ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ↔ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) |
30 |
28 29
|
bitrd |
⊢ ( 𝜑 → ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ↔ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) |
31 |
5
|
seqeq2d |
⊢ ( 𝜑 → seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) = seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ) |
32 |
31 26
|
fveq12d |
⊢ ( 𝜑 → ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) = ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) |
33 |
32
|
eqeq2d |
⊢ ( 𝜑 → ( 𝑥 = ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ↔ 𝑥 = ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) |
34 |
30 33
|
anbi12d |
⊢ ( 𝜑 → ( ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ↔ ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) ) |
35 |
34
|
exbidv |
⊢ ( 𝜑 → ( ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) ) |
36 |
35
|
iotabidv |
⊢ ( 𝜑 → ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) = ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) ) |
37 |
23 36
|
ifeq12d |
⊢ ( 𝜑 → if ( dom 𝐹 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐺 ) , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) ) = if ( dom 𝐹 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) ) ) |
38 |
13 16 37
|
ifbieq12d |
⊢ ( 𝜑 → if ( ran 𝐹 ⊆ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } , ( 0g ‘ 𝐺 ) , if ( dom 𝐹 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐺 ) , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) ) ) = if ( ran 𝐹 ⊆ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } , ( 0g ‘ 𝐻 ) , if ( dom 𝐹 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) ) ) ) |
39 |
|
eqid |
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) |
40 |
|
eqid |
⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 ) |
41 |
|
eqid |
⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) |
42 |
|
eqid |
⊢ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } = { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } |
43 |
|
eqidd |
⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) = ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) |
44 |
|
eqidd |
⊢ ( 𝜑 → dom 𝐹 = dom 𝐹 ) |
45 |
39 40 41 42 43 2 1 44
|
gsumvalx |
⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = if ( ran 𝐹 ⊆ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } , ( 0g ‘ 𝐺 ) , if ( dom 𝐹 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐺 ) , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) ) ) ) |
46 |
|
eqid |
⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 ) |
47 |
|
eqid |
⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 ) |
48 |
|
eqid |
⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 ) |
49 |
|
eqid |
⊢ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } = { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } |
50 |
|
eqidd |
⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) = ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) |
51 |
46 47 48 49 50 3 1 44
|
gsumvalx |
⊢ ( 𝜑 → ( 𝐻 Σg 𝐹 ) = if ( ran 𝐹 ⊆ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } , ( 0g ‘ 𝐻 ) , if ( dom 𝐹 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) ) ) ) ) ) ) ) |
52 |
38 45 51
|
3eqtr4d |
⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐻 Σg 𝐹 ) ) |