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

Theorem frgpnabllem2 18201
 Description: Lemma for frgpnabl 18202. (Contributed by Mario Carneiro, 21-Apr-2016.)
Hypotheses
Ref Expression
frgpnabl.g 𝐺 = (freeGrp‘𝐼)
frgpnabl.w 𝑊 = ( I ‘Word (𝐼 × 2𝑜))
frgpnabl.r = ( ~FG𝐼)
frgpnabl.p + = (+g𝐺)
frgpnabl.m 𝑀 = (𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)
frgpnabl.t 𝑇 = (𝑣𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀𝑤)”⟩⟩)))
frgpnabl.d 𝐷 = (𝑊 𝑥𝑊 ran (𝑇𝑥))
frgpnabl.u 𝑈 = (varFGrp𝐼)
frgpnabl.i (𝜑𝐼 ∈ V)
frgpnabl.a (𝜑𝐴𝐼)
frgpnabl.b (𝜑𝐵𝐼)
frgpnabl.n (𝜑 → ((𝑈𝐴) + (𝑈𝐵)) = ((𝑈𝐵) + (𝑈𝐴)))
Assertion
Ref Expression
frgpnabllem2 (𝜑𝐴 = 𝐵)
Distinct variable groups:   𝑥,𝐴   𝑣,𝑛,𝑤,𝑥,𝑦,𝑧,𝐼   𝜑,𝑥   𝑥, ,𝑦,𝑧   𝑥,𝐵   𝑛,𝑊,𝑣,𝑤,𝑥,𝑦,𝑧   𝑥,𝐺   𝑛,𝑀,𝑣,𝑤,𝑥   𝑥,𝑇
Allowed substitution hints:   𝜑(𝑦,𝑧,𝑤,𝑣,𝑛)   𝐴(𝑦,𝑧,𝑤,𝑣,𝑛)   𝐵(𝑦,𝑧,𝑤,𝑣,𝑛)   𝐷(𝑥,𝑦,𝑧,𝑤,𝑣,𝑛)   + (𝑥,𝑦,𝑧,𝑤,𝑣,𝑛)   (𝑤,𝑣,𝑛)   𝑇(𝑦,𝑧,𝑤,𝑣,𝑛)   𝑈(𝑥,𝑦,𝑧,𝑤,𝑣,𝑛)   𝐺(𝑦,𝑧,𝑤,𝑣,𝑛)   𝑀(𝑦,𝑧)

