Metamath Proof Explorer

Theorem r1peuqusdeg1

Description: Uniqueness of polynomial remainder in terms of a quotient structure in the sense of the right hand side of r1pid2 . (Contributed by SN, 21-Jun-2025)

Ref Expression
Hypotheses r1peuqus.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
r1peuqus.i ⊢ 𝐼 = ( ( RSpan ‘ 𝑃 ) ‘ { 𝐹 } )
r1peuqus.t ⊢ 𝑇 = ( 𝑃 /s ( 𝑃 ~QG 𝐼 ) )
r1peuqus.q ⊢ 𝑄 = ( Base ‘ 𝑇 )
r1peuqus.n ⊢ 𝑁 = ( Unic1p ‘ 𝑅 )
r1peuqus.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
r1peuqus.r ⊢ ( 𝜑 → 𝑅 ∈ Domn )
r1peuqus.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑁 )
r1peuqus.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑄 )
Assertion r1peuqusdeg1 ( 𝜑 → ∃! 𝑞 ∈ 𝑍 ( 𝐷 ‘ 𝑞 ) < ( 𝐷 ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 r1peuqus.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 r1peuqus.i ⊢ 𝐼 = ( ( RSpan ‘ 𝑃 ) ‘ { 𝐹 } )
3 r1peuqus.t ⊢ 𝑇 = ( 𝑃 /s ( 𝑃 ~QG 𝐼 ) )
4 r1peuqus.q ⊢ 𝑄 = ( Base ‘ 𝑇 )
5 r1peuqus.n ⊢ 𝑁 = ( Unic1p ‘ 𝑅 )
6 r1peuqus.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
7 r1peuqus.r ⊢ ( 𝜑 → 𝑅 ∈ Domn )
8 r1peuqus.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑁 )
9 r1peuqus.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑄 )
10 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
11 eqid ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
12 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
13 eqid ⊢ ( 𝑃 ~QG 𝐼 ) = ( 𝑃 ~QG 𝐼 )
14 1 ply1domn ⊢ ( 𝑅 ∈ Domn → 𝑃 ∈ Domn )
15 7 14 syl ⊢ ( 𝜑 → 𝑃 ∈ Domn )
16 domnring ⊢ ( 𝑃 ∈ Domn → 𝑃 ∈ Ring )
17 15 16 syl ⊢ ( 𝜑 → 𝑃 ∈ Ring )
18 1 10 5 uc1pcl ⊢ ( 𝐹 ∈ 𝑁 → 𝐹 ∈ ( Base ‘ 𝑃 ) )
19 8 18 syl ⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ 𝑃 ) )
20 9 4 eleqtrdi ⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝑇 ) )
21 10 11 12 13 3 2 17 19 20 ellcsrspsn ⊢ ( 𝜑 → ∃ 𝑝 ∈ ( Base ‘ 𝑃 ) ( 𝑍 = [ 𝑝 ] ( 𝑃 ~QG 𝐼 ) ∧ 𝑍 = { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } ) )
22 domnring ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )
23 7 22 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) → 𝑅 ∈ Ring )
25 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) → 𝑝 ∈ ( Base ‘ 𝑃 ) )
26 8 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) → 𝐹 ∈ 𝑁 )
27 1 6 10 11 12 5 24 25 26 ply1divalg3 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) → ∃! 𝑠 ∈ ( Base ‘ 𝑃 ) ( 𝐷 ‘ ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) ) < ( 𝐷 ‘ 𝐹 ) )
28 27 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) ∧ ( 𝑍 = [ 𝑝 ] ( 𝑃 ~QG 𝐼 ) ∧ 𝑍 = { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } ) ) → ∃! 𝑠 ∈ ( Base ‘ 𝑃 ) ( 𝐷 ‘ ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) ) < ( 𝐷 ‘ 𝐹 ) )
29 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) ∧ ( 𝑍 = [ 𝑝 ] ( 𝑃 ~QG 𝐼 ) ∧ 𝑍 = { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) ∈ V )
30 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) ∧ ( 𝑍 = [ 𝑝 ] ( 𝑃 ~QG 𝐼 ) ∧ 𝑍 = { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑃 ) ) → 𝑠 ∈ ( Base ‘ 𝑃 ) )
31 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) ∧ ( 𝑍 = [ 𝑝 ] ( 𝑃 ~QG 𝐼 ) ∧ 𝑍 = { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) )
32 oveq1 ⊢ ( 𝑦 = 𝑠 → ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) = ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) )
33 32 oveq2d ⊢ ( 𝑦 = 𝑠 → ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) )
34 33 eqeq2d ⊢ ( 𝑦 = 𝑠 → ( ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) ↔ ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) ) )
35 34 rspcev ⊢ ( ( 𝑠 ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) ) → ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) )
36 30 31 35 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) ∧ ( 𝑍 = [ 𝑝 ] ( 𝑃 ~QG 𝐼 ) ∧ 𝑍 = { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑃 ) ) → ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) )
37 eqeq1 ⊢ ( 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) → ( 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) ↔ ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) ) )
38 37 rexbidv ⊢ ( 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) → ( ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) ↔ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) ) )
39 29 36 38 elabd ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) ∧ ( 𝑍 = [ 𝑝 ] ( 𝑃 ~QG 𝐼 ) ∧ 𝑍 = { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) ∈ { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } )
40 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) ∧ ( 𝑍 = [ 𝑝 ] ( 𝑃 ~QG 𝐼 ) ∧ 𝑍 = { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑃 ) ) → 𝑍 = { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } )
41 39 40 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) ∧ ( 𝑍 = [ 𝑝 ] ( 𝑃 ~QG 𝐼 ) ∧ 𝑍 = { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) ∈ 𝑍 )
42 simprr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) ∧ ( 𝑍 = [ 𝑝 ] ( 𝑃 ~QG 𝐼 ) ∧ 𝑍 = { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } ) ) → 𝑍 = { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } )
43 42 eqimssd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) ∧ ( 𝑍 = [ 𝑝 ] ( 𝑃 ~QG 𝐼 ) ∧ 𝑍 = { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } ) ) → 𝑍 ⊆ { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } )
44 43 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) ∧ ( 𝑍 = [ 𝑝 ] ( 𝑃 ~QG 𝐼 ) ∧ 𝑍 = { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } ) ) ∧ 𝑞 ∈ 𝑍 ) → 𝑞 ∈ { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } )
45 eqeq1 ⊢ ( 𝑧 = 𝑞 → ( 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) ↔ 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) ) )
46 45 rexbidv ⊢ ( 𝑧 = 𝑞 → ( ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) ↔ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) ) )
47 33 eqeq2d ⊢ ( 𝑦 = 𝑠 → ( 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) ↔ 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) ) )
48 47 cbvrexvw ⊢ ( ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) ↔ ∃ 𝑠 ∈ ( Base ‘ 𝑃 ) 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) )
49 46 48 bitrdi ⊢ ( 𝑧 = 𝑞 → ( ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) ↔ ∃ 𝑠 ∈ ( Base ‘ 𝑃 ) 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) ) )
50 49 elabg ⊢ ( 𝑞 ∈ { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } → ( 𝑞 ∈ { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } ↔ ∃ 𝑠 ∈ ( Base ‘ 𝑃 ) 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) ) )
51 50 ibi ⊢ ( 𝑞 ∈ { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } → ∃ 𝑠 ∈ ( Base ‘ 𝑃 ) 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) )
52 44 51 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) ∧ ( 𝑍 = [ 𝑝 ] ( 𝑃 ~QG 𝐼 ) ∧ 𝑍 = { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } ) ) ∧ 𝑞 ∈ 𝑍 ) → ∃ 𝑠 ∈ ( Base ‘ 𝑃 ) 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) )
53 eqtr2 ⊢ ( ( 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) ∧ 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) ) ) → ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) ) )
54 17 ringgrpd ⊢ ( 𝜑 → 𝑃 ∈ Grp )
55 54 adantr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ∧ 𝑠 ∈ ( Base ‘ 𝑃 ) ∧ 𝑡 ∈ ( Base ‘ 𝑃 ) ) ) → 𝑃 ∈ Grp )
56 17 adantr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ∧ 𝑠 ∈ ( Base ‘ 𝑃 ) ∧ 𝑡 ∈ ( Base ‘ 𝑃 ) ) ) → 𝑃 ∈ Ring )
57 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ∧ 𝑠 ∈ ( Base ‘ 𝑃 ) ∧ 𝑡 ∈ ( Base ‘ 𝑃 ) ) ) → 𝑠 ∈ ( Base ‘ 𝑃 ) )
58 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ∧ 𝑠 ∈ ( Base ‘ 𝑃 ) ∧ 𝑡 ∈ ( Base ‘ 𝑃 ) ) ) → 𝐹 ∈ ( Base ‘ 𝑃 ) )
59 10 12 56 57 58 ringcld ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ∧ 𝑠 ∈ ( Base ‘ 𝑃 ) ∧ 𝑡 ∈ ( Base ‘ 𝑃 ) ) ) → ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ∈ ( Base ‘ 𝑃 ) )
60 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ∧ 𝑠 ∈ ( Base ‘ 𝑃 ) ∧ 𝑡 ∈ ( Base ‘ 𝑃 ) ) ) → 𝑡 ∈ ( Base ‘ 𝑃 ) )
61 10 12 56 60 58 ringcld ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ∧ 𝑠 ∈ ( Base ‘ 𝑃 ) ∧ 𝑡 ∈ ( Base ‘ 𝑃 ) ) ) → ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) ∈ ( Base ‘ 𝑃 ) )
62 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ∧ 𝑠 ∈ ( Base ‘ 𝑃 ) ∧ 𝑡 ∈ ( Base ‘ 𝑃 ) ) ) → 𝑝 ∈ ( Base ‘ 𝑃 ) )
63 10 11 grplcan ⊢ ( ( 𝑃 ∈ Grp ∧ ( ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) ∈ ( Base ‘ 𝑃 ) ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) ) → ( ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) ) ↔ ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) = ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) ) )
64 55 59 61 62 63 syl13anc ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ∧ 𝑠 ∈ ( Base ‘ 𝑃 ) ∧ 𝑡 ∈ ( Base ‘ 𝑃 ) ) ) → ( ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) ) ↔ ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) = ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) ) )
65 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
66 simplr2 ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ∧ 𝑠 ∈ ( Base ‘ 𝑃 ) ∧ 𝑡 ∈ ( Base ‘ 𝑃 ) ) ) ∧ ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) = ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) ) → 𝑠 ∈ ( Base ‘ 𝑃 ) )
67 simplr3 ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ∧ 𝑠 ∈ ( Base ‘ 𝑃 ) ∧ 𝑡 ∈ ( Base ‘ 𝑃 ) ) ) ∧ ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) = ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) ) → 𝑡 ∈ ( Base ‘ 𝑃 ) )
68 1 65 5 uc1pn0 ⊢ ( 𝐹 ∈ 𝑁 → 𝐹 ≠ ( 0g ‘ 𝑃 ) )
69 8 68 syl ⊢ ( 𝜑 → 𝐹 ≠ ( 0g ‘ 𝑃 ) )
70 19 69 eldifsnd ⊢ ( 𝜑 → 𝐹 ∈ ( ( Base ‘ 𝑃 ) ∖ { ( 0g ‘ 𝑃 ) } ) )
71 70 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ∧ 𝑠 ∈ ( Base ‘ 𝑃 ) ∧ 𝑡 ∈ ( Base ‘ 𝑃 ) ) ) ∧ ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) = ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) ) → 𝐹 ∈ ( ( Base ‘ 𝑃 ) ∖ { ( 0g ‘ 𝑃 ) } ) )
72 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ∧ 𝑠 ∈ ( Base ‘ 𝑃 ) ∧ 𝑡 ∈ ( Base ‘ 𝑃 ) ) ) ∧ ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) = ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) ) → 𝑃 ∈ Domn )
73 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ∧ 𝑠 ∈ ( Base ‘ 𝑃 ) ∧ 𝑡 ∈ ( Base ‘ 𝑃 ) ) ) ∧ ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) = ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) ) → ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) = ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) )
74 10 65 12 66 67 71 72 73 domnrcan ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ∧ 𝑠 ∈ ( Base ‘ 𝑃 ) ∧ 𝑡 ∈ ( Base ‘ 𝑃 ) ) ) ∧ ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) = ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) ) → 𝑠 = 𝑡 )
75 74 ex ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ∧ 𝑠 ∈ ( Base ‘ 𝑃 ) ∧ 𝑡 ∈ ( Base ‘ 𝑃 ) ) ) → ( ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) = ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) → 𝑠 = 𝑡 ) )
76 64 75 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ∧ 𝑠 ∈ ( Base ‘ 𝑃 ) ∧ 𝑡 ∈ ( Base ‘ 𝑃 ) ) ) → ( ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) ) → 𝑠 = 𝑡 ) )
77 76 3exp2 ⊢ ( 𝜑 → ( 𝑝 ∈ ( Base ‘ 𝑃 ) → ( 𝑠 ∈ ( Base ‘ 𝑃 ) → ( 𝑡 ∈ ( Base ‘ 𝑃 ) → ( ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) ) → 𝑠 = 𝑡 ) ) ) ) )
78 77 imp43 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) ∧ ( 𝑠 ∈ ( Base ‘ 𝑃 ) ∧ 𝑡 ∈ ( Base ‘ 𝑃 ) ) ) → ( ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) ) → 𝑠 = 𝑡 ) )
79 53 78 syl5 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) ∧ ( 𝑠 ∈ ( Base ‘ 𝑃 ) ∧ 𝑡 ∈ ( Base ‘ 𝑃 ) ) ) → ( ( 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) ∧ 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) ) ) → 𝑠 = 𝑡 ) )
80 79 ralrimivva ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) → ∀ 𝑠 ∈ ( Base ‘ 𝑃 ) ∀ 𝑡 ∈ ( Base ‘ 𝑃 ) ( ( 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) ∧ 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) ) ) → 𝑠 = 𝑡 ) )
81 oveq1 ⊢ ( 𝑠 = 𝑡 → ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) = ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) )
82 81 oveq2d ⊢ ( 𝑠 = 𝑡 → ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) ) )
83 82 eqeq2d ⊢ ( 𝑠 = 𝑡 → ( 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) ↔ 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) ) ) )
84 83 rmo4 ⊢ ( ∃* 𝑠 ∈ ( Base ‘ 𝑃 ) 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) ↔ ∀ 𝑠 ∈ ( Base ‘ 𝑃 ) ∀ 𝑡 ∈ ( Base ‘ 𝑃 ) ( ( 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) ∧ 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑡 ( .r ‘ 𝑃 ) 𝐹 ) ) ) → 𝑠 = 𝑡 ) )
85 80 84 sylibr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) → ∃* 𝑠 ∈ ( Base ‘ 𝑃 ) 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) )
86 85 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) ∧ ( 𝑍 = [ 𝑝 ] ( 𝑃 ~QG 𝐼 ) ∧ 𝑍 = { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } ) ) ∧ 𝑞 ∈ 𝑍 ) → ∃* 𝑠 ∈ ( Base ‘ 𝑃 ) 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) )
87 reu5 ⊢ ( ∃! 𝑠 ∈ ( Base ‘ 𝑃 ) 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) ↔ ( ∃ 𝑠 ∈ ( Base ‘ 𝑃 ) 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) ∧ ∃* 𝑠 ∈ ( Base ‘ 𝑃 ) 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) ) )
88 52 86 87 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) ∧ ( 𝑍 = [ 𝑝 ] ( 𝑃 ~QG 𝐼 ) ∧ 𝑍 = { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } ) ) ∧ 𝑞 ∈ 𝑍 ) → ∃! 𝑠 ∈ ( Base ‘ 𝑃 ) 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) )
89 fveq2 ⊢ ( 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) → ( 𝐷 ‘ 𝑞 ) = ( 𝐷 ‘ ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) ) )
90 89 breq1d ⊢ ( 𝑞 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) → ( ( 𝐷 ‘ 𝑞 ) < ( 𝐷 ‘ 𝐹 ) ↔ ( 𝐷 ‘ ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) ) < ( 𝐷 ‘ 𝐹 ) ) )
91 41 88 90 reuxfr1ds ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) ∧ ( 𝑍 = [ 𝑝 ] ( 𝑃 ~QG 𝐼 ) ∧ 𝑍 = { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } ) ) → ( ∃! 𝑞 ∈ 𝑍 ( 𝐷 ‘ 𝑞 ) < ( 𝐷 ‘ 𝐹 ) ↔ ∃! 𝑠 ∈ ( Base ‘ 𝑃 ) ( 𝐷 ‘ ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑠 ( .r ‘ 𝑃 ) 𝐹 ) ) ) < ( 𝐷 ‘ 𝐹 ) ) )
92 28 91 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) ∧ ( 𝑍 = [ 𝑝 ] ( 𝑃 ~QG 𝐼 ) ∧ 𝑍 = { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } ) ) → ∃! 𝑞 ∈ 𝑍 ( 𝐷 ‘ 𝑞 ) < ( 𝐷 ‘ 𝐹 ) )
93 92 ex ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝑍 = [ 𝑝 ] ( 𝑃 ~QG 𝐼 ) ∧ 𝑍 = { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } ) → ∃! 𝑞 ∈ 𝑍 ( 𝐷 ‘ 𝑞 ) < ( 𝐷 ‘ 𝐹 ) ) )
94 93 reximdva ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ( Base ‘ 𝑃 ) ( 𝑍 = [ 𝑝 ] ( 𝑃 ~QG 𝐼 ) ∧ 𝑍 = { 𝑧 ∣ ∃ 𝑦 ∈ ( Base ‘ 𝑃 ) 𝑧 = ( 𝑝 ( +g ‘ 𝑃 ) ( 𝑦 ( .r ‘ 𝑃 ) 𝐹 ) ) } ) → ∃ 𝑝 ∈ ( Base ‘ 𝑃 ) ∃! 𝑞 ∈ 𝑍 ( 𝐷 ‘ 𝑞 ) < ( 𝐷 ‘ 𝐹 ) ) )
95 21 94 mpd ⊢ ( 𝜑 → ∃ 𝑝 ∈ ( Base ‘ 𝑃 ) ∃! 𝑞 ∈ 𝑍 ( 𝐷 ‘ 𝑞 ) < ( 𝐷 ‘ 𝐹 ) )
96 id ⊢ ( ∃! 𝑞 ∈ 𝑍 ( 𝐷 ‘ 𝑞 ) < ( 𝐷 ‘ 𝐹 ) → ∃! 𝑞 ∈ 𝑍 ( 𝐷 ‘ 𝑞 ) < ( 𝐷 ‘ 𝐹 ) )
97 96 rexlimivw ⊢ ( ∃ 𝑝 ∈ ( Base ‘ 𝑃 ) ∃! 𝑞 ∈ 𝑍 ( 𝐷 ‘ 𝑞 ) < ( 𝐷 ‘ 𝐹 ) → ∃! 𝑞 ∈ 𝑍 ( 𝐷 ‘ 𝑞 ) < ( 𝐷 ‘ 𝐹 ) )
98 95 97 syl ⊢ ( 𝜑 → ∃! 𝑞 ∈ 𝑍 ( 𝐷 ‘ 𝑞 ) < ( 𝐷 ‘ 𝐹 ) )