Metamath Proof Explorer

Theorem rngunsnply1chr2

Description: When adjoining an element X with characteristic polynomial of degree 2 to a subring S , the elements Y of the generated subring can be written as a linear form. (Contributed by Thierry Arnoux, 8-Nov-2026)

Ref Expression
Hypotheses rngunsnply1chr2.v 
|- V = ( Base ` R )
rngunsnply1chr2.p 
|- P = ( Poly1 ` ( R |`s S ) )
rngunsnply1chr2.u 
|- U = ( Base ` P )
rngunsnply1chr2.q 
|- Q = ( R evalSub1 S )
rngunsnply1chr2.r 
|- ( ph -> R e. CRing )
rngunsnply1chr2.1 
|- ( ph -> R e. NzRing )
rngunsnply1chr2.s 
|- ( ph -> S e. ( SubRing ` R ) )
rngunsnply1chr2.x 
|- ( ph -> X e. V )
rngunsnply1chr2.y 
|- ( ph -> Y e. ( N ` ( S u. { X } ) ) )
rngunsnply1chr2.n 
|- N = ( RingSpan ` R )
rngunsnply1chr2.2 
|- .+ = ( +g ` R )
rngunsnply1chr2.3 
|- .x. = ( .r ` R )
rngunsnply1chr2.4 
|- .^ = ( .g ` ( mulGrp ` R ) )
rngunsnply1chr2.a 
|- ( ph -> A e. S )
rngunsnply1chr2.b 
|- ( ph -> B e. S )
rngunsnply1chr2.5 
|- ( ph -> ( 2 .^ X ) = ( ( A .x. X ) .+ B ) )
Assertion rngunsnply1chr2 
|- ( ph -> E. a e. S E. b e. S Y = ( ( a .x. X ) .+ b ) )

Proof

Step Hyp Ref Expression
1 rngunsnply1chr2.v 
 |-  V = ( Base ` R )
2 rngunsnply1chr2.p 
 |-  P = ( Poly1 ` ( R |`s S ) )
3 rngunsnply1chr2.u 
 |-  U = ( Base ` P )
4 rngunsnply1chr2.q 
 |-  Q = ( R evalSub1 S )
5 rngunsnply1chr2.r 
 |-  ( ph -> R e. CRing )
6 rngunsnply1chr2.1 
 |-  ( ph -> R e. NzRing )
7 rngunsnply1chr2.s 
 |-  ( ph -> S e. ( SubRing ` R ) )
8 rngunsnply1chr2.x 
 |-  ( ph -> X e. V )
9 rngunsnply1chr2.y 
 |-  ( ph -> Y e. ( N ` ( S u. { X } ) ) )
10 rngunsnply1chr2.n 
 |-  N = ( RingSpan ` R )
11 rngunsnply1chr2.2 
 |-  .+ = ( +g ` R )
12 rngunsnply1chr2.3 
 |-  .x. = ( .r ` R )
13 rngunsnply1chr2.4 
 |-  .^ = ( .g ` ( mulGrp ` R ) )
14 rngunsnply1chr2.a 
 |-  ( ph -> A e. S )
15 rngunsnply1chr2.b 
 |-  ( ph -> B e. S )
16 rngunsnply1chr2.5 
 |-  ( ph -> ( 2 .^ X ) = ( ( A .x. X ) .+ B ) )
17 oveq1 
 |-  ( a = ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 1 ) -> ( a .x. X ) = ( ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 1 ) .x. X ) )
18 17 oveq1d 
 |-  ( a = ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 1 ) -> ( ( a .x. X ) .+ b ) = ( ( ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 1 ) .x. X ) .+ b ) )
19 18 eqeq2d 
 |-  ( a = ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 1 ) -> ( Y = ( ( a .x. X ) .+ b ) <-> Y = ( ( ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 1 ) .x. X ) .+ b ) ) )
20 oveq2 
 |-  ( b = ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 0 ) -> ( ( ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 1 ) .x. X ) .+ b ) = ( ( ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 1 ) .x. X ) .+ ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 0 ) ) )
21 20 eqeq2d 
 |-  ( b = ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 0 ) -> ( Y = ( ( ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 1 ) .x. X ) .+ b ) <-> Y = ( ( ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 1 ) .x. X ) .+ ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 0 ) ) ) )
22 eqid 
 |-  ( R |`s S ) = ( R |`s S )
23 22 subrgring 
 |-  ( S e. ( SubRing ` R ) -> ( R |`s S ) e. Ring )
24 7 23 syl 
 |-  ( ph -> ( R |`s S ) e. Ring )
25 24 adantr 
 |-  ( ( ph /\ p e. U ) -> ( R |`s S ) e. Ring )
26 simpr 
 |-  ( ( ph /\ p e. U ) -> p e. U )
27 5 adantr 
 |-  ( ( ph /\ p e. U ) -> R e. CRing )
28 6 adantr 
 |-  ( ( ph /\ p e. U ) -> R e. NzRing )
29 7 adantr 
 |-  ( ( ph /\ p e. U ) -> S e. ( SubRing ` R ) )
30 8 adantr 
 |-  ( ( ph /\ p e. U ) -> X e. V )
31 9 adantr 
 |-  ( ( ph /\ p e. U ) -> Y e. ( N ` ( S u. { X } ) ) )
32 14 adantr 
 |-  ( ( ph /\ p e. U ) -> A e. S )
33 15 adantr 
 |-  ( ( ph /\ p e. U ) -> B e. S )
34 16 adantr 
 |-  ( ( ph /\ p e. U ) -> ( 2 .^ X ) = ( ( A .x. X ) .+ B ) )