Proof of Theorem frgpnabllem2
Dummy variables 𝑑 𝑚 𝑡 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frgpnabl.a . 2 (𝜑𝐴𝐼)
2 0ex 4752 . . 3 ∅ ∈ V
32a1i 11 . 2 (𝜑 → ∅ ∈ V)
4 frgpnabl.d . . . . . . . 8 𝐷 = (𝑊 𝑥𝑊 ran (𝑇𝑥))
5 difss 3717 . . . . . . . 8 (𝑊 𝑥𝑊 ran (𝑇𝑥)) ⊆ 𝑊
64, 5eqsstri 3616 . . . . . . 7 𝐷𝑊
7 inss1 3813 . . . . . . . 8 (𝐷 ∩ ((𝑈𝐵) + (𝑈𝐴))) ⊆ 𝐷
8 frgpnabl.g . . . . . . . . 9 𝐺 = (freeGrp‘𝐼)
9 frgpnabl.w . . . . . . . . 9 𝑊 = ( I ‘Word (𝐼 × 2𝑜))
10 frgpnabl.r . . . . . . . . 9 = ( ~FG𝐼)
11 frgpnabl.p . . . . . . . . 9 + = (+g𝐺)
12 frgpnabl.m . . . . . . . . 9 𝑀 = (𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)
13 frgpnabl.t . . . . . . . . 9 𝑇 = (𝑣𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀𝑤)”⟩⟩)))
14 frgpnabl.u . . . . . . . . 9 𝑈 = (varFGrp𝐼)
15 frgpnabl.i . . . . . . . . 9 (𝜑𝐼 ∈ V)
16 frgpnabl.b . . . . . . . . 9 (𝜑𝐵𝐼)
178, 9, 10, 11, 12, 13, 4, 14, 15, 16, 1frgpnabllem1 18200 . . . . . . . 8 (𝜑 → ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩ ∈ (𝐷 ∩ ((𝑈𝐵) + (𝑈𝐴))))
187, 17sseldi 3582 . . . . . . 7 (𝜑 → ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩ ∈ 𝐷)
196, 18sseldi 3582 . . . . . 6 (𝜑 → ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩ ∈ 𝑊)
20 eqid 2621 . . . . . . 7 (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1)))
219, 10, 12, 13, 4, 20efgredeu 18089 . . . . . 6 (⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩ ∈ 𝑊 → ∃!𝑑𝐷 𝑑 ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩)
22 reurmo 3150 . . . . . 6 (∃!𝑑𝐷 𝑑 ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩ → ∃*𝑑𝐷 𝑑 ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩)
2319, 21, 223syl 18 . . . . 5 (𝜑 → ∃*𝑑𝐷 𝑑 ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩)
24 inss1 3813 . . . . . 6 (𝐷 ∩ ((𝑈𝐴) + (𝑈𝐵))) ⊆ 𝐷
258, 9, 10, 11, 12, 13, 4, 14, 15, 1, 16frgpnabllem1 18200 . . . . . 6 (𝜑 → ⟨“⟨𝐴, ∅⟩⟨𝐵, ∅⟩”⟩ ∈ (𝐷 ∩ ((𝑈𝐴) + (𝑈𝐵))))
2624, 25sseldi 3582 . . . . 5 (𝜑 → ⟨“⟨𝐴, ∅⟩⟨𝐵, ∅⟩”⟩ ∈ 𝐷)
279, 10efger 18055 . . . . . . . . 9 Er 𝑊
2827a1i 11 . . . . . . . 8 (𝜑 Er 𝑊)
298frgpgrp 18099 . . . . . . . . . . 11 (𝐼 ∈ V → 𝐺 ∈ Grp)
3015, 29syl 17 . . . . . . . . . 10 (𝜑𝐺 ∈ Grp)
31 eqid 2621 . . . . . . . . . . . . 13 (Base‘𝐺) = (Base‘𝐺)
3210, 14, 8, 31vrgpf 18105 . . . . . . . . . . . 12 (𝐼 ∈ V → 𝑈:𝐼⟶(Base‘𝐺))
3315, 32syl 17 . . . . . . . . . . 11 (𝜑𝑈:𝐼⟶(Base‘𝐺))
3433, 1ffvelrnd 6318 . . . . . . . . . 10 (𝜑 → (𝑈𝐴) ∈ (Base‘𝐺))
3533, 16ffvelrnd 6318 . . . . . . . . . 10 (𝜑 → (𝑈𝐵) ∈ (Base‘𝐺))
3631, 11grpcl 17354 . . . . . . . . . 10 ((𝐺 ∈ Grp ∧ (𝑈𝐴) ∈ (Base‘𝐺) ∧ (𝑈𝐵) ∈ (Base‘𝐺)) → ((𝑈𝐴) + (𝑈𝐵)) ∈ (Base‘𝐺))
3730, 34, 35, 36syl3anc 1323 . . . . . . . . 9 (𝜑 → ((𝑈𝐴) + (𝑈𝐵)) ∈ (Base‘𝐺))
38 eqid 2621 . . . . . . . . . . . 12 (freeMnd‘(𝐼 × 2𝑜)) = (freeMnd‘(𝐼 × 2𝑜))
398, 38, 10frgpval 18095 . . . . . . . . . . 11 (𝐼 ∈ V → 𝐺 = ((freeMnd‘(𝐼 × 2𝑜)) /s ))
4015, 39syl 17 . . . . . . . . . 10 (𝜑𝐺 = ((freeMnd‘(𝐼 × 2𝑜)) /s ))
41 2on 7516 . . . . . . . . . . . . . 14 2𝑜 ∈ On
42 xpexg 6916 . . . . . . . . . . . . . 14 ((𝐼 ∈ V ∧ 2𝑜 ∈ On) → (𝐼 × 2𝑜) ∈ V)
4315, 41, 42sylancl 693 . . . . . . . . . . . . 13 (𝜑 → (𝐼 × 2𝑜) ∈ V)
44 wrdexg 13257 . . . . . . . . . . . . 13 ((𝐼 × 2𝑜) ∈ V → Word (𝐼 × 2𝑜) ∈ V)
45 fvi 6214 . . . . . . . . . . . . 13 (Word (𝐼 × 2𝑜) ∈ V → ( I ‘Word (𝐼 × 2𝑜)) = Word (𝐼 × 2𝑜))
4643, 44, 453syl 18 . . . . . . . . . . . 12 (𝜑 → ( I ‘Word (𝐼 × 2𝑜)) = Word (𝐼 × 2𝑜))
479, 46syl5eq 2667 . . . . . . . . . . 11 (𝜑𝑊 = Word (𝐼 × 2𝑜))
48 eqid 2621 . . . . . . . . . . . . 13 (Base‘(freeMnd‘(𝐼 × 2𝑜))) = (Base‘(freeMnd‘(𝐼 × 2𝑜)))
4938, 48frmdbas 17313 . . . . . . . . . . . 12 ((𝐼 × 2𝑜) ∈ V → (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word (𝐼 × 2𝑜))
5043, 49syl 17 . . . . . . . . . . 11 (𝜑 → (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word (𝐼 × 2𝑜))
5147, 50eqtr4d 2658 . . . . . . . . . 10 (𝜑𝑊 = (Base‘(freeMnd‘(𝐼 × 2𝑜))))
52 fvex 6160 . . . . . . . . . . . 12 ( ~FG𝐼) ∈ V
5310, 52eqeltri 2694 . . . . . . . . . . 11 ∈ V
5453a1i 11 . . . . . . . . . 10 (𝜑 ∈ V)
55 fvex 6160 . . . . . . . . . . 11 (freeMnd‘(𝐼 × 2𝑜)) ∈ V
5655a1i 11 . . . . . . . . . 10 (𝜑 → (freeMnd‘(𝐼 × 2𝑜)) ∈ V)
5740, 51, 54, 56qusbas 16129 . . . . . . . . 9 (𝜑 → (𝑊 / ) = (Base‘𝐺))
5837, 57eleqtrrd 2701 . . . . . . . 8 (𝜑 → ((𝑈𝐴) + (𝑈𝐵)) ∈ (𝑊 / ))
59 inss2 3814 . . . . . . . . 9 (𝐷 ∩ ((𝑈𝐴) + (𝑈𝐵))) ⊆ ((𝑈𝐴) + (𝑈𝐵))
6059, 25sseldi 3582 . . . . . . . 8 (𝜑 → ⟨“⟨𝐴, ∅⟩⟨𝐵, ∅⟩”⟩ ∈ ((𝑈𝐴) + (𝑈𝐵)))
61 qsel 7774 . . . . . . . 8 (( Er 𝑊 ∧ ((𝑈𝐴) + (𝑈𝐵)) ∈ (𝑊 / ) ∧ ⟨“⟨𝐴, ∅⟩⟨𝐵, ∅⟩”⟩ ∈ ((𝑈𝐴) + (𝑈𝐵))) → ((𝑈𝐴) + (𝑈𝐵)) = [⟨“⟨𝐴, ∅⟩⟨𝐵, ∅⟩”⟩] )
6228, 58, 60, 61syl3anc 1323 . . . . . . 7 (𝜑 → ((𝑈𝐴) + (𝑈𝐵)) = [⟨“⟨𝐴, ∅⟩⟨𝐵, ∅⟩”⟩] )
63 inss2 3814 . . . . . . . . . 10 (𝐷 ∩ ((𝑈𝐵) + (𝑈𝐴))) ⊆ ((𝑈𝐵) + (𝑈𝐴))
6463, 17sseldi 3582 . . . . . . . . 9 (𝜑 → ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩ ∈ ((𝑈𝐵) + (𝑈𝐴)))
65 frgpnabl.n . . . . . . . . 9 (𝜑 → ((𝑈𝐴) + (𝑈𝐵)) = ((𝑈𝐵) + (𝑈𝐴)))
6664, 65eleqtrrd 2701 . . . . . . . 8 (𝜑 → ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩ ∈ ((𝑈𝐴) + (𝑈𝐵)))
67 qsel 7774 . . . . . . . 8 (( Er 𝑊 ∧ ((𝑈𝐴) + (𝑈𝐵)) ∈ (𝑊 / ) ∧ ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩ ∈ ((𝑈𝐴) + (𝑈𝐵))) → ((𝑈𝐴) + (𝑈𝐵)) = [⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩] )
6828, 58, 66, 67syl3anc 1323 . . . . . . 7 (𝜑 → ((𝑈𝐴) + (𝑈𝐵)) = [⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩] )
6962, 68eqtr3d 2657 . . . . . 6 (𝜑 → [⟨“⟨𝐴, ∅⟩⟨𝐵, ∅⟩”⟩] = [⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩] )
706, 26sseldi 3582 . . . . . . 7 (𝜑 → ⟨“⟨𝐴, ∅⟩⟨𝐵, ∅⟩”⟩ ∈ 𝑊)
7128, 70erth 7739 . . . . . 6 (𝜑 → (⟨“⟨𝐴, ∅⟩⟨𝐵, ∅⟩”⟩ ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩ ↔ [⟨“⟨𝐴, ∅⟩⟨𝐵, ∅⟩”⟩] = [⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩] ))
7269, 71mpbird 247 . . . . 5 (𝜑 → ⟨“⟨𝐴, ∅⟩⟨𝐵, ∅⟩”⟩ ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩)
7328, 19erref 7710 . . . . 5 (𝜑 → ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩ ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩)
74 breq1 4618 . . . . . 6 (𝑑 = ⟨“⟨𝐴, ∅⟩⟨𝐵, ∅⟩”⟩ → (𝑑 ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩ ↔ ⟨“⟨𝐴, ∅⟩⟨𝐵, ∅⟩”⟩ ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩))
75 breq1 4618 . . . . . 6 (𝑑 = ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩ → (𝑑 ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩ ↔ ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩ ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩))
7674, 75rmoi 3512 . . . . 5 ((∃*𝑑𝐷 𝑑 ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩ ∧ (⟨“⟨𝐴, ∅⟩⟨𝐵, ∅⟩”⟩ ∈ 𝐷 ∧ ⟨“⟨𝐴, ∅⟩⟨𝐵, ∅⟩”⟩ ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩) ∧ (⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩ ∈ 𝐷 ∧ ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩ ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩)) → ⟨“⟨𝐴, ∅⟩⟨𝐵, ∅⟩”⟩ = ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩)
7723, 26, 72, 18, 73, 76syl122anc 1332 . . . 4 (𝜑 → ⟨“⟨𝐴, ∅⟩⟨𝐵, ∅⟩”⟩ = ⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩)
7877fveq1d 6152 . . 3 (𝜑 → (⟨“⟨𝐴, ∅⟩⟨𝐵, ∅⟩”⟩‘0) = (⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩‘0))
79 opex 4895 . . . 4 𝐴, ∅⟩ ∈ V
80 s2fv0 13571 . . . 4 (⟨𝐴, ∅⟩ ∈ V → (⟨“⟨𝐴, ∅⟩⟨𝐵, ∅⟩”⟩‘0) = ⟨𝐴, ∅⟩)
8179, 80ax-mp 5 . . 3 (⟨“⟨𝐴, ∅⟩⟨𝐵, ∅⟩”⟩‘0) = ⟨𝐴, ∅⟩
82 opex 4895 . . . 4 𝐵, ∅⟩ ∈ V
83 s2fv0 13571 . . . 4 (⟨𝐵, ∅⟩ ∈ V → (⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩‘0) = ⟨𝐵, ∅⟩)
8482, 83ax-mp 5 . . 3 (⟨“⟨𝐵, ∅⟩⟨𝐴, ∅⟩”⟩‘0) = ⟨𝐵, ∅⟩
8578, 81, 843eqtr3g 2678 . 2 (𝜑 → ⟨𝐴, ∅⟩ = ⟨𝐵, ∅⟩)
86 opthg 4908 . . 3 ((𝐴𝐼 ∧ ∅ ∈ V) → (⟨𝐴, ∅⟩ = ⟨𝐵, ∅⟩ ↔ (𝐴 = 𝐵 ∧ ∅ = ∅)))
8786simprbda 652 . 2 (((𝐴𝐼 ∧ ∅ ∈ V) ∧ ⟨𝐴, ∅⟩ = ⟨𝐵, ∅⟩) → 𝐴 = 𝐵)
881, 3, 85, 87syl21anc 1322 1 (𝜑𝐴 = 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   = wceq 1480   ∈ wcel 1987  ∀wral 2907  ∃!wreu 2909  ∃*wrmo 2910  {crab 2911  Vcvv 3186   ∖ cdif 3553   ∩ cin 3555  ∅c0 3893  {csn 4150  ⟨cop 4156  ⟨cotp 4158  ∪ ciun 4487   class class class wbr 4615   ↦ cmpt 4675   I cid 4986   × cxp 5074  ran crn 5077  Oncon0 5684  ⟶wf 5845  ‘cfv 5849  (class class class)co 6607   ↦ cmpt2 6609  1𝑜c1o 7501  2𝑜c2o 7502   Er wer 7687  [cec 7688   / cqs 7689  0cc0 9883  1c1 9884   − cmin 10213  ...cfz 12271  ..^cfzo 12409  #chash 13060  Word cword 13233   splice csplice 13238  ⟨“cs2 13526  Basecbs 15784  +gcplusg 15865   /s cqus 16089  freeMndcfrmd 17308  Grpcgrp 17346   ~FG cefg 18043  freeGrpcfrgp 18044  varFGrpcvrgp 18045 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 4733  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905  ax-cnex 9939  ax-resscn 9940  ax-1cn 9941  ax-icn 9942  ax-addcl 9943  ax-addrcl 9944  ax-mulcl 9945  ax-mulrcl 9946  ax-mulcom 9947  ax-addass 9948  ax-mulass 9949  ax-distr 9950  ax-i2m1 9951  ax-1ne0 9952  ax-1rid 9953  ax-rnegex 9954  ax-rrecex 9955  ax-cnre 9956  ax-pre-lttri 9957  ax-pre-lttrn 9958  ax-pre-ltadd 9959  ax-pre-mulgt0 9960 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 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-pss 3572  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-tp 4155  df-op 4157  df-ot 4159  df-uni 4405  df-int 4443  df-iun 4489  df-iin 4490  df-br 4616  df-opab 4676  df-mpt 4677  df-tr 4715  df-eprel 4987  df-id 4991  df-po 4997  df-so 4998  df-fr 5035  df-we 5037  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-pred 5641  df-ord 5687  df-on 5688  df-lim 5689  df-suc 5690  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-riota 6568  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-om 7016  df-1st 7116  df-2nd 7117  df-wrecs 7355  df-recs 7416  df-rdg 7454  df-1o 7508  df-2o 7509  df-oadd 7512  df-er 7690  df-ec 7692  df-qs 7696  df-map 7807  df-pm 7808  df-en 7903  df-dom 7904  df-sdom 7905  df-fin 7906  df-sup 8295  df-inf 8296  df-card 8712  df-pnf 10023  df-mnf 10024  df-xr 10025  df-ltxr 10026  df-le 10027  df-sub 10215  df-neg 10216  df-nn 10968  df-2 11026  df-3 11027  df-4 11028  df-5 11029  df-6 11030  df-7 11031  df-8 11032  df-9 11033  df-n0 11240  df-xnn0 11311  df-z 11325  df-dec 11441  df-uz 11635  df-rp 11780  df-fz 12272  df-fzo 12410  df-hash 13061  df-word 13241  df-lsw 13242  df-concat 13243  df-s1 13244  df-substr 13245  df-splice 13246  df-reverse 13247  df-s2 13533  df-struct 15786  df-ndx 15787  df-slot 15788  df-base 15789  df-plusg 15878  df-mulr 15879  df-sca 15881  df-vsca 15882  df-ip 15883  df-tset 15884  df-ple 15885  df-ds 15888  df-0g 16026  df-imas 16092  df-qus 16093  df-mgm 17166  df-sgrp 17208  df-mnd 17219  df-frmd 17310  df-grp 17349  df-efg 18046  df-frgp 18047  df-vrgp 18048 This theorem is referenced by:  frgpnabl  18202
 Copyright terms: Public domain W3C validator