Metamath Proof Explorer


Theorem irredmul

Description: If product of two elements is irreducible, then one of the elements must be a unit. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses irredn0.i I=IrredR
irredmul.b B=BaseR
irredmul.u U=UnitR
irredmul.t ·˙=R
Assertion irredmul XBYBX·˙YIXUYU

Proof

Step Hyp Ref Expression
1 irredn0.i I=IrredR
2 irredmul.b B=BaseR
3 irredmul.u U=UnitR
4 irredmul.t ·˙=R
5 2 3 1 4 isirred2 X·˙YIX·˙YB¬X·˙YUxByBx·˙y=X·˙YxUyU
6 5 simp3bi X·˙YIxByBx·˙y=X·˙YxUyU
7 eqid X·˙Y=X·˙Y
8 oveq1 x=Xx·˙y=X·˙y
9 8 eqeq1d x=Xx·˙y=X·˙YX·˙y=X·˙Y
10 eleq1 x=XxUXU
11 10 orbi1d x=XxUyUXUyU
12 9 11 imbi12d x=Xx·˙y=X·˙YxUyUX·˙y=X·˙YXUyU
13 oveq2 y=YX·˙y=X·˙Y
14 13 eqeq1d y=YX·˙y=X·˙YX·˙Y=X·˙Y
15 eleq1 y=YyUYU
16 15 orbi2d y=YXUyUXUYU
17 14 16 imbi12d y=YX·˙y=X·˙YXUyUX·˙Y=X·˙YXUYU
18 12 17 rspc2v XBYBxByBx·˙y=X·˙YxUyUX·˙Y=X·˙YXUYU
19 7 18 mpii XBYBxByBx·˙y=X·˙YxUyUXUYU
20 6 19 syl5 XBYBX·˙YIXUYU
21 20 3impia XBYBX·˙YIXUYU