Metamath Proof Explorer

Theorem gsumpropd2lem

Description: Lemma for gsumpropd2 . (Contributed by Thierry Arnoux, 28-Jun-2017)

Ref Expression
Hypotheses gsumpropd2.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
gsumpropd2.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
gsumpropd2.h ⊢ ( 𝜑 → 𝐻 ∈ 𝑋 )
gsumpropd2.b ⊢ ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐻 ) )
gsumpropd2.c ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ 𝐺 ) ∧ 𝑡 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) ∈ ( Base ‘ 𝐺 ) )
gsumpropd2.e ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ 𝐺 ) ∧ 𝑡 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) )
gsumpropd2.n ⊢ ( 𝜑 → Fun 𝐹 )
gsumpropd2.r ⊢ ( 𝜑 → ran 𝐹 ⊆ ( Base ‘ 𝐺 ) )
gsumprop2dlem.1 ⊢ 𝐴 = ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) )
gsumprop2dlem.2 ⊢ 𝐵 = ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) )
Assertion gsumpropd2lem ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐻 Σg 𝐹 ) )

Proof

Step Hyp Ref Expression
1 gsumpropd2.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2 gsumpropd2.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
3 gsumpropd2.h ⊢ ( 𝜑 → 𝐻 ∈ 𝑋 )
4 gsumpropd2.b ⊢ ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐻 ) )
5 gsumpropd2.c ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ 𝐺 ) ∧ 𝑡 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) ∈ ( Base ‘ 𝐺 ) )
6 gsumpropd2.e ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ 𝐺 ) ∧ 𝑡 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) )
7 gsumpropd2.n ⊢ ( 𝜑 → Fun 𝐹 )
8 gsumpropd2.r ⊢ ( 𝜑 → ran 𝐹 ⊆ ( Base ‘ 𝐺 ) )
9 gsumprop2dlem.1 ⊢ 𝐴 = ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) )
10 gsumprop2dlem.2 ⊢ 𝐵 = ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) )
11 4 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( Base ‘ 𝐺 ) ) → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐻 ) )
12 6 eqeq1d ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ 𝐺 ) ∧ 𝑡 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ↔ ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ) )
13 6 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) = ( 𝑎 ( +g ‘ 𝐻 ) 𝑏 ) )
14 13 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( Base ‘ 𝐺 ) ∧ 𝑠 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) )
15 14 ancom2s ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ 𝐺 ) ∧ 𝑡 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) )
16 15 eqeq1d ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ 𝐺 ) ∧ 𝑡 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ↔ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) )
17 12 16 anbi12d ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ 𝐺 ) ∧ 𝑡 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) ↔ ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) ) )
18 17 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑡 ∈ ( Base ‘ 𝐺 ) ) → ( ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) ↔ ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) ) )
19 11 18 raleqbidva ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( Base ‘ 𝐺 ) ) → ( ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) ↔ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) ) )
20 4 19 rabeqbidva ⊢ ( 𝜑 → { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } = { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } )
21 20 sseq2d ⊢ ( 𝜑 → ( ran 𝐹 ⊆ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ↔ ran 𝐹 ⊆ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) )
22 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
23 22 4 6 grpidpropd ⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐻 ) )
24 simprl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∧ dom 𝐹 = ( 𝑚 ... 𝑛 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) )
25 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∧ dom 𝐹 = ( 𝑚 ... 𝑛 ) ) ) ∧ 𝑠 ∈ ( 𝑚 ... 𝑛 ) ) → ran 𝐹 ⊆ ( Base ‘ 𝐺 ) )
26 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∧ dom 𝐹 = ( 𝑚 ... 𝑛 ) ) ) ∧ 𝑠 ∈ ( 𝑚 ... 𝑛 ) ) → Fun 𝐹 )
27 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∧ dom 𝐹 = ( 𝑚 ... 𝑛 ) ) ) ∧ 𝑠 ∈ ( 𝑚 ... 𝑛 ) ) → 𝑠 ∈ ( 𝑚 ... 𝑛 ) )
28 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∧ dom 𝐹 = ( 𝑚 ... 𝑛 ) ) ) ∧ 𝑠 ∈ ( 𝑚 ... 𝑛 ) ) → dom 𝐹 = ( 𝑚 ... 𝑛 ) )
29 27 28 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∧ dom 𝐹 = ( 𝑚 ... 𝑛 ) ) ) ∧ 𝑠 ∈ ( 𝑚 ... 𝑛 ) ) → 𝑠 ∈ dom 𝐹 )
30 fvelrn ⊢ ( ( Fun 𝐹 ∧ 𝑠 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑠 ) ∈ ran 𝐹 )
31 26 29 30 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∧ dom 𝐹 = ( 𝑚 ... 𝑛 ) ) ) ∧ 𝑠 ∈ ( 𝑚 ... 𝑛 ) ) → ( 𝐹 ‘ 𝑠 ) ∈ ran 𝐹 )
32 25 31 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∧ dom 𝐹 = ( 𝑚 ... 𝑛 ) ) ) ∧ 𝑠 ∈ ( 𝑚 ... 𝑛 ) ) → ( 𝐹 ‘ 𝑠 ) ∈ ( Base ‘ 𝐺 ) )
33 5 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∧ dom 𝐹 = ( 𝑚 ... 𝑛 ) ) ) ∧ ( 𝑠 ∈ ( Base ‘ 𝐺 ) ∧ 𝑡 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) ∈ ( Base ‘ 𝐺 ) )
34 6 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∧ dom 𝐹 = ( 𝑚 ... 𝑛 ) ) ) ∧ ( 𝑠 ∈ ( Base ‘ 𝐺 ) ∧ 𝑡 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) )
35 24 32 33 34 seqfeq4 ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∧ dom 𝐹 = ( 𝑚 ... 𝑛 ) ) ) → ( seq 𝑚 ( ( +g ‘ 𝐺 ) , 𝐹 ) ‘ 𝑛 ) = ( seq 𝑚 ( ( +g ‘ 𝐻 ) , 𝐹 ) ‘ 𝑛 ) )
36 35 eqeq2d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∧ dom 𝐹 = ( 𝑚 ... 𝑛 ) ) ) → ( 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐺 ) , 𝐹 ) ‘ 𝑛 ) ↔ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) )
37 36 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ) ∧ dom 𝐹 = ( 𝑚 ... 𝑛 ) ) → ( 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐺 ) , 𝐹 ) ‘ 𝑛 ) ↔ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) )
38 37 pm5.32da ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐺 ) , 𝐹 ) ‘ 𝑛 ) ) ↔ ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) )
39 38 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐺 ) , 𝐹 ) ‘ 𝑛 ) ) ↔ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) )
40 39 exbidv ⊢ ( 𝜑 → ( ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐺 ) , 𝐹 ) ‘ 𝑛 ) ) ↔ ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) )
41 40 iotabidv ⊢ ( 𝜑 → ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐺 ) , 𝐹 ) ‘ 𝑛 ) ) ) = ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) )
42 20 difeq2d ⊢ ( 𝜑 → ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) = ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) )
43 42 imaeq2d ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) = ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) )
44 43 9 10 3eqtr4g ⊢ ( 𝜑 → 𝐴 = 𝐵 )
45 44 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) )
46 45 fveq2d ⊢ ( 𝜑 → ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) )
47 46 adantr ⊢ ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) )
48 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ∧ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) → ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) )
49 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ∧ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → ran 𝐹 ⊆ ( Base ‘ 𝐺 ) )
50 f1ofun ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → Fun 𝑓 )
51 50 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ∧ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → Fun 𝑓 )
52 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ∧ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
53 f1odm ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → dom 𝑓 = ( 1 ... ( ♯ ‘ 𝐴 ) ) )
54 53 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ∧ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → dom 𝑓 = ( 1 ... ( ♯ ‘ 𝐴 ) ) )
55 45 oveq2d ⊢ ( 𝜑 → ( 1 ... ( ♯ ‘ 𝐴 ) ) = ( 1 ... ( ♯ ‘ 𝐵 ) ) )
56 55 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ∧ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → ( 1 ... ( ♯ ‘ 𝐴 ) ) = ( 1 ... ( ♯ ‘ 𝐵 ) ) )
57 54 56 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ∧ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → dom 𝑓 = ( 1 ... ( ♯ ‘ 𝐵 ) ) )
58 52 57 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ∧ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → 𝑎 ∈ dom 𝑓 )
59 fvco ⊢ ( ( Fun 𝑓 ∧ 𝑎 ∈ dom 𝑓 ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑓 ‘ 𝑎 ) ) )
60 51 58 59 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ∧ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑓 ‘ 𝑎 ) ) )
61 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ∧ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → Fun 𝐹 )
62 difpreima ⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) = ( ( ◡ 𝐹 “ V ) ∖ ( ◡ 𝐹 “ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) )
63 7 62 syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) = ( ( ◡ 𝐹 “ V ) ∖ ( ◡ 𝐹 “ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) )
64 9 63 eqtrid ⊢ ( 𝜑 → 𝐴 = ( ( ◡ 𝐹 “ V ) ∖ ( ◡ 𝐹 “ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) )
65 difss ⊢ ( ( ◡ 𝐹 “ V ) ∖ ( ◡ 𝐹 “ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) ⊆ ( ◡ 𝐹 “ V )
66 64 65 eqsstrdi ⊢ ( 𝜑 → 𝐴 ⊆ ( ◡ 𝐹 “ V ) )
67 dfdm4 ⊢ dom 𝐹 = ran ◡ 𝐹
68 dfrn4 ⊢ ran ◡ 𝐹 = ( ◡ 𝐹 “ V )
69 67 68 eqtri ⊢ dom 𝐹 = ( ◡ 𝐹 “ V )
70 66 69 sseqtrrdi ⊢ ( 𝜑 → 𝐴 ⊆ dom 𝐹 )
71 70 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ∧ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → 𝐴 ⊆ dom 𝐹 )
72 f1of ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
73 72 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ∧ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
74 52 56 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ∧ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
75 73 74 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ∧ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → ( 𝑓 ‘ 𝑎 ) ∈ 𝐴 )
76 71 75 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ∧ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → ( 𝑓 ‘ 𝑎 ) ∈ dom 𝐹 )
77 fvelrn ⊢ ( ( Fun 𝐹 ∧ ( 𝑓 ‘ 𝑎 ) ∈ dom 𝐹 ) → ( 𝐹 ‘ ( 𝑓 ‘ 𝑎 ) ) ∈ ran 𝐹 )
78 61 76 77 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ∧ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → ( 𝐹 ‘ ( 𝑓 ‘ 𝑎 ) ) ∈ ran 𝐹 )
79 60 78 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ∧ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑎 ) ∈ ran 𝐹 )
80 49 79 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ∧ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝐺 ) )
81 5 caovclg ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ ( Base ‘ 𝐺 ) )
82 81 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ∧ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ ( Base ‘ 𝐺 ) )
83 13 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ∧ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) = ( 𝑎 ( +g ‘ 𝐻 ) 𝑏 ) )
84 48 80 82 83 seqfeq4 ⊢ ( ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ∧ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) → ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) = ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) )
85 simpr ⊢ ( ( 𝜑 ∧ ¬ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) → ¬ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) )
86 1z ⊢ 1 ∈ ℤ
87 seqfn ⊢ ( 1 ∈ ℤ → seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) Fn ( ℤ≥ ‘ 1 ) )
88 fndm ⊢ ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) Fn ( ℤ≥ ‘ 1 ) → dom seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) = ( ℤ≥ ‘ 1 ) )
89 86 87 88 mp2b ⊢ dom seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) = ( ℤ≥ ‘ 1 )
90 89 eleq2i ⊢ ( ( ♯ ‘ 𝐵 ) ∈ dom seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ↔ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) )
91 85 90 sylnibr ⊢ ( ( 𝜑 ∧ ¬ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) → ¬ ( ♯ ‘ 𝐵 ) ∈ dom seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) )
92 ndmfv ⊢ ( ¬ ( ♯ ‘ 𝐵 ) ∈ dom seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) → ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) = ∅ )
93 91 92 syl ⊢ ( ( 𝜑 ∧ ¬ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) → ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) = ∅ )
94 seqfn ⊢ ( 1 ∈ ℤ → seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) Fn ( ℤ≥ ‘ 1 ) )
95 fndm ⊢ ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) Fn ( ℤ≥ ‘ 1 ) → dom seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) = ( ℤ≥ ‘ 1 ) )
96 86 94 95 mp2b ⊢ dom seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) = ( ℤ≥ ‘ 1 )
97 96 eleq2i ⊢ ( ( ♯ ‘ 𝐵 ) ∈ dom seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ↔ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) )
98 85 97 sylnibr ⊢ ( ( 𝜑 ∧ ¬ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) → ¬ ( ♯ ‘ 𝐵 ) ∈ dom seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) )
99 ndmfv ⊢ ( ¬ ( ♯ ‘ 𝐵 ) ∈ dom seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) → ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) = ∅ )
100 98 99 syl ⊢ ( ( 𝜑 ∧ ¬ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) → ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) = ∅ )
101 93 100 eqtr4d ⊢ ( ( 𝜑 ∧ ¬ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) → ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) = ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) )
102 101 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ∧ ¬ ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) ) → ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) = ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) )
103 84 102 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) = ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) )
104 47 103 eqtrd ⊢ ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) = ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) )
105 104 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( 𝑥 = ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) ↔ 𝑥 = ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) ) )
106 105 pm5.32da ⊢ ( 𝜑 → ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) ) ↔ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) ) ) )
107 55 f1oeq2d ⊢ ( 𝜑 → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ↔ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐴 ) )
108 44 f1oeq3d ⊢ ( 𝜑 → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐴 ↔ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) )
109 107 108 bitrd ⊢ ( 𝜑 → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ↔ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) )
110 109 anbi1d ⊢ ( 𝜑 → ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) ) ↔ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) ) ) )
111 106 110 bitrd ⊢ ( 𝜑 → ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) ) ↔ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) ) ) )
112 111 exbidv ⊢ ( 𝜑 → ( ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) ) ) )
113 112 iotabidv ⊢ ( 𝜑 → ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) ) ) = ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) ) ) )
114 41 113 ifeq12d ⊢ ( 𝜑 → if ( dom 𝐹 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐺 ) , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) ) ) ) = if ( dom 𝐹 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) ) ) ) )
115 21 23 114 ifbieq12d ⊢ ( 𝜑 → if ( ran 𝐹 ⊆ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } , ( 0g ‘ 𝐺 ) , if ( dom 𝐹 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐺 ) , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) ) ) ) ) = if ( ran 𝐹 ⊆ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } , ( 0g ‘ 𝐻 ) , if ( dom 𝐹 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) ) ) ) ) )
116 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
117 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
118 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
119 eqid ⊢ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } = { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) }
120 9 a1i ⊢ ( 𝜑 → 𝐴 = ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } ) ) )
121 eqidd ⊢ ( 𝜑 → dom 𝐹 = dom 𝐹 )
122 116 117 118 119 120 2 1 121 gsumvalx ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = if ( ran 𝐹 ⊆ { 𝑠 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐺 ) ( ( 𝑠 ( +g ‘ 𝐺 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐺 ) 𝑠 ) = 𝑡 ) } , ( 0g ‘ 𝐺 ) , if ( dom 𝐹 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐺 ) , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) ) ) ) ) )
123 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
124 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
125 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
126 eqid ⊢ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } = { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) }
127 10 a1i ⊢ ( 𝜑 → 𝐵 = ( ◡ 𝐹 “ ( V ∖ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } ) ) )
128 123 124 125 126 127 3 1 121 gsumvalx ⊢ ( 𝜑 → ( 𝐻 Σg 𝐹 ) = if ( ran 𝐹 ⊆ { 𝑠 ∈ ( Base ‘ 𝐻 ) ∣ ∀ 𝑡 ∈ ( Base ‘ 𝐻 ) ( ( 𝑠 ( +g ‘ 𝐻 ) 𝑡 ) = 𝑡 ∧ ( 𝑡 ( +g ‘ 𝐻 ) 𝑠 ) = 𝑡 ) } , ( 0g ‘ 𝐻 ) , if ( dom 𝐹 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝐹 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝐻 ) , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝐻 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐵 ) ) ) ) ) ) )
129 115 122 128 3eqtr4d ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐻 Σg 𝐹 ) )