Metamath Proof Explorer

Theorem q1pdir

Description: Distribution of univariate polynomial quotient over addition. (Contributed by Thierry Arnoux, 2-Apr-2025)

Ref Expression
Hypotheses r1padd1.p 
|- P = ( Poly1 ` R )
r1padd1.u 
|- U = ( Base ` P )
r1padd1.n 
|- N = ( Unic1p ` R )
q1pdir.d 
|- ./ = ( quot1p ` R )
q1pdir.r 
|- ( ph -> R e. Ring )
q1pdir.a 
|- ( ph -> A e. U )
q1pdir.c 
|- ( ph -> C e. N )
q1pdir.b 
|- ( ph -> B e. U )
q1pdir.1 
|- .+ = ( +g ` P )
Assertion q1pdir 
|- ( ph -> ( ( A .+ B ) ./ C ) = ( ( A ./ C ) .+ ( B ./ C ) ) )

Proof

Step Hyp Ref Expression
1 r1padd1.p 
 |-  P = ( Poly1 ` R )
2 r1padd1.u 
 |-  U = ( Base ` P )
3 r1padd1.n 
 |-  N = ( Unic1p ` R )
4 q1pdir.d 
 |-  ./ = ( quot1p ` R )
5 q1pdir.r 
 |-  ( ph -> R e. Ring )
6 q1pdir.a 
 |-  ( ph -> A e. U )
7 q1pdir.c 
 |-  ( ph -> C e. N )
8 q1pdir.b 
 |-  ( ph -> B e. U )
9 q1pdir.1 
 |-  .+ = ( +g ` P )
10 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
11 5 10 syl 
 |-  ( ph -> P e. Ring )
12 11 ringgrpd 
 |-  ( ph -> P e. Grp )
13 2 9 12 6 8 grpcld 
 |-  ( ph -> ( A .+ B ) e. U )
14 4 1 2 3 q1pcl 
 |-  ( ( R e. Ring /\ A e. U /\ C e. N ) -> ( A ./ C ) e. U )
15 5 6 7 14 syl3anc 
 |-  ( ph -> ( A ./ C ) e. U )
16 4 1 2 3 q1pcl 
 |-  ( ( R e. Ring /\ B e. U /\ C e. N ) -> ( B ./ C ) e. U )
17 5 8 7 16 syl3anc 
 |-  ( ph -> ( B ./ C ) e. U )
18 2 9 12 15 17 grpcld 
 |-  ( ph -> ( ( A ./ C ) .+ ( B ./ C ) ) e. U )
19 1 2 3 uc1pcl 
 |-  ( C e. N -> C e. U )
20 7 19 syl 
 |-  ( ph -> C e. U )
21 eqid 
 |-  ( .r ` P ) = ( .r ` P )
22 2 9 21 ringdir 
 |-  ( ( P e. Ring /\ ( ( A ./ C ) e. U /\ ( B ./ C ) e. U /\ C e. U ) ) -> ( ( ( A ./ C ) .+ ( B ./ C ) ) ( .r ` P ) C ) = ( ( ( A ./ C ) ( .r ` P ) C ) .+ ( ( B ./ C ) ( .r ` P ) C ) ) )
23 11 15 17 20 22 syl13anc 
 |-  ( ph -> ( ( ( A ./ C ) .+ ( B ./ C ) ) ( .r ` P ) C ) = ( ( ( A ./ C ) ( .r ` P ) C ) .+ ( ( B ./ C ) ( .r ` P ) C ) ) )
24 23 oveq2d 
 |-  ( ph -> ( ( A .+ B ) ( -g ` P ) ( ( ( A ./ C ) .+ ( B ./ C ) ) ( .r ` P ) C ) ) = ( ( A .+ B ) ( -g ` P ) ( ( ( A ./ C ) ( .r ` P ) C ) .+ ( ( B ./ C ) ( .r ` P ) C ) ) ) )
25 11 ringabld 
 |-  ( ph -> P e. Abel )
26 2 21 11 15 20 ringcld 
 |-  ( ph -> ( ( A ./ C ) ( .r ` P ) C ) e. U )
27 2 21 11 17 20 ringcld 
 |-  ( ph -> ( ( B ./ C ) ( .r ` P ) C ) e. U )
28 eqid 
 |-  ( -g ` P ) = ( -g ` P )
29 2 9 28 ablsub4 
 |-  ( ( P e. Abel /\ ( A e. U /\ B e. U ) /\ ( ( ( A ./ C ) ( .r ` P ) C ) e. U /\ ( ( B ./ C ) ( .r ` P ) C ) e. U ) ) -> ( ( A .+ B ) ( -g ` P ) ( ( ( A ./ C ) ( .r ` P ) C ) .+ ( ( B ./ C ) ( .r ` P ) C ) ) ) = ( ( A ( -g ` P ) ( ( A ./ C ) ( .r ` P ) C ) ) .+ ( B ( -g ` P ) ( ( B ./ C ) ( .r ` P ) C ) ) ) )
30 25 6 8 26 27 29 syl122anc 
 |-  ( ph -> ( ( A .+ B ) ( -g ` P ) ( ( ( A ./ C ) ( .r ` P ) C ) .+ ( ( B ./ C ) ( .r ` P ) C ) ) ) = ( ( A ( -g ` P ) ( ( A ./ C ) ( .r ` P ) C ) ) .+ ( B ( -g ` P ) ( ( B ./ C ) ( .r ` P ) C ) ) ) )
31 24 30 eqtrd 
 |-  ( ph -> ( ( A .+ B ) ( -g ` P ) ( ( ( A ./ C ) .+ ( B ./ C ) ) ( .r ` P ) C ) ) = ( ( A ( -g ` P ) ( ( A ./ C ) ( .r ` P ) C ) ) .+ ( B ( -g ` P ) ( ( B ./ C ) ( .r ` P ) C ) ) ) )
32 31 fveq2d 
 |-  ( ph -> ( ( deg1 ` R ) ` ( ( A .+ B ) ( -g ` P ) ( ( ( A ./ C ) .+ ( B ./ C ) ) ( .r ` P ) C ) ) ) = ( ( deg1 ` R ) ` ( ( A ( -g ` P ) ( ( A ./ C ) ( .r ` P ) C ) ) .+ ( B ( -g ` P ) ( ( B ./ C ) ( .r ` P ) C ) ) ) ) )
33 eqid 
 |-  ( deg1 ` R ) = ( deg1 ` R )
34 eqid 
 |-  ( rem1p ` R ) = ( rem1p ` R )
35 34 1 2 4 21 28 r1pval 
 |-  ( ( A e. U /\ C e. U ) -> ( A ( rem1p ` R ) C ) = ( A ( -g ` P ) ( ( A ./ C ) ( .r ` P ) C ) ) )
36 6 20 35 syl2anc 
 |-  ( ph -> ( A ( rem1p ` R ) C ) = ( A ( -g ` P ) ( ( A ./ C ) ( .r ` P ) C ) ) )
37 34 1 2 3 r1pcl 
 |-  ( ( R e. Ring /\ A e. U /\ C e. N ) -> ( A ( rem1p ` R ) C ) e. U )
38 5 6 7 37 syl3anc 
 |-  ( ph -> ( A ( rem1p ` R ) C ) e. U )
39 36 38 eqeltrrd 
 |-  ( ph -> ( A ( -g ` P ) ( ( A ./ C ) ( .r ` P ) C ) ) e. U )
40 34 1 2 4 21 28 r1pval 
 |-  ( ( B e. U /\ C e. U ) -> ( B ( rem1p ` R ) C ) = ( B ( -g ` P ) ( ( B ./ C ) ( .r ` P ) C ) ) )
41 8 20 40 syl2anc 
 |-  ( ph -> ( B ( rem1p ` R ) C ) = ( B ( -g ` P ) ( ( B ./ C ) ( .r ` P ) C ) ) )
42 34 1 2 3 r1pcl 
 |-  ( ( R e. Ring /\ B e. U /\ C e. N ) -> ( B ( rem1p ` R ) C ) e. U )
43 5 8 7 42 syl3anc 
 |-  ( ph -> ( B ( rem1p ` R ) C ) e. U )
44 41 43 eqeltrrd 
 |-  ( ph -> ( B ( -g ` P ) ( ( B ./ C ) ( .r ` P ) C ) ) e. U )
45 33 1 2 deg1xrcl 
 |-  ( C e. U -> ( ( deg1 ` R ) ` C ) e. RR* )
46 20 45 syl 
 |-  ( ph -> ( ( deg1 ` R ) ` C ) e. RR* )
47 36 fveq2d 
 |-  ( ph -> ( ( deg1 ` R ) ` ( A ( rem1p ` R ) C ) ) = ( ( deg1 ` R ) ` ( A ( -g ` P ) ( ( A ./ C ) ( .r ` P ) C ) ) ) )
48 34 1 2 3 33 r1pdeglt 
 |-  ( ( R e. Ring /\ A e. U /\ C e. N ) -> ( ( deg1 ` R ) ` ( A ( rem1p ` R ) C ) ) < ( ( deg1 ` R ) ` C ) )
49 5 6 7 48 syl3anc 
 |-  ( ph -> ( ( deg1 ` R ) ` ( A ( rem1p ` R ) C ) ) < ( ( deg1 ` R ) ` C ) )
50 47 49 eqbrtrrd 
 |-  ( ph -> ( ( deg1 ` R ) ` ( A ( -g ` P ) ( ( A ./ C ) ( .r ` P ) C ) ) ) < ( ( deg1 ` R ) ` C ) )
51 41 fveq2d 
 |-  ( ph -> ( ( deg1 ` R ) ` ( B ( rem1p ` R ) C ) ) = ( ( deg1 ` R ) ` ( B ( -g ` P ) ( ( B ./ C ) ( .r ` P ) C ) ) ) )
52 34 1 2 3 33 r1pdeglt 
 |-  ( ( R e. Ring /\ B e. U /\ C e. N ) -> ( ( deg1 ` R ) ` ( B ( rem1p ` R ) C ) ) < ( ( deg1 ` R ) ` C ) )
53 5 8 7 52 syl3anc 
 |-  ( ph -> ( ( deg1 ` R ) ` ( B ( rem1p ` R ) C ) ) < ( ( deg1 ` R ) ` C ) )
54 51 53 eqbrtrrd 
 |-  ( ph -> ( ( deg1 ` R ) ` ( B ( -g ` P ) ( ( B ./ C ) ( .r ` P ) C ) ) ) < ( ( deg1 ` R ) ` C ) )
55 1 33 5 2 9 39 44 46 50 54 deg1addlt 
 |-  ( ph -> ( ( deg1 ` R ) ` ( ( A ( -g ` P ) ( ( A ./ C ) ( .r ` P ) C ) ) .+ ( B ( -g ` P ) ( ( B ./ C ) ( .r ` P ) C ) ) ) ) < ( ( deg1 ` R ) ` C ) )
56 32 55 eqbrtrd 
 |-  ( ph -> ( ( deg1 ` R ) ` ( ( A .+ B ) ( -g ` P ) ( ( ( A ./ C ) .+ ( B ./ C ) ) ( .r ` P ) C ) ) ) < ( ( deg1 ` R ) ` C ) )
57 4 1 2 33 28 21 3 q1peqb 
 |-  ( ( R e. Ring /\ ( A .+ B ) e. U /\ C e. N ) -> ( ( ( ( A ./ C ) .+ ( B ./ C ) ) e. U /\ ( ( deg1 ` R ) ` ( ( A .+ B ) ( -g ` P ) ( ( ( A ./ C ) .+ ( B ./ C ) ) ( .r ` P ) C ) ) ) < ( ( deg1 ` R ) ` C ) ) <-> ( ( A .+ B ) ./ C ) = ( ( A ./ C ) .+ ( B ./ C ) ) ) )
58 57 biimpa 
 |-  ( ( ( R e. Ring /\ ( A .+ B ) e. U /\ C e. N ) /\ ( ( ( A ./ C ) .+ ( B ./ C ) ) e. U /\ ( ( deg1 ` R ) ` ( ( A .+ B ) ( -g ` P ) ( ( ( A ./ C ) .+ ( B ./ C ) ) ( .r ` P ) C ) ) ) < ( ( deg1 ` R ) ` C ) ) ) -> ( ( A .+ B ) ./ C ) = ( ( A ./ C ) .+ ( B ./ C ) ) )
59 5 13 7 18 56 58 syl32anc 
 |-  ( ph -> ( ( A .+ B ) ./ C ) = ( ( A ./ C ) .+ ( B ./ C ) ) )