Metamath Proof Explorer

Theorem rngqiprnglin

Description: F is linear with respect to the multiplication. (Contributed by AV, 28-Feb-2025)

Ref Expression
Hypotheses rng2idlring.r 
|- ( ph -> R e. Rng )
rng2idlring.i 
|- ( ph -> I e. ( 2Ideal ` R ) )
rng2idlring.j 
|- J = ( R |`s I )
rng2idlring.u 
|- ( ph -> J e. Ring )
rng2idlring.b 
|- B = ( Base ` R )
rng2idlring.t 
|- .x. = ( .r ` R )
rng2idlring.1 
|- .1. = ( 1r ` J )
rngqiprngim.g 
|- .~ = ( R ~QG I )
rngqiprngim.q 
|- Q = ( R /s .~ )
rngqiprngim.c 
|- C = ( Base ` Q )
rngqiprngim.p 
|- P = ( Q Xs. J )
rngqiprngim.f 
|- F = ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. )
Assertion rngqiprnglin 
|- ( ph -> A. a e. B A. b e. B ( F ` ( a .x. b ) ) = ( ( F ` a ) ( .r ` P ) ( F ` b ) ) )

Proof

Step Hyp Ref Expression
1 rng2idlring.r 
 |-  ( ph -> R e. Rng )
2 rng2idlring.i 
 |-  ( ph -> I e. ( 2Ideal ` R ) )
3 rng2idlring.j 
 |-  J = ( R |`s I )
4 rng2idlring.u 
 |-  ( ph -> J e. Ring )
5 rng2idlring.b 
 |-  B = ( Base ` R )
6 rng2idlring.t 
 |-  .x. = ( .r ` R )
7 rng2idlring.1 
 |-  .1. = ( 1r ` J )
8 rngqiprngim.g 
 |-  .~ = ( R ~QG I )
9 rngqiprngim.q 
 |-  Q = ( R /s .~ )
10 rngqiprngim.c 
 |-  C = ( Base ` Q )
11 rngqiprngim.p 
 |-  P = ( Q Xs. J )
12 rngqiprngim.f 
 |-  F = ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. )
13 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
14 eqid 
 |-  ( Base ` J ) = ( Base ` J )
15 9 ovexi 
 |-  Q e. _V
16 15 a1i 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> Q e. _V )
17 4 adantr 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> J e. Ring )
18 simpl 
 |-  ( ( a e. B /\ b e. B ) -> a e. B )
19 8 9 5 13 quseccl0 
 |-  ( ( R e. Rng /\ a e. B ) -> [ a ] .~ e. ( Base ` Q ) )
20 1 18 19 syl2an 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> [ a ] .~ e. ( Base ` Q ) )
21 1 2 3 4 5 6 7 rngqiprngghmlem1 
 |-  ( ( ph /\ a e. B ) -> ( .1. .x. a ) e. ( Base ` J ) )
22 18 21 sylan2 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( .1. .x. a ) e. ( Base ` J ) )
23 simpr 
 |-  ( ( a e. B /\ b e. B ) -> b e. B )
24 8 9 5 13 quseccl0 
 |-  ( ( R e. Rng /\ b e. B ) -> [ b ] .~ e. ( Base ` Q ) )
25 1 23 24 syl2an 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> [ b ] .~ e. ( Base ` Q ) )
26 1 2 3 4 5 6 7 rngqiprngghmlem1 
 |-  ( ( ph /\ b e. B ) -> ( .1. .x. b ) e. ( Base ` J ) )
27 23 26 sylan2 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( .1. .x. b ) e. ( Base ` J ) )
28 1 2 3 4 5 6 7 8 9 rngqiprnglinlem3 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( [ a ] .~ ( .r ` Q ) [ b ] .~ ) e. ( Base ` Q ) )
29 eqid 
 |-  ( .r ` J ) = ( .r ` J )
30 14 29 17 22 27 ringcld 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( .1. .x. a ) ( .r ` J ) ( .1. .x. b ) ) e. ( Base ` J ) )
31 eqid 
 |-  ( .r ` Q ) = ( .r ` Q )
32 eqid 
 |-  ( .r ` P ) = ( .r ` P )