35 eqid 
 |-  ( deg1 ` R ) = ( deg1 ` R )
36 eqid 
 |-  ( rem1p ` ( R |`s S ) ) = ( rem1p ` ( R |`s S ) )
37 eqid 
 |-  ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) = ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) )
38 eqid 
 |-  ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) = ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) )
39 1 2 3 4 27 28 29 30 31 10 11 12 13 32 33 34 35 36 37 38 26 rngunsnply1chr2lem2 
 |-  ( ( ph /\ p e. U ) -> ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) e. ( Unic1p ` ( R |`s S ) ) )
40 eqid 
 |-  ( Unic1p ` ( R |`s S ) ) = ( Unic1p ` ( R |`s S ) )
41 36 2 3 40 r1pcl 
 |-  ( ( ( R |`s S ) e. Ring /\ p e. U /\ ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) e. ( Unic1p ` ( R |`s S ) ) ) -> ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) e. U )
42 25 26 39 41 syl3anc 
 |-  ( ( ph /\ p e. U ) -> ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) e. U )
43 1nn0 
 |-  1 e. NN0
44 eqid 
 |-  ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) = ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) )
45 eqid 
 |-  ( Base ` ( R |`s S ) ) = ( Base ` ( R |`s S ) )
46 44 3 2 45 coe1fvalcl 
 |-  ( ( ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) e. U /\ 1 e. NN0 ) -> ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 1 ) e. ( Base ` ( R |`s S ) ) )
47 42 43 46 sylancl 
 |-  ( ( ph /\ p e. U ) -> ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 1 ) e. ( Base ` ( R |`s S ) ) )
48 22 subrgbas 
 |-  ( S e. ( SubRing ` R ) -> S = ( Base ` ( R |`s S ) ) )
49 29 48 syl 
 |-  ( ( ph /\ p e. U ) -> S = ( Base ` ( R |`s S ) ) )
50 47 49 eleqtrrd 
 |-  ( ( ph /\ p e. U ) -> ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 1 ) e. S )
51 50 adantr 
 |-  ( ( ( ph /\ p e. U ) /\ Y = ( ( Q ` p ) ` X ) ) -> ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 1 ) e. S )
52 0nn0 
 |-  0 e. NN0
53 44 3 2 45 coe1fvalcl 
 |-  ( ( ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) e. U /\ 0 e. NN0 ) -> ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 0 ) e. ( Base ` ( R |`s S ) ) )
54 42 52 53 sylancl 
 |-  ( ( ph /\ p e. U ) -> ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 0 ) e. ( Base ` ( R |`s S ) ) )
55 54 49 eleqtrrd 
 |-  ( ( ph /\ p e. U ) -> ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 0 ) e. S )
56 55 adantr 
 |-  ( ( ( ph /\ p e. U ) /\ Y = ( ( Q ` p ) ` X ) ) -> ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 0 ) e. S )
57 simpr 
 |-  ( ( ( ph /\ p e. U ) /\ Y = ( ( Q ` p ) ` X ) ) -> Y = ( ( Q ` p ) ` X ) )
58 1 2 3 4 27 28 29 30 31 10 11 12 13 32 33 34 35 36 37 38 26 rngunsnply1chr2lem3 
 |-  ( ( ph /\ p e. U ) -> ( ( ( deg1 ` R ) ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) <_ 1 /\ ( ( Q ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` X ) = ( ( Q ` p ) ` X ) ) )
59 58 simprd 
 |-  ( ( ph /\ p e. U ) -> ( ( Q ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` X ) = ( ( Q ` p ) ` X ) )
60 59 adantr 
 |-  ( ( ( ph /\ p e. U ) /\ Y = ( ( Q ` p ) ` X ) ) -> ( ( Q ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` X ) = ( ( Q ` p ) ` X ) )
61 eqid 
 |-  ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 1 ) = ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 1 )
62 eqid 
 |-  ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 0 ) = ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 0 )
63 58 simpld 
 |-  ( ( ph /\ p e. U ) -> ( ( deg1 ` R ) ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) <_ 1 )
64 2 4 1 3 12 11 44 35 61 62 27 29 42 63 30 evls1degle1 
 |-  ( ( ph /\ p e. U ) -> ( ( Q ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` X ) = ( ( ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 1 ) .x. X ) .+ ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 0 ) ) )
65 64 adantr 
 |-  ( ( ( ph /\ p e. U ) /\ Y = ( ( Q ` p ) ` X ) ) -> ( ( Q ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` X ) = ( ( ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 1 ) .x. X ) .+ ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 0 ) ) )
66 57 60 65 3eqtr2d 
 |-  ( ( ( ph /\ p e. U ) /\ Y = ( ( Q ` p ) ` X ) ) -> Y = ( ( ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 1 ) .x. X ) .+ ( ( coe1 ` ( p ( rem1p ` ( R |`s S ) ) ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ) ` 0 ) ) )
67 19 21 51 56 66 2rspcedvdw 
 |-  ( ( ( ph /\ p e. U ) /\ Y = ( ( Q ` p ) ` X ) ) -> E. a e. S E. b e. S Y = ( ( a .x. X ) .+ b ) )
68 1 2 3 4 5 7 8 10 rngunsnply1 
 |-  ( ph -> ( Y e. ( N ` ( S u. { X } ) ) <-> E. p e. U Y = ( ( Q ` p ) ` X ) ) )
69 9 68 mpbid 
 |-  ( ph -> E. p e. U Y = ( ( Q ` p ) ` X ) )
70 67 69 r19.29a 
 |-  ( ph -> E. a e. S E. b e. S Y = ( ( a .x. X ) .+ b ) )