Metamath Proof Explorer

Theorem irredrmul

Description: The product of an irreducible element and a unit is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses irredn0.i โŠข ๐ผ = ( Irred โ€˜ ๐‘… )
irredrmul.u โŠข ๐‘ˆ = ( Unit โ€˜ ๐‘… )
irredrmul.t โŠข ยท = ( .r โ€˜ ๐‘… )
Assertion irredrmul ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐ผ )

Proof

Step Hyp Ref Expression
1 irredn0.i โŠข ๐ผ = ( Irred โ€˜ ๐‘… )
2 irredrmul.u โŠข ๐‘ˆ = ( Unit โ€˜ ๐‘… )
3 irredrmul.t โŠข ยท = ( .r โ€˜ ๐‘… )
4 simp2 โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ๐‘‹ โˆˆ ๐ผ )
5 simp1 โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ๐‘… โˆˆ Ring )
6 simp3 โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ๐‘Œ โˆˆ ๐‘ˆ )
7 eqid โŠข ( /r โ€˜ ๐‘… ) = ( /r โ€˜ ๐‘… )
8 2 7 unitdvcl โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐‘ˆ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) ( /r โ€˜ ๐‘… ) ๐‘Œ ) โˆˆ ๐‘ˆ )
9 8 3com23 โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘Œ โˆˆ ๐‘ˆ โˆง ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐‘ˆ ) โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) ( /r โ€˜ ๐‘… ) ๐‘Œ ) โˆˆ ๐‘ˆ )
10 9 3expia โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐‘ˆ โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) ( /r โ€˜ ๐‘… ) ๐‘Œ ) โˆˆ ๐‘ˆ ) )
11 5 6 10 syl2anc โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐‘ˆ โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) ( /r โ€˜ ๐‘… ) ๐‘Œ ) โˆˆ ๐‘ˆ ) )
12 eqid โŠข ( Base โ€˜ ๐‘… ) = ( Base โ€˜ ๐‘… )
13 1 12 irredcl โŠข ( ๐‘‹ โˆˆ ๐ผ โ†’ ๐‘‹ โˆˆ ( Base โ€˜ ๐‘… ) )
14 13 3ad2ant2 โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ๐‘‹ โˆˆ ( Base โ€˜ ๐‘… ) )
15 12 2 7 3 dvrcan3 โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ( Base โ€˜ ๐‘… ) โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) ( /r โ€˜ ๐‘… ) ๐‘Œ ) = ๐‘‹ )
16 5 14 6 15 syl3anc โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) ( /r โ€˜ ๐‘… ) ๐‘Œ ) = ๐‘‹ )
17 16 eleq1d โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ( ( ( ๐‘‹ ยท ๐‘Œ ) ( /r โ€˜ ๐‘… ) ๐‘Œ ) โˆˆ ๐‘ˆ โ†” ๐‘‹ โˆˆ ๐‘ˆ ) )
18 11 17 sylibd โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐‘ˆ โ†’ ๐‘‹ โˆˆ ๐‘ˆ ) )
19 5 ad2antrr โŠข ( ( ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โˆง ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ) โˆง ( ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) = ( ๐‘‹ ยท ๐‘Œ ) ) ) โ†’ ๐‘… โˆˆ Ring )
20 eldifi โŠข ( ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โ†’ ๐‘ฆ โˆˆ ( Base โ€˜ ๐‘… ) )
21 20 ad2antrl โŠข ( ( ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โˆง ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ) โˆง ( ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) = ( ๐‘‹ ยท ๐‘Œ ) ) ) โ†’ ๐‘ฆ โˆˆ ( Base โ€˜ ๐‘… ) )
22 6 ad2antrr โŠข ( ( ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โˆง ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ) โˆง ( ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) = ( ๐‘‹ ยท ๐‘Œ ) ) ) โ†’ ๐‘Œ โˆˆ ๐‘ˆ )
23 12 2 7 dvrcl โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘ฆ โˆˆ ( Base โ€˜ ๐‘… ) โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) โˆˆ ( Base โ€˜ ๐‘… ) )
24 19 21 22 23 syl3anc โŠข ( ( ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โˆง ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ) โˆง ( ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) = ( ๐‘‹ ยท ๐‘Œ ) ) ) โ†’ ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) โˆˆ ( Base โ€˜ ๐‘… ) )
25 eldifn โŠข ( ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โ†’ ยฌ ๐‘ฆ โˆˆ ๐‘ˆ )
26 25 ad2antrl โŠข ( ( ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โˆง ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ) โˆง ( ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) = ( ๐‘‹ ยท ๐‘Œ ) ) ) โ†’ ยฌ ๐‘ฆ โˆˆ ๐‘ˆ )
27 2 3 unitmulcl โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) โˆˆ ๐‘ˆ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ( ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) ยท ๐‘Œ ) โˆˆ ๐‘ˆ )
28 27 3com23 โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘Œ โˆˆ ๐‘ˆ โˆง ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) โˆˆ ๐‘ˆ ) โ†’ ( ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) ยท ๐‘Œ ) โˆˆ ๐‘ˆ )
29 28 3expia โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ( ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) โˆˆ ๐‘ˆ โ†’ ( ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) ยท ๐‘Œ ) โˆˆ ๐‘ˆ ) )
30 19 22 29 syl2anc โŠข ( ( ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โˆง ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ) โˆง ( ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) = ( ๐‘‹ ยท ๐‘Œ ) ) ) โ†’ ( ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) โˆˆ ๐‘ˆ โ†’ ( ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) ยท ๐‘Œ ) โˆˆ ๐‘ˆ ) )
31 12 2 7 3 dvrcan1 โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘ฆ โˆˆ ( Base โ€˜ ๐‘… ) โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ( ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) ยท ๐‘Œ ) = ๐‘ฆ )
32 19 21 22 31 syl3anc โŠข ( ( ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โˆง ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ) โˆง ( ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) = ( ๐‘‹ ยท ๐‘Œ ) ) ) โ†’ ( ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) ยท ๐‘Œ ) = ๐‘ฆ )
33 32 eleq1d โŠข ( ( ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โˆง ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ) โˆง ( ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) = ( ๐‘‹ ยท ๐‘Œ ) ) ) โ†’ ( ( ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) ยท ๐‘Œ ) โˆˆ ๐‘ˆ โ†” ๐‘ฆ โˆˆ ๐‘ˆ ) )
34 30 33 sylibd โŠข ( ( ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โˆง ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ) โˆง ( ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) = ( ๐‘‹ ยท ๐‘Œ ) ) ) โ†’ ( ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) โˆˆ ๐‘ˆ โ†’ ๐‘ฆ โˆˆ ๐‘ˆ ) )
35 26 34 mtod โŠข ( ( ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โˆง ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ) โˆง ( ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) = ( ๐‘‹ ยท ๐‘Œ ) ) ) โ†’ ยฌ ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) โˆˆ ๐‘ˆ )
36 24 35 eldifd โŠข ( ( ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โˆง ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ) โˆง ( ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) = ( ๐‘‹ ยท ๐‘Œ ) ) ) โ†’ ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) )
37 simprr โŠข ( ( ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โˆง ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ) โˆง ( ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) = ( ๐‘‹ ยท ๐‘Œ ) ) ) โ†’ ( ๐‘ฅ ยท ๐‘ฆ ) = ( ๐‘‹ ยท ๐‘Œ ) )
38 37 oveq1d โŠข ( ( ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โˆง ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ) โˆง ( ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) = ( ๐‘‹ ยท ๐‘Œ ) ) ) โ†’ ( ( ๐‘ฅ ยท ๐‘ฆ ) ( /r โ€˜ ๐‘… ) ๐‘Œ ) = ( ( ๐‘‹ ยท ๐‘Œ ) ( /r โ€˜ ๐‘… ) ๐‘Œ ) )
39 eldifi โŠข ( ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โ†’ ๐‘ฅ โˆˆ ( Base โ€˜ ๐‘… ) )
40 39 ad2antlr โŠข ( ( ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โˆง ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ) โˆง ( ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) = ( ๐‘‹ ยท ๐‘Œ ) ) ) โ†’ ๐‘ฅ โˆˆ ( Base โ€˜ ๐‘… ) )
41 12 2 7 3 dvrass โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ๐‘… ) โˆง ๐‘ฆ โˆˆ ( Base โ€˜ ๐‘… ) โˆง ๐‘Œ โˆˆ ๐‘ˆ ) ) โ†’ ( ( ๐‘ฅ ยท ๐‘ฆ ) ( /r โ€˜ ๐‘… ) ๐‘Œ ) = ( ๐‘ฅ ยท ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) ) )
42 19 40 21 22 41 syl13anc โŠข ( ( ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โˆง ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ) โˆง ( ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) = ( ๐‘‹ ยท ๐‘Œ ) ) ) โ†’ ( ( ๐‘ฅ ยท ๐‘ฆ ) ( /r โ€˜ ๐‘… ) ๐‘Œ ) = ( ๐‘ฅ ยท ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) ) )
43 16 ad2antrr โŠข ( ( ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โˆง ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ) โˆง ( ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) = ( ๐‘‹ ยท ๐‘Œ ) ) ) โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) ( /r โ€˜ ๐‘… ) ๐‘Œ ) = ๐‘‹ )
44 38 42 43 3eqtr3d โŠข ( ( ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โˆง ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ) โˆง ( ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) = ( ๐‘‹ ยท ๐‘Œ ) ) ) โ†’ ( ๐‘ฅ ยท ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) ) = ๐‘‹ )
45 oveq2 โŠข ( ๐‘ง = ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) โ†’ ( ๐‘ฅ ยท ๐‘ง ) = ( ๐‘ฅ ยท ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) ) )
46 45 eqeq1d โŠข ( ๐‘ง = ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) โ†’ ( ( ๐‘ฅ ยท ๐‘ง ) = ๐‘‹ โ†” ( ๐‘ฅ ยท ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) ) = ๐‘‹ ) )
47 46 rspcev โŠข ( ( ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆง ( ๐‘ฅ ยท ( ๐‘ฆ ( /r โ€˜ ๐‘… ) ๐‘Œ ) ) = ๐‘‹ ) โ†’ โˆƒ ๐‘ง โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ( ๐‘ฅ ยท ๐‘ง ) = ๐‘‹ )
48 36 44 47 syl2anc โŠข ( ( ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โˆง ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ) โˆง ( ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) = ( ๐‘‹ ยท ๐‘Œ ) ) ) โ†’ โˆƒ ๐‘ง โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ( ๐‘ฅ ยท ๐‘ง ) = ๐‘‹ )
49 48 rexlimdvaa โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โˆง ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ) โ†’ ( โˆƒ ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ( ๐‘ฅ ยท ๐‘ฆ ) = ( ๐‘‹ ยท ๐‘Œ ) โ†’ โˆƒ ๐‘ง โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ( ๐‘ฅ ยท ๐‘ง ) = ๐‘‹ ) )
50 49 reximdva โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ( โˆƒ ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆƒ ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ( ๐‘ฅ ยท ๐‘ฆ ) = ( ๐‘‹ ยท ๐‘Œ ) โ†’ โˆƒ ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆƒ ๐‘ง โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ( ๐‘ฅ ยท ๐‘ง ) = ๐‘‹ ) )
51 18 50 orim12d โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ( ( ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐‘ˆ โˆจ โˆƒ ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆƒ ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ( ๐‘ฅ ยท ๐‘ฆ ) = ( ๐‘‹ ยท ๐‘Œ ) ) โ†’ ( ๐‘‹ โˆˆ ๐‘ˆ โˆจ โˆƒ ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆƒ ๐‘ง โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ( ๐‘ฅ ยท ๐‘ง ) = ๐‘‹ ) ) )
52 12 2 unitcl โŠข ( ๐‘Œ โˆˆ ๐‘ˆ โ†’ ๐‘Œ โˆˆ ( Base โ€˜ ๐‘… ) )
53 52 3ad2ant3 โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ๐‘Œ โˆˆ ( Base โ€˜ ๐‘… ) )
54 12 3 ringcl โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ( Base โ€˜ ๐‘… ) โˆง ๐‘Œ โˆˆ ( Base โ€˜ ๐‘… ) ) โ†’ ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ( Base โ€˜ ๐‘… ) )
55 5 14 53 54 syl3anc โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ( Base โ€˜ ๐‘… ) )
56 eqid โŠข ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) = ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ )
57 12 2 1 56 3 isnirred โŠข ( ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ( Base โ€˜ ๐‘… ) โ†’ ( ยฌ ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐ผ โ†” ( ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐‘ˆ โˆจ โˆƒ ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆƒ ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ( ๐‘ฅ ยท ๐‘ฆ ) = ( ๐‘‹ ยท ๐‘Œ ) ) ) )
58 55 57 syl โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ( ยฌ ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐ผ โ†” ( ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐‘ˆ โˆจ โˆƒ ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆƒ ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ( ๐‘ฅ ยท ๐‘ฆ ) = ( ๐‘‹ ยท ๐‘Œ ) ) ) )
59 12 2 1 56 3 isnirred โŠข ( ๐‘‹ โˆˆ ( Base โ€˜ ๐‘… ) โ†’ ( ยฌ ๐‘‹ โˆˆ ๐ผ โ†” ( ๐‘‹ โˆˆ ๐‘ˆ โˆจ โˆƒ ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆƒ ๐‘ง โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ( ๐‘ฅ ยท ๐‘ง ) = ๐‘‹ ) ) )
60 14 59 syl โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ( ยฌ ๐‘‹ โˆˆ ๐ผ โ†” ( ๐‘‹ โˆˆ ๐‘ˆ โˆจ โˆƒ ๐‘ฅ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) โˆƒ ๐‘ง โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– ๐‘ˆ ) ( ๐‘ฅ ยท ๐‘ง ) = ๐‘‹ ) ) )
61 51 58 60 3imtr4d โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ( ยฌ ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐ผ โ†’ ยฌ ๐‘‹ โˆˆ ๐ผ ) )
62 4 61 mt4d โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ผ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐ผ )