Metamath Proof Explorer

Theorem lgsqrlem3

Description: Lemma for lgsqr . (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypotheses lgsqr.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑃 )
lgsqr.s ⊢ 𝑆 = ( Poly1 ‘ 𝑌 )
lgsqr.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
lgsqr.d ⊢ 𝐷 = ( deg1 ‘ 𝑌 )
lgsqr.o ⊢ 𝑂 = ( eval1 ‘ 𝑌 )
lgsqr.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑆 ) )
lgsqr.x ⊢ 𝑋 = ( var1 ‘ 𝑌 )
lgsqr.m ⊢ − = ( -g ‘ 𝑆 )
lgsqr.u ⊢ 1 = ( 1r ‘ 𝑆 )
lgsqr.t ⊢ 𝑇 = ( ( ( ( 𝑃 − 1 ) / 2 ) ↑ 𝑋 ) − 1 )
lgsqr.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
lgsqr.1 ⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
lgsqr.g ⊢ 𝐺 = ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) )
lgsqr.3 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
lgsqr.4 ⊢ ( 𝜑 → ( 𝐴 /L 𝑃 ) = 1 )
Assertion lgsqrlem3 ( 𝜑 → ( 𝐿 ‘ 𝐴 ) ∈ ( ◡ ( 𝑂 ‘ 𝑇 ) “ { ( 0g ‘ 𝑌 ) } ) )

Proof

