MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gsmsymgreqlem2 Structured version   Visualization version   GIF version

Theorem gsmsymgreqlem2 17772
Description: Lemma 2 for gsmsymgreq 17773. (Contributed by AV, 26-Jan-2019.)
Hypotheses
Ref Expression
gsmsymgrfix.s 𝑆 = (SymGrp‘𝑁)
gsmsymgrfix.b 𝐵 = (Base‘𝑆)
gsmsymgreq.z 𝑍 = (SymGrp‘𝑀)
gsmsymgreq.p 𝑃 = (Base‘𝑍)
gsmsymgreq.i 𝐼 = (𝑁𝑀)
Assertion
Ref Expression
gsmsymgreqlem2 (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) → ((∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛𝐼 ((𝑋𝑖)‘𝑛) = ((𝑌𝑖)‘𝑛) → ∀𝑛𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛)) → (∀𝑖 ∈ (0..^(#‘(𝑋 ++ ⟨“𝐶”⟩)))∀𝑛𝐼 (((𝑋 ++ ⟨“𝐶”⟩)‘𝑖)‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘𝑖)‘𝑛) → ∀𝑛𝐼 ((𝑆 Σg (𝑋 ++ ⟨“𝐶”⟩))‘𝑛) = ((𝑍 Σg (𝑌 ++ ⟨“𝑅”⟩))‘𝑛))))
Distinct variable groups:   𝐵,𝑖   𝑖,𝑁   𝑃,𝑖   𝑛,𝐼   𝑛,𝑋   𝐶,𝑛   𝑅,𝑛   𝑆,𝑛   𝑛,𝑌   𝑛,𝑍   𝐵,𝑛   𝐶,𝑖,𝑛   𝑖,𝐼   𝑛,𝑀   𝑛,𝑁   𝑃,𝑛   𝑅,𝑖   𝑖,𝑋   𝑖,𝑌
Allowed substitution hints:   𝑆(𝑖)   𝑀(𝑖)   𝑍(𝑖)

Proof of Theorem gsmsymgreqlem2
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 ccatws1len 13337 . . . . . . . . 9 ((𝑋 ∈ Word 𝐵𝐶𝐵) → (#‘(𝑋 ++ ⟨“𝐶”⟩)) = ((#‘𝑋) + 1))
213ad2ant1 1080 . . . . . . . 8 (((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (#‘(𝑋 ++ ⟨“𝐶”⟩)) = ((#‘𝑋) + 1))
32oveq2d 6620 . . . . . . 7 (((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (0..^(#‘(𝑋 ++ ⟨“𝐶”⟩))) = (0..^((#‘𝑋) + 1)))
4 lencl 13263 . . . . . . . . . . 11 (𝑋 ∈ Word 𝐵 → (#‘𝑋) ∈ ℕ0)
5 elnn0uz 11669 . . . . . . . . . . 11 ((#‘𝑋) ∈ ℕ0 ↔ (#‘𝑋) ∈ (ℤ‘0))
64, 5sylib 208 . . . . . . . . . 10 (𝑋 ∈ Word 𝐵 → (#‘𝑋) ∈ (ℤ‘0))
76adantr 481 . . . . . . . . 9 ((𝑋 ∈ Word 𝐵𝐶𝐵) → (#‘𝑋) ∈ (ℤ‘0))
8 fzosplitsn 12517 . . . . . . . . 9 ((#‘𝑋) ∈ (ℤ‘0) → (0..^((#‘𝑋) + 1)) = ((0..^(#‘𝑋)) ∪ {(#‘𝑋)}))
97, 8syl 17 . . . . . . . 8 ((𝑋 ∈ Word 𝐵𝐶𝐵) → (0..^((#‘𝑋) + 1)) = ((0..^(#‘𝑋)) ∪ {(#‘𝑋)}))
1093ad2ant1 1080 . . . . . . 7 (((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (0..^((#‘𝑋) + 1)) = ((0..^(#‘𝑋)) ∪ {(#‘𝑋)}))
113, 10eqtrd 2655 . . . . . 6 (((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (0..^(#‘(𝑋 ++ ⟨“𝐶”⟩))) = ((0..^(#‘𝑋)) ∪ {(#‘𝑋)}))
1211raleqdv 3133 . . . . 5 (((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (∀𝑖 ∈ (0..^(#‘(𝑋 ++ ⟨“𝐶”⟩)))∀𝑛𝐼 (((𝑋 ++ ⟨“𝐶”⟩)‘𝑖)‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘𝑖)‘𝑛) ↔ ∀𝑖 ∈ ((0..^(#‘𝑋)) ∪ {(#‘𝑋)})∀𝑛𝐼 (((𝑋 ++ ⟨“𝐶”⟩)‘𝑖)‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘𝑖)‘𝑛)))
134adantr 481 . . . . . . 7 ((𝑋 ∈ Word 𝐵𝐶𝐵) → (#‘𝑋) ∈ ℕ0)
14133ad2ant1 1080 . . . . . 6 (((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (#‘𝑋) ∈ ℕ0)
15 fveq2 6148 . . . . . . . . . 10 (𝑖 = (#‘𝑋) → ((𝑋 ++ ⟨“𝐶”⟩)‘𝑖) = ((𝑋 ++ ⟨“𝐶”⟩)‘(#‘𝑋)))
1615fveq1d 6150 . . . . . . . . 9 (𝑖 = (#‘𝑋) → (((𝑋 ++ ⟨“𝐶”⟩)‘𝑖)‘𝑛) = (((𝑋 ++ ⟨“𝐶”⟩)‘(#‘𝑋))‘𝑛))
17 fveq2 6148 . . . . . . . . . 10 (𝑖 = (#‘𝑋) → ((𝑌 ++ ⟨“𝑅”⟩)‘𝑖) = ((𝑌 ++ ⟨“𝑅”⟩)‘(#‘𝑋)))
1817fveq1d 6150 . . . . . . . . 9 (𝑖 = (#‘𝑋) → (((𝑌 ++ ⟨“𝑅”⟩)‘𝑖)‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘(#‘𝑋))‘𝑛))
1916, 18eqeq12d 2636 . . . . . . . 8 (𝑖 = (#‘𝑋) → ((((𝑋 ++ ⟨“𝐶”⟩)‘𝑖)‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘𝑖)‘𝑛) ↔ (((𝑋 ++ ⟨“𝐶”⟩)‘(#‘𝑋))‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘(#‘𝑋))‘𝑛)))
2019ralbidv 2980 . . . . . . 7 (𝑖 = (#‘𝑋) → (∀𝑛𝐼 (((𝑋 ++ ⟨“𝐶”⟩)‘𝑖)‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘𝑖)‘𝑛) ↔ ∀𝑛𝐼 (((𝑋 ++ ⟨“𝐶”⟩)‘(#‘𝑋))‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘(#‘𝑋))‘𝑛)))
2120ralunsn 4390 . . . . . 6 ((#‘𝑋) ∈ ℕ0 → (∀𝑖 ∈ ((0..^(#‘𝑋)) ∪ {(#‘𝑋)})∀𝑛𝐼 (((𝑋 ++ ⟨“𝐶”⟩)‘𝑖)‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘𝑖)‘𝑛) ↔ (∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛𝐼 (((𝑋 ++ ⟨“𝐶”⟩)‘𝑖)‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘𝑖)‘𝑛) ∧ ∀𝑛𝐼 (((𝑋 ++ ⟨“𝐶”⟩)‘(#‘𝑋))‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘(#‘𝑋))‘𝑛))))
2214, 21syl 17 . . . . 5 (((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (∀𝑖 ∈ ((0..^(#‘𝑋)) ∪ {(#‘𝑋)})∀𝑛𝐼 (((𝑋 ++ ⟨“𝐶”⟩)‘𝑖)‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘𝑖)‘𝑛) ↔ (∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛𝐼 (((𝑋 ++ ⟨“𝐶”⟩)‘𝑖)‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘𝑖)‘𝑛) ∧ ∀𝑛𝐼 (((𝑋 ++ ⟨“𝐶”⟩)‘(#‘𝑋))‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘(#‘𝑋))‘𝑛))))
23 simpl 473 . . . . . . . . . . . . 13 ((𝑋 ∈ Word 𝐵𝐶𝐵) → 𝑋 ∈ Word 𝐵)
24233ad2ant1 1080 . . . . . . . . . . . 12 (((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → 𝑋 ∈ Word 𝐵)
2524adantr 481 . . . . . . . . . . 11 ((((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) ∧ 𝑖 ∈ (0..^(#‘𝑋))) → 𝑋 ∈ Word 𝐵)
26 simpr 477 . . . . . . . . . . . . 13 ((𝑋 ∈ Word 𝐵𝐶𝐵) → 𝐶𝐵)
27263ad2ant1 1080 . . . . . . . . . . . 12 (((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → 𝐶𝐵)
2827adantr 481 . . . . . . . . . . 11 ((((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) ∧ 𝑖 ∈ (0..^(#‘𝑋))) → 𝐶𝐵)
29 simpr 477 . . . . . . . . . . 11 ((((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) ∧ 𝑖 ∈ (0..^(#‘𝑋))) → 𝑖 ∈ (0..^(#‘𝑋)))
30 ccats1val1 13341 . . . . . . . . . . 11 ((𝑋 ∈ Word 𝐵𝐶𝐵𝑖 ∈ (0..^(#‘𝑋))) → ((𝑋 ++ ⟨“𝐶”⟩)‘𝑖) = (𝑋𝑖))
3125, 28, 29, 30syl3anc 1323 . . . . . . . . . 10 ((((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) ∧ 𝑖 ∈ (0..^(#‘𝑋))) → ((𝑋 ++ ⟨“𝐶”⟩)‘𝑖) = (𝑋𝑖))
3231fveq1d 6150 . . . . . . . . 9 ((((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) ∧ 𝑖 ∈ (0..^(#‘𝑋))) → (((𝑋 ++ ⟨“𝐶”⟩)‘𝑖)‘𝑛) = ((𝑋𝑖)‘𝑛))
33 simpl2l 1112 . . . . . . . . . . 11 ((((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) ∧ 𝑖 ∈ (0..^(#‘𝑋))) → 𝑌 ∈ Word 𝑃)
34 simpl2r 1113 . . . . . . . . . . 11 ((((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) ∧ 𝑖 ∈ (0..^(#‘𝑋))) → 𝑅𝑃)
35 oveq2 6612 . . . . . . . . . . . . . . 15 ((#‘𝑋) = (#‘𝑌) → (0..^(#‘𝑋)) = (0..^(#‘𝑌)))
3635eleq2d 2684 . . . . . . . . . . . . . 14 ((#‘𝑋) = (#‘𝑌) → (𝑖 ∈ (0..^(#‘𝑋)) ↔ 𝑖 ∈ (0..^(#‘𝑌))))
3736biimpd 219 . . . . . . . . . . . . 13 ((#‘𝑋) = (#‘𝑌) → (𝑖 ∈ (0..^(#‘𝑋)) → 𝑖 ∈ (0..^(#‘𝑌))))
38373ad2ant3 1082 . . . . . . . . . . . 12 (((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (𝑖 ∈ (0..^(#‘𝑋)) → 𝑖 ∈ (0..^(#‘𝑌))))
3938imp 445 . . . . . . . . . . 11 ((((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) ∧ 𝑖 ∈ (0..^(#‘𝑋))) → 𝑖 ∈ (0..^(#‘𝑌)))
40 ccats1val1 13341 . . . . . . . . . . 11 ((𝑌 ∈ Word 𝑃𝑅𝑃𝑖 ∈ (0..^(#‘𝑌))) → ((𝑌 ++ ⟨“𝑅”⟩)‘𝑖) = (𝑌𝑖))
4133, 34, 39, 40syl3anc 1323 . . . . . . . . . 10 ((((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) ∧ 𝑖 ∈ (0..^(#‘𝑋))) → ((𝑌 ++ ⟨“𝑅”⟩)‘𝑖) = (𝑌𝑖))
4241fveq1d 6150 . . . . . . . . 9 ((((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) ∧ 𝑖 ∈ (0..^(#‘𝑋))) → (((𝑌 ++ ⟨“𝑅”⟩)‘𝑖)‘𝑛) = ((𝑌𝑖)‘𝑛))
4332, 42eqeq12d 2636 . . . . . . . 8 ((((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) ∧ 𝑖 ∈ (0..^(#‘𝑋))) → ((((𝑋 ++ ⟨“𝐶”⟩)‘𝑖)‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘𝑖)‘𝑛) ↔ ((𝑋𝑖)‘𝑛) = ((𝑌𝑖)‘𝑛)))
4443ralbidv 2980 . . . . . . 7 ((((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) ∧ 𝑖 ∈ (0..^(#‘𝑋))) → (∀𝑛𝐼 (((𝑋 ++ ⟨“𝐶”⟩)‘𝑖)‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘𝑖)‘𝑛) ↔ ∀𝑛𝐼 ((𝑋𝑖)‘𝑛) = ((𝑌𝑖)‘𝑛)))
4544ralbidva 2979 . . . . . 6 (((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛𝐼 (((𝑋 ++ ⟨“𝐶”⟩)‘𝑖)‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘𝑖)‘𝑛) ↔ ∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛𝐼 ((𝑋𝑖)‘𝑛) = ((𝑌𝑖)‘𝑛)))
46 eqidd 2622 . . . . . . . . . . . 12 ((𝑋 ∈ Word 𝐵𝐶𝐵) → (#‘𝑋) = (#‘𝑋))
4723, 26, 463jca 1240 . . . . . . . . . . 11 ((𝑋 ∈ Word 𝐵𝐶𝐵) → (𝑋 ∈ Word 𝐵𝐶𝐵 ∧ (#‘𝑋) = (#‘𝑋)))
48473ad2ant1 1080 . . . . . . . . . 10 (((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (𝑋 ∈ Word 𝐵𝐶𝐵 ∧ (#‘𝑋) = (#‘𝑋)))
49 ccats1val2 13342 . . . . . . . . . 10 ((𝑋 ∈ Word 𝐵𝐶𝐵 ∧ (#‘𝑋) = (#‘𝑋)) → ((𝑋 ++ ⟨“𝐶”⟩)‘(#‘𝑋)) = 𝐶)
5048, 49syl 17 . . . . . . . . 9 (((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → ((𝑋 ++ ⟨“𝐶”⟩)‘(#‘𝑋)) = 𝐶)
5150fveq1d 6150 . . . . . . . 8 (((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (((𝑋 ++ ⟨“𝐶”⟩)‘(#‘𝑋))‘𝑛) = (𝐶𝑛))
52 df-3an 1038 . . . . . . . . . . 11 ((𝑌 ∈ Word 𝑃𝑅𝑃 ∧ (#‘𝑋) = (#‘𝑌)) ↔ ((𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)))
5352biimpri 218 . . . . . . . . . 10 (((𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (𝑌 ∈ Word 𝑃𝑅𝑃 ∧ (#‘𝑋) = (#‘𝑌)))
54533adant1 1077 . . . . . . . . 9 (((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (𝑌 ∈ Word 𝑃𝑅𝑃 ∧ (#‘𝑋) = (#‘𝑌)))
55 ccats1val2 13342 . . . . . . . . . 10 ((𝑌 ∈ Word 𝑃𝑅𝑃 ∧ (#‘𝑋) = (#‘𝑌)) → ((𝑌 ++ ⟨“𝑅”⟩)‘(#‘𝑋)) = 𝑅)
5655fveq1d 6150 . . . . . . . . 9 ((𝑌 ∈ Word 𝑃𝑅𝑃 ∧ (#‘𝑋) = (#‘𝑌)) → (((𝑌 ++ ⟨“𝑅”⟩)‘(#‘𝑋))‘𝑛) = (𝑅𝑛))
5754, 56syl 17 . . . . . . . 8 (((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (((𝑌 ++ ⟨“𝑅”⟩)‘(#‘𝑋))‘𝑛) = (𝑅𝑛))
5851, 57eqeq12d 2636 . . . . . . 7 (((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → ((((𝑋 ++ ⟨“𝐶”⟩)‘(#‘𝑋))‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘(#‘𝑋))‘𝑛) ↔ (𝐶𝑛) = (𝑅𝑛)))
5958ralbidv 2980 . . . . . 6 (((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (∀𝑛𝐼 (((𝑋 ++ ⟨“𝐶”⟩)‘(#‘𝑋))‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘(#‘𝑋))‘𝑛) ↔ ∀𝑛𝐼 (𝐶𝑛) = (𝑅𝑛)))
6045, 59anbi12d 746 . . . . 5 (((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → ((∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛𝐼 (((𝑋 ++ ⟨“𝐶”⟩)‘𝑖)‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘𝑖)‘𝑛) ∧ ∀𝑛𝐼 (((𝑋 ++ ⟨“𝐶”⟩)‘(#‘𝑋))‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘(#‘𝑋))‘𝑛)) ↔ (∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛𝐼 ((𝑋𝑖)‘𝑛) = ((𝑌𝑖)‘𝑛) ∧ ∀𝑛𝐼 (𝐶𝑛) = (𝑅𝑛))))
6112, 22, 603bitrd 294 . . . 4 (((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (∀𝑖 ∈ (0..^(#‘(𝑋 ++ ⟨“𝐶”⟩)))∀𝑛𝐼 (((𝑋 ++ ⟨“𝐶”⟩)‘𝑖)‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘𝑖)‘𝑛) ↔ (∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛𝐼 ((𝑋𝑖)‘𝑛) = ((𝑌𝑖)‘𝑛) ∧ ∀𝑛𝐼 (𝐶𝑛) = (𝑅𝑛))))
6261ad2antlr 762 . . 3 ((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ (∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛𝐼 ((𝑋𝑖)‘𝑛) = ((𝑌𝑖)‘𝑛) → ∀𝑛𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛))) → (∀𝑖 ∈ (0..^(#‘(𝑋 ++ ⟨“𝐶”⟩)))∀𝑛𝐼 (((𝑋 ++ ⟨“𝐶”⟩)‘𝑖)‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘𝑖)‘𝑛) ↔ (∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛𝐼 ((𝑋𝑖)‘𝑛) = ((𝑌𝑖)‘𝑛) ∧ ∀𝑛𝐼 (𝐶𝑛) = (𝑅𝑛))))
63 pm3.35 610 . . . . . . 7 ((∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛𝐼 ((𝑋𝑖)‘𝑛) = ((𝑌𝑖)‘𝑛) ∧ (∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛𝐼 ((𝑋𝑖)‘𝑛) = ((𝑌𝑖)‘𝑛) → ∀𝑛𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛))) → ∀𝑛𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛))
64 fveq2 6148 . . . . . . . . . . 11 (𝑛 = 𝑗 → ((𝑆 Σg 𝑋)‘𝑛) = ((𝑆 Σg 𝑋)‘𝑗))
65 fveq2 6148 . . . . . . . . . . 11 (𝑛 = 𝑗 → ((𝑍 Σg 𝑌)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑗))
6664, 65eqeq12d 2636 . . . . . . . . . 10 (𝑛 = 𝑗 → (((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛) ↔ ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)))
6766cbvralv 3159 . . . . . . . . 9 (∀𝑛𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛) ↔ ∀𝑗𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗))
68 simp-4l 805 . . . . . . . . . . . . . . 15 (((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ ∀𝑗𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛𝐼) → 𝑁 ∈ Fin)
69 simp-4r 806 . . . . . . . . . . . . . . 15 (((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ ∀𝑗𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛𝐼) → 𝑀 ∈ Fin)
70 simpr 477 . . . . . . . . . . . . . . 15 (((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ ∀𝑗𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛𝐼) → 𝑛𝐼)
7168, 69, 703jca 1240 . . . . . . . . . . . . . 14 (((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ ∀𝑗𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛𝐼) → (𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝑛𝐼))
7271adantr 481 . . . . . . . . . . . . 13 ((((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ ∀𝑗𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛𝐼) ∧ (𝐶𝑛) = (𝑅𝑛)) → (𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝑛𝐼))
73 simp-4r 806 . . . . . . . . . . . . 13 ((((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ ∀𝑗𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛𝐼) ∧ (𝐶𝑛) = (𝑅𝑛)) → ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌)))
74 simpr 477 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ ∀𝑗𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) → ∀𝑗𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗))
7574adantr 481 . . . . . . . . . . . . . 14 (((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ ∀𝑗𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛𝐼) → ∀𝑗𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗))
7675anim1i 591 . . . . . . . . . . . . 13 ((((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ ∀𝑗𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛𝐼) ∧ (𝐶𝑛) = (𝑅𝑛)) → (∀𝑗𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗) ∧ (𝐶𝑛) = (𝑅𝑛)))
77 gsmsymgrfix.s . . . . . . . . . . . . . . 15 𝑆 = (SymGrp‘𝑁)
78 gsmsymgrfix.b . . . . . . . . . . . . . . 15 𝐵 = (Base‘𝑆)
79 gsmsymgreq.z . . . . . . . . . . . . . . 15 𝑍 = (SymGrp‘𝑀)
80 gsmsymgreq.p . . . . . . . . . . . . . . 15 𝑃 = (Base‘𝑍)
81 gsmsymgreq.i . . . . . . . . . . . . . . 15 𝐼 = (𝑁𝑀)
8277, 78, 79, 80, 81gsmsymgreqlem1 17771 . . . . . . . . . . . . . 14 (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝑛𝐼) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) → ((∀𝑗𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗) ∧ (𝐶𝑛) = (𝑅𝑛)) → ((𝑆 Σg (𝑋 ++ ⟨“𝐶”⟩))‘𝑛) = ((𝑍 Σg (𝑌 ++ ⟨“𝑅”⟩))‘𝑛)))
8382imp 445 . . . . . . . . . . . . 13 ((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝑛𝐼) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ (∀𝑗𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗) ∧ (𝐶𝑛) = (𝑅𝑛))) → ((𝑆 Σg (𝑋 ++ ⟨“𝐶”⟩))‘𝑛) = ((𝑍 Σg (𝑌 ++ ⟨“𝑅”⟩))‘𝑛))
8472, 73, 76, 83syl21anc 1322 . . . . . . . . . . . 12 ((((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ ∀𝑗𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛𝐼) ∧ (𝐶𝑛) = (𝑅𝑛)) → ((𝑆 Σg (𝑋 ++ ⟨“𝐶”⟩))‘𝑛) = ((𝑍 Σg (𝑌 ++ ⟨“𝑅”⟩))‘𝑛))
8584ex 450 . . . . . . . . . . 11 (((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ ∀𝑗𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛𝐼) → ((𝐶𝑛) = (𝑅𝑛) → ((𝑆 Σg (𝑋 ++ ⟨“𝐶”⟩))‘𝑛) = ((𝑍 Σg (𝑌 ++ ⟨“𝑅”⟩))‘𝑛)))
8685ralimdva 2956 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ ∀𝑗𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) → (∀𝑛𝐼 (𝐶𝑛) = (𝑅𝑛) → ∀𝑛𝐼 ((𝑆 Σg (𝑋 ++ ⟨“𝐶”⟩))‘𝑛) = ((𝑍 Σg (𝑌 ++ ⟨“𝑅”⟩))‘𝑛)))
8786expcom 451 . . . . . . . . 9 (∀𝑗𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗) → (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) → (∀𝑛𝐼 (𝐶𝑛) = (𝑅𝑛) → ∀𝑛𝐼 ((𝑆 Σg (𝑋 ++ ⟨“𝐶”⟩))‘𝑛) = ((𝑍 Σg (𝑌 ++ ⟨“𝑅”⟩))‘𝑛))))
8867, 87sylbi 207 . . . . . . . 8 (∀𝑛𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛) → (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) → (∀𝑛𝐼 (𝐶𝑛) = (𝑅𝑛) → ∀𝑛𝐼 ((𝑆 Σg (𝑋 ++ ⟨“𝐶”⟩))‘𝑛) = ((𝑍 Σg (𝑌 ++ ⟨“𝑅”⟩))‘𝑛))))
8988com23 86 . . . . . . 7 (∀𝑛𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛) → (∀𝑛𝐼 (𝐶𝑛) = (𝑅𝑛) → (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) → ∀𝑛𝐼 ((𝑆 Σg (𝑋 ++ ⟨“𝐶”⟩))‘𝑛) = ((𝑍 Σg (𝑌 ++ ⟨“𝑅”⟩))‘𝑛))))
9063, 89syl 17 . . . . . 6 ((∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛𝐼 ((𝑋𝑖)‘𝑛) = ((𝑌𝑖)‘𝑛) ∧ (∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛𝐼 ((𝑋𝑖)‘𝑛) = ((𝑌𝑖)‘𝑛) → ∀𝑛𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛))) → (∀𝑛𝐼 (𝐶𝑛) = (𝑅𝑛) → (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) → ∀𝑛𝐼 ((𝑆 Σg (𝑋 ++ ⟨“𝐶”⟩))‘𝑛) = ((𝑍 Σg (𝑌 ++ ⟨“𝑅”⟩))‘𝑛))))
9190impancom 456 . . . . 5 ((∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛𝐼 ((𝑋𝑖)‘𝑛) = ((𝑌𝑖)‘𝑛) ∧ ∀𝑛𝐼 (𝐶𝑛) = (𝑅𝑛)) → ((∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛𝐼 ((𝑋𝑖)‘𝑛) = ((𝑌𝑖)‘𝑛) → ∀𝑛𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛)) → (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) → ∀𝑛𝐼 ((𝑆 Σg (𝑋 ++ ⟨“𝐶”⟩))‘𝑛) = ((𝑍 Σg (𝑌 ++ ⟨“𝑅”⟩))‘𝑛))))
9291com13 88 . . . 4 (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) → ((∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛𝐼 ((𝑋𝑖)‘𝑛) = ((𝑌𝑖)‘𝑛) → ∀𝑛𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛)) → ((∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛𝐼 ((𝑋𝑖)‘𝑛) = ((𝑌𝑖)‘𝑛) ∧ ∀𝑛𝐼 (𝐶𝑛) = (𝑅𝑛)) → ∀𝑛𝐼 ((𝑆 Σg (𝑋 ++ ⟨“𝐶”⟩))‘𝑛) = ((𝑍 Σg (𝑌 ++ ⟨“𝑅”⟩))‘𝑛))))
9392imp 445 . . 3 ((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ (∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛𝐼 ((𝑋𝑖)‘𝑛) = ((𝑌𝑖)‘𝑛) → ∀𝑛𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛))) → ((∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛𝐼 ((𝑋𝑖)‘𝑛) = ((𝑌𝑖)‘𝑛) ∧ ∀𝑛𝐼 (𝐶𝑛) = (𝑅𝑛)) → ∀𝑛𝐼 ((𝑆 Σg (𝑋 ++ ⟨“𝐶”⟩))‘𝑛) = ((𝑍 Σg (𝑌 ++ ⟨“𝑅”⟩))‘𝑛)))
9462, 93sylbid 230 . 2 ((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ (∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛𝐼 ((𝑋𝑖)‘𝑛) = ((𝑌𝑖)‘𝑛) → ∀𝑛𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛))) → (∀𝑖 ∈ (0..^(#‘(𝑋 ++ ⟨“𝐶”⟩)))∀𝑛𝐼 (((𝑋 ++ ⟨“𝐶”⟩)‘𝑖)‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘𝑖)‘𝑛) → ∀𝑛𝐼 ((𝑆 Σg (𝑋 ++ ⟨“𝐶”⟩))‘𝑛) = ((𝑍 Σg (𝑌 ++ ⟨“𝑅”⟩))‘𝑛)))
9594ex 450 1 (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵𝐶𝐵) ∧ (𝑌 ∈ Word 𝑃𝑅𝑃) ∧ (#‘𝑋) = (#‘𝑌))) → ((∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛𝐼 ((𝑋𝑖)‘𝑛) = ((𝑌𝑖)‘𝑛) → ∀𝑛𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛)) → (∀𝑖 ∈ (0..^(#‘(𝑋 ++ ⟨“𝐶”⟩)))∀𝑛𝐼 (((𝑋 ++ ⟨“𝐶”⟩)‘𝑖)‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘𝑖)‘𝑛) → ∀𝑛𝐼 ((𝑆 Σg (𝑋 ++ ⟨“𝐶”⟩))‘𝑛) = ((𝑍 Σg (𝑌 ++ ⟨“𝑅”⟩))‘𝑛))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wral 2907  cun 3553  cin 3554  {csn 4148  cfv 5847  (class class class)co 6604  Fincfn 7899  0cc0 9880  1c1 9881   + caddc 9883  0cn0 11236  cuz 11631  ..^cfzo 12406  #chash 13057  Word cword 13230   ++ cconcat 13232  ⟨“cs1 13233  Basecbs 15781   Σg cgsu 16022  SymGrpcsymg 17718
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-oadd 7509  df-er 7687  df-map 7804  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-card 8709  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-nn 10965  df-2 11023  df-3 11024  df-4 11025  df-5 11026  df-6 11027  df-7 11028  df-8 11029  df-9 11030  df-n0 11237  df-z 11322  df-uz 11632  df-fz 12269  df-fzo 12407  df-seq 12742  df-hash 13058  df-word 13238  df-concat 13240  df-s1 13241  df-struct 15783  df-ndx 15784  df-slot 15785  df-base 15786  df-sets 15787  df-ress 15788  df-plusg 15875  df-tset 15881  df-0g 16023  df-gsum 16024  df-mgm 17163  df-sgrp 17205  df-mnd 17216  df-submnd 17257  df-grp 17346  df-symg 17719
This theorem is referenced by:  gsmsymgreq  17773
  Copyright terms: Public domain W3C validator