33 11 13 14 16 17 20 22 25 27 28 30 31 29 32 xpsmul 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( <. [ a ] .~ , ( .1. .x. a ) >. ( .r ` P ) <. [ b ] .~ , ( .1. .x. b ) >. ) = <. ( [ a ] .~ ( .r ` Q ) [ b ] .~ ) , ( ( .1. .x. a ) ( .r ` J ) ( .1. .x. b ) ) >. )
34 1 2 3 4 5 6 7 8 9 rngqiprnglinlem2 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> [ ( a .x. b ) ] .~ = ( [ a ] .~ ( .r ` Q ) [ b ] .~ ) )
35 34 eqcomd 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( [ a ] .~ ( .r ` Q ) [ b ] .~ ) = [ ( a .x. b ) ] .~ )
36 2 adantr 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> I e. ( 2Ideal ` R ) )
37 3 6 ressmulr 
 |-  ( I e. ( 2Ideal ` R ) -> .x. = ( .r ` J ) )
38 36 37 syl 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> .x. = ( .r ` J ) )
39 38 eqcomd 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( .r ` J ) = .x. )
40 39 oveqd 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( .1. .x. a ) ( .r ` J ) ( .1. .x. b ) ) = ( ( .1. .x. a ) .x. ( .1. .x. b ) ) )
41 1 2 3 4 5 6 7 rngqiprnglinlem1 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( .1. .x. a ) .x. ( .1. .x. b ) ) = ( .1. .x. ( a .x. b ) ) )
42 40 41 eqtrd 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( .1. .x. a ) ( .r ` J ) ( .1. .x. b ) ) = ( .1. .x. ( a .x. b ) ) )
43 35 42 opeq12d 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> <. ( [ a ] .~ ( .r ` Q ) [ b ] .~ ) , ( ( .1. .x. a ) ( .r ` J ) ( .1. .x. b ) ) >. = <. [ ( a .x. b ) ] .~ , ( .1. .x. ( a .x. b ) ) >. )
44 33 43 eqtr2d 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> <. [ ( a .x. b ) ] .~ , ( .1. .x. ( a .x. b ) ) >. = ( <. [ a ] .~ , ( .1. .x. a ) >. ( .r ` P ) <. [ b ] .~ , ( .1. .x. b ) >. ) )
45 1 anim1i 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( R e. Rng /\ ( a e. B /\ b e. B ) ) )
46 3anass 
 |-  ( ( R e. Rng /\ a e. B /\ b e. B ) <-> ( R e. Rng /\ ( a e. B /\ b e. B ) ) )
47 45 46 sylibr 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( R e. Rng /\ a e. B /\ b e. B ) )
48 5 6 rngcl 
 |-  ( ( R e. Rng /\ a e. B /\ b e. B ) -> ( a .x. b ) e. B )
49 47 48 syl 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( a .x. b ) e. B )
50 1 2 3 4 5 6 7 8 9 10 11 12 rngqiprngimfv 
 |-  ( ( ph /\ ( a .x. b ) e. B ) -> ( F ` ( a .x. b ) ) = <. [ ( a .x. b ) ] .~ , ( .1. .x. ( a .x. b ) ) >. )
51 49 50 syldan 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( F ` ( a .x. b ) ) = <. [ ( a .x. b ) ] .~ , ( .1. .x. ( a .x. b ) ) >. )
52 1 2 3 4 5 6 7 8 9 10 11 12 rngqiprngimfv 
 |-  ( ( ph /\ a e. B ) -> ( F ` a ) = <. [ a ] .~ , ( .1. .x. a ) >. )
53 18 52 sylan2 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( F ` a ) = <. [ a ] .~ , ( .1. .x. a ) >. )
54 1 2 3 4 5 6 7 8 9 10 11 12 rngqiprngimfv 
 |-  ( ( ph /\ b e. B ) -> ( F ` b ) = <. [ b ] .~ , ( .1. .x. b ) >. )
55 23 54 sylan2 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( F ` b ) = <. [ b ] .~ , ( .1. .x. b ) >. )
56 53 55 oveq12d 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( F ` a ) ( .r ` P ) ( F ` b ) ) = ( <. [ a ] .~ , ( .1. .x. a ) >. ( .r ` P ) <. [ b ] .~ , ( .1. .x. b ) >. ) )
57 44 51 56 3eqtr4d 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( F ` ( a .x. b ) ) = ( ( F ` a ) ( .r ` P ) ( F ` b ) ) )
58 57 ralrimivva 
 |-  ( ph -> A. a e. B A. b e. B ( F ` ( a .x. b ) ) = ( ( F ` a ) ( .r ` P ) ( F ` b ) ) )