Step Hyp Ref Expression
1 lgsqr.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑃 )
2 lgsqr.s ⊢ 𝑆 = ( Poly1 ‘ 𝑌 )
3 lgsqr.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
4 lgsqr.d ⊢ 𝐷 = ( deg1 ‘ 𝑌 )
5 lgsqr.o ⊢ 𝑂 = ( eval1 ‘ 𝑌 )
6 lgsqr.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑆 ) )
7 lgsqr.x ⊢ 𝑋 = ( var1 ‘ 𝑌 )
8 lgsqr.m ⊢ − = ( -g ‘ 𝑆 )
9 lgsqr.u ⊢ 1 = ( 1r ‘ 𝑆 )
10 lgsqr.t ⊢ 𝑇 = ( ( ( ( 𝑃 − 1 ) / 2 ) ↑ 𝑋 ) − 1 )
11 lgsqr.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
12 lgsqr.1 ⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
13 lgsqr.g ⊢ 𝐺 = ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) )
14 lgsqr.3 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
15 lgsqr.4 ⊢ ( 𝜑 → ( 𝐴 /L 𝑃 ) = 1 )
16 12 eldifad ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
17 1 znfld ⊢ ( 𝑃 ∈ ℙ → 𝑌 ∈ Field )
18 16 17 syl ⊢ ( 𝜑 → 𝑌 ∈ Field )
19 fldidom ⊢ ( 𝑌 ∈ Field → 𝑌 ∈ IDomn )
20 18 19 syl ⊢ ( 𝜑 → 𝑌 ∈ IDomn )
21 isidom ⊢ ( 𝑌 ∈ IDomn ↔ ( 𝑌 ∈ CRing ∧ 𝑌 ∈ Domn ) )
22 21 simplbi ⊢ ( 𝑌 ∈ IDomn → 𝑌 ∈ CRing )
23 20 22 syl ⊢ ( 𝜑 → 𝑌 ∈ CRing )
24 crngring ⊢ ( 𝑌 ∈ CRing → 𝑌 ∈ Ring )
25 23 24 syl ⊢ ( 𝜑 → 𝑌 ∈ Ring )
26 11 zrhrhm ⊢ ( 𝑌 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑌 ) )
27 25 26 syl ⊢ ( 𝜑 → 𝐿 ∈ ( ℤring RingHom 𝑌 ) )
28 zringbas ⊢ ℤ = ( Base ‘ ℤring )
29 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
30 28 29 rhmf ⊢ ( 𝐿 ∈ ( ℤring RingHom 𝑌 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) )
31 27 30 syl ⊢ ( 𝜑 → 𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) )
32 31 14 ffvelrnd ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐴 ) ∈ ( Base ‘ 𝑌 ) )
33 lgsvalmod ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 /L 𝑃 ) mod 𝑃 ) = ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) )
34 14 12 33 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 /L 𝑃 ) mod 𝑃 ) = ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) )
35 15 oveq1d ⊢ ( 𝜑 → ( ( 𝐴 /L 𝑃 ) mod 𝑃 ) = ( 1 mod 𝑃 ) )
36 34 35 eqtr3d ⊢ ( 𝜑 → ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( 1 mod 𝑃 ) )
37 1 2 3 4 5 6 7 8 9 10 11 12 14 36 lgsqrlem1 ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑇 ) ‘ ( 𝐿 ‘ 𝐴 ) ) = ( 0g ‘ 𝑌 ) )
38 eqid ⊢ ( 𝑌 ↑s ( Base ‘ 𝑌 ) ) = ( 𝑌 ↑s ( Base ‘ 𝑌 ) )
39 eqid ⊢ ( Base ‘ ( 𝑌 ↑s ( Base ‘ 𝑌 ) ) ) = ( Base ‘ ( 𝑌 ↑s ( Base ‘ 𝑌 ) ) )
40 fvexd ⊢ ( 𝜑 → ( Base ‘ 𝑌 ) ∈ V )
41 5 2 38 29 evl1rhm ⊢ ( 𝑌 ∈ CRing → 𝑂 ∈ ( 𝑆 RingHom ( 𝑌 ↑s ( Base ‘ 𝑌 ) ) ) )
42 23 41 syl ⊢ ( 𝜑 → 𝑂 ∈ ( 𝑆 RingHom ( 𝑌 ↑s ( Base ‘ 𝑌 ) ) ) )
43 3 39 rhmf ⊢ ( 𝑂 ∈ ( 𝑆 RingHom ( 𝑌 ↑s ( Base ‘ 𝑌 ) ) ) → 𝑂 : 𝐵 ⟶ ( Base ‘ ( 𝑌 ↑s ( Base ‘ 𝑌 ) ) ) )
44 42 43 syl ⊢ ( 𝜑 → 𝑂 : 𝐵 ⟶ ( Base ‘ ( 𝑌 ↑s ( Base ‘ 𝑌 ) ) ) )
45 2 ply1ring ⊢ ( 𝑌 ∈ Ring → 𝑆 ∈ Ring )
46 25 45 syl ⊢ ( 𝜑 → 𝑆 ∈ Ring )
47 ringgrp ⊢ ( 𝑆 ∈ Ring → 𝑆 ∈ Grp )
48 46 47 syl ⊢ ( 𝜑 → 𝑆 ∈ Grp )
49 eqid ⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
50 49 ringmgp ⊢ ( 𝑆 ∈ Ring → ( mulGrp ‘ 𝑆 ) ∈ Mnd )
51 46 50 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑆 ) ∈ Mnd )
52 oddprm ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
53 12 52 syl ⊢ ( 𝜑 → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
54 53 nnnn0d ⊢ ( 𝜑 → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 )
55 7 2 3 vr1cl ⊢ ( 𝑌 ∈ Ring → 𝑋 ∈ 𝐵 )
56 25 55 syl ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
57 49 3 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑆 ) )
58 57 6 mulgnn0cl ⊢ ( ( ( mulGrp ‘ 𝑆 ) ∈ Mnd ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( ( ( 𝑃 − 1 ) / 2 ) ↑ 𝑋 ) ∈ 𝐵 )
59 51 54 56 58 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑃 − 1 ) / 2 ) ↑ 𝑋 ) ∈ 𝐵 )
60 3 9 ringidcl ⊢ ( 𝑆 ∈ Ring → 1 ∈ 𝐵 )
61 46 60 syl ⊢ ( 𝜑 → 1 ∈ 𝐵 )
62 3 8 grpsubcl ⊢ ( ( 𝑆 ∈ Grp ∧ ( ( ( 𝑃 − 1 ) / 2 ) ↑ 𝑋 ) ∈ 𝐵 ∧ 1 ∈ 𝐵 ) → ( ( ( ( 𝑃 − 1 ) / 2 ) ↑ 𝑋 ) − 1 ) ∈ 𝐵 )
63 48 59 61 62 syl3anc ⊢ ( 𝜑 → ( ( ( ( 𝑃 − 1 ) / 2 ) ↑ 𝑋 ) − 1 ) ∈ 𝐵 )
64 10 63 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ 𝐵 )
65 44 64 ffvelrnd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑇 ) ∈ ( Base ‘ ( 𝑌 ↑s ( Base ‘ 𝑌 ) ) ) )
66 38 29 39 18 40 65 pwselbas ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑇 ) : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑌 ) )
67 66 ffnd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑇 ) Fn ( Base ‘ 𝑌 ) )
68 fniniseg ⊢ ( ( 𝑂 ‘ 𝑇 ) Fn ( Base ‘ 𝑌 ) → ( ( 𝐿 ‘ 𝐴 ) ∈ ( ◡ ( 𝑂 ‘ 𝑇 ) “ { ( 0g ‘ 𝑌 ) } ) ↔ ( ( 𝐿 ‘ 𝐴 ) ∈ ( Base ‘ 𝑌 ) ∧ ( ( 𝑂 ‘ 𝑇 ) ‘ ( 𝐿 ‘ 𝐴 ) ) = ( 0g ‘ 𝑌 ) ) ) )
69 67 68 syl ⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐴 ) ∈ ( ◡ ( 𝑂 ‘ 𝑇 ) “ { ( 0g ‘ 𝑌 ) } ) ↔ ( ( 𝐿 ‘ 𝐴 ) ∈ ( Base ‘ 𝑌 ) ∧ ( ( 𝑂 ‘ 𝑇 ) ‘ ( 𝐿 ‘ 𝐴 ) ) = ( 0g ‘ 𝑌 ) ) ) )
70 32 37 69 mpbir2and ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐴 ) ∈ ( ◡ ( 𝑂 ‘ 𝑇 ) “ { ( 0g ‘ 𝑌 ) } ) )