Metamath Proof Explorer

Definition df-gfoo

Description: Define the Galois field of order p ^ +oo , as a direct limit of the Galois finite fields. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Assertion df-gfoo GF∞ = ( 𝑝 ∈ ℙ ↦ ⦋ ( ℤ/nℤ ‘ 𝑝 ) / 𝑟 ⦌ ( 𝑟 polySplitLim ( 𝑛 ∈ ℕ ↦ { ⦋ ( Poly1 ‘ 𝑟 ) / 𝑠 ⦌ ⦋ ( var1 ‘ 𝑟 ) / 𝑥 ⦌ ( ( ( 𝑝 ↑ 𝑛 ) ( .g ‘ ( mulGrp ‘ 𝑠 ) ) 𝑥 ) ( -g ‘ 𝑠 ) 𝑥 ) } ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgfo ⊢ GF∞
1 vp ⊢ 𝑝
2 cprime ⊢ ℙ
3 czn ⊢ ℤ/nℤ
4 1 cv ⊢ 𝑝
5 4 3 cfv ⊢ ( ℤ/nℤ ‘ 𝑝 )
6 vr ⊢ 𝑟
7 6 cv ⊢ 𝑟
8 cpsl ⊢ polySplitLim
9 vn ⊢ 𝑛
10 cn ⊢ ℕ
11 cpl1 ⊢ Poly1
12 7 11 cfv ⊢ ( Poly1 ‘ 𝑟 )
13 vs ⊢ 𝑠
14 cv1 ⊢ var1
15 7 14 cfv ⊢ ( var1 ‘ 𝑟 )
16 vx ⊢ 𝑥
17 cexp ⊢ ↑
18 9 cv ⊢ 𝑛
19 4 18 17 co ⊢ ( 𝑝 ↑ 𝑛 )
20 cmg ⊢ .g
21 cmgp ⊢ mulGrp
22 13 cv ⊢ 𝑠
23 22 21 cfv ⊢ ( mulGrp ‘ 𝑠 )
24 23 20 cfv ⊢ ( .g ‘ ( mulGrp ‘ 𝑠 ) )
25 16 cv ⊢ 𝑥
26 19 25 24 co ⊢ ( ( 𝑝 ↑ 𝑛 ) ( .g ‘ ( mulGrp ‘ 𝑠 ) ) 𝑥 )
27 csg ⊢ -g
28 22 27 cfv ⊢ ( -g ‘ 𝑠 )
29 26 25 28 co ⊢ ( ( ( 𝑝 ↑ 𝑛 ) ( .g ‘ ( mulGrp ‘ 𝑠 ) ) 𝑥 ) ( -g ‘ 𝑠 ) 𝑥 )
30 16 15 29 csb ⊢ ⦋ ( var1 ‘ 𝑟 ) / 𝑥 ⦌ ( ( ( 𝑝 ↑ 𝑛 ) ( .g ‘ ( mulGrp ‘ 𝑠 ) ) 𝑥 ) ( -g ‘ 𝑠 ) 𝑥 )
31 13 12 30 csb ⊢ ⦋ ( Poly1 ‘ 𝑟 ) / 𝑠 ⦌ ⦋ ( var1 ‘ 𝑟 ) / 𝑥 ⦌ ( ( ( 𝑝 ↑ 𝑛 ) ( .g ‘ ( mulGrp ‘ 𝑠 ) ) 𝑥 ) ( -g ‘ 𝑠 ) 𝑥 )
32 31 csn ⊢ { ⦋ ( Poly1 ‘ 𝑟 ) / 𝑠 ⦌ ⦋ ( var1 ‘ 𝑟 ) / 𝑥 ⦌ ( ( ( 𝑝 ↑ 𝑛 ) ( .g ‘ ( mulGrp ‘ 𝑠 ) ) 𝑥 ) ( -g ‘ 𝑠 ) 𝑥 ) }
33 9 10 32 cmpt ⊢ ( 𝑛 ∈ ℕ ↦ { ⦋ ( Poly1 ‘ 𝑟 ) / 𝑠 ⦌ ⦋ ( var1 ‘ 𝑟 ) / 𝑥 ⦌ ( ( ( 𝑝 ↑ 𝑛 ) ( .g ‘ ( mulGrp ‘ 𝑠 ) ) 𝑥 ) ( -g ‘ 𝑠 ) 𝑥 ) } )
34 7 33 8 co ⊢ ( 𝑟 polySplitLim ( 𝑛 ∈ ℕ ↦ { ⦋ ( Poly1 ‘ 𝑟 ) / 𝑠 ⦌ ⦋ ( var1 ‘ 𝑟 ) / 𝑥 ⦌ ( ( ( 𝑝 ↑ 𝑛 ) ( .g ‘ ( mulGrp ‘ 𝑠 ) ) 𝑥 ) ( -g ‘ 𝑠 ) 𝑥 ) } ) )
35 6 5 34 csb ⊢ ⦋ ( ℤ/nℤ ‘ 𝑝 ) / 𝑟 ⦌ ( 𝑟 polySplitLim ( 𝑛 ∈ ℕ ↦ { ⦋ ( Poly1 ‘ 𝑟 ) / 𝑠 ⦌ ⦋ ( var1 ‘ 𝑟 ) / 𝑥 ⦌ ( ( ( 𝑝 ↑ 𝑛 ) ( .g ‘ ( mulGrp ‘ 𝑠 ) ) 𝑥 ) ( -g ‘ 𝑠 ) 𝑥 ) } ) )
36 1 2 35 cmpt ⊢ ( 𝑝 ∈ ℙ ↦ ⦋ ( ℤ/nℤ ‘ 𝑝 ) / 𝑟 ⦌ ( 𝑟 polySplitLim ( 𝑛 ∈ ℕ ↦ { ⦋ ( Poly1 ‘ 𝑟 ) / 𝑠 ⦌ ⦋ ( var1 ‘ 𝑟 ) / 𝑥 ⦌ ( ( ( 𝑝 ↑ 𝑛 ) ( .g ‘ ( mulGrp ‘ 𝑠 ) ) 𝑥 ) ( -g ‘ 𝑠 ) 𝑥 ) } ) ) )
37 0 36 wceq ⊢ GF∞ = ( 𝑝 ∈ ℙ ↦ ⦋ ( ℤ/nℤ ‘ 𝑝 ) / 𝑟 ⦌ ( 𝑟 polySplitLim ( 𝑛 ∈ ℕ ↦ { ⦋ ( Poly1 ‘ 𝑟 ) / 𝑠 ⦌ ⦋ ( var1 ‘ 𝑟 ) / 𝑥 ⦌ ( ( ( 𝑝 ↑ 𝑛 ) ( .g ‘ ( mulGrp ‘ 𝑠 ) ) 𝑥 ) ( -g ‘ 𝑠 ) 𝑥 ) } ) ) )