This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( Irred ` R )
irredmul.b 
|- B = ( Base ` R )
irredmul.u 
|- U = ( Unit ` R )
irredmul.t 
|- .x. = ( .r ` R )
Assertion irredmul 
|- ( ( X e. B /\ Y e. B /\ ( X .x. Y ) e. I ) -> ( X e. U \/ Y e. U ) )

Proof

Step Hyp Ref Expression
1 irredn0.i 
 |-  I = ( Irred ` R )
2 irredmul.b 
 |-  B = ( Base ` R )
3 irredmul.u 
 |-  U = ( Unit ` R )
4 irredmul.t 
 |-  .x. = ( .r ` R )
5 2 3 1 4 isirred2 
 |-  ( ( X .x. Y ) e. I <-> ( ( X .x. Y ) e. B /\ -. ( X .x. Y ) e. U /\ A. x e. B A. y e. B ( ( x .x. y ) = ( X .x. Y ) -> ( x e. U \/ y e. U ) ) ) )
6 5 simp3bi 
 |-  ( ( X .x. Y ) e. I -> A. x e. B A. y e. B ( ( x .x. y ) = ( X .x. Y ) -> ( x e. U \/ y e. U ) ) )
7 eqid 
 |-  ( X .x. Y ) = ( X .x. Y )
8 oveq1 
 |-  ( x = X -> ( x .x. y ) = ( X .x. y ) )
9 8 eqeq1d 
 |-  ( x = X -> ( ( x .x. y ) = ( X .x. Y ) <-> ( X .x. y ) = ( X .x. Y ) ) )
10 eleq1 
 |-  ( x = X -> ( x e. U <-> X e. U ) )
11 10 orbi1d 
 |-  ( x = X -> ( ( x e. U \/ y e. U ) <-> ( X e. U \/ y e. U ) ) )
12 9 11 imbi12d 
 |-  ( x = X -> ( ( ( x .x. y ) = ( X .x. Y ) -> ( x e. U \/ y e. U ) ) <-> ( ( X .x. y ) = ( X .x. Y ) -> ( X e. U \/ y e. U ) ) ) )
13 oveq2 
 |-  ( y = Y -> ( X .x. y ) = ( X .x. Y ) )
14 13 eqeq1d 
 |-  ( y = Y -> ( ( X .x. y ) = ( X .x. Y ) <-> ( X .x. Y ) = ( X .x. Y ) ) )
15 eleq1 
 |-  ( y = Y -> ( y e. U <-> Y e. U ) )
16 15 orbi2d 
 |-  ( y = Y -> ( ( X e. U \/ y e. U ) <-> ( X e. U \/ Y e. U ) ) )
17 14 16 imbi12d 
 |-  ( y = Y -> ( ( ( X .x. y ) = ( X .x. Y ) -> ( X e. U \/ y e. U ) ) <-> ( ( X .x. Y ) = ( X .x. Y ) -> ( X e. U \/ Y e. U ) ) ) )
18 12 17 rspc2v 
 |-  ( ( X e. B /\ Y e. B ) -> ( A. x e. B A. y e. B ( ( x .x. y ) = ( X .x. Y ) -> ( x e. U \/ y e. U ) ) -> ( ( X .x. Y ) = ( X .x. Y ) -> ( X e. U \/ Y e. U ) ) ) )
19 7 18 mpii 
 |-  ( ( X e. B /\ Y e. B ) -> ( A. x e. B A. y e. B ( ( x .x. y ) = ( X .x. Y ) -> ( x e. U \/ y e. U ) ) -> ( X e. U \/ Y e. U ) ) )
20 6 19 syl5 
 |-  ( ( X e. B /\ Y e. B ) -> ( ( X .x. Y ) e. I -> ( X e. U \/ Y e. U ) ) )
21 20 3impia 
 |-  ( ( X e. B /\ Y e. B /\ ( X .x. Y ) e. I ) -> ( X e. U \/ Y e. U ) )