Metamath Proof Explorer

Theorem prmidlval

Description: The class of prime ideals of a ring R . (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Thierry Arnoux, 12-Jan-2024)

Ref Expression
Hypotheses prmidlval.1 ⊢ B = Base R
prmidlval.2 ⊢ · ˙ = ⋅ R
Assertion prmidlval Could not format assertion : No typesetting found for |- ( R e. Ring -> ( PrmIdeal ` R ) = { i e. ( LIdeal ` R ) | ( i =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } ) with typecode |-

Proof

Step Hyp Ref Expression
1 prmidlval.1 ⊢ B = Base R
2 prmidlval.2 ⊢ · ˙ = ⋅ R
3 df-prmidl Could not format PrmIdeal = ( r e. Ring |-> { i e. ( LIdeal ` r ) | ( i =/= ( Base ` r ) /\ A. a e. ( LIdeal ` r ) A. b e. ( LIdeal ` r ) ( A. x e. a A. y e. b ( x ( .r ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } ) : No typesetting found for |- PrmIdeal = ( r e. Ring |-> { i e. ( LIdeal ` r ) | ( i =/= ( Base ` r ) /\ A. a e. ( LIdeal ` r ) A. b e. ( LIdeal ` r ) ( A. x e. a A. y e. b ( x ( .r ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } ) with typecode |-
4 fveq2 ⊢ r = R → LIdeal ⁡ r = LIdeal ⁡ R
5 fveq2 ⊢ r = R → Base r = Base R
6 5 1 eqtr4di ⊢ r = R → Base r = B
7 6 neeq2d ⊢ r = R → i ≠ Base r ↔ i ≠ B
8 fveq2 ⊢ r = R → ⋅ r = ⋅ R
9 8 2 eqtr4di ⊢ r = R → ⋅ r = · ˙
10 9 oveqd ⊢ r = R → x ⋅ r y = x · ˙ y
11 10 eleq1d ⊢ r = R → x ⋅ r y ∈ i ↔ x · ˙ y ∈ i
12 11 2ralbidv ⊢ r = R → ∀ x ∈ a ∀ y ∈ b x ⋅ r y ∈ i ↔ ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i
13 12 imbi1d ⊢ r = R → ∀ x ∈ a ∀ y ∈ b x ⋅ r y ∈ i → a ⊆ i ∨ b ⊆ i ↔ ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i → a ⊆ i ∨ b ⊆ i
14 4 13 raleqbidv ⊢ r = R → ∀ b ∈ LIdeal ⁡ r ∀ x ∈ a ∀ y ∈ b x ⋅ r y ∈ i → a ⊆ i ∨ b ⊆ i ↔ ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i → a ⊆ i ∨ b ⊆ i
15 4 14 raleqbidv ⊢ r = R → ∀ a ∈ LIdeal ⁡ r ∀ b ∈ LIdeal ⁡ r ∀ x ∈ a ∀ y ∈ b x ⋅ r y ∈ i → a ⊆ i ∨ b ⊆ i ↔ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i → a ⊆ i ∨ b ⊆ i
16 7 15 anbi12d ⊢ r = R → i ≠ Base r ∧ ∀ a ∈ LIdeal ⁡ r ∀ b ∈ LIdeal ⁡ r ∀ x ∈ a ∀ y ∈ b x ⋅ r y ∈ i → a ⊆ i ∨ b ⊆ i ↔ i ≠ B ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i → a ⊆ i ∨ b ⊆ i
17 4 16 rabeqbidv ⊢ r = R → i ∈ LIdeal ⁡ r | i ≠ Base r ∧ ∀ a ∈ LIdeal ⁡ r ∀ b ∈ LIdeal ⁡ r ∀ x ∈ a ∀ y ∈ b x ⋅ r y ∈ i → a ⊆ i ∨ b ⊆ i = i ∈ LIdeal ⁡ R | i ≠ B ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i → a ⊆ i ∨ b ⊆ i
18 id ⊢ R ∈ Ring → R ∈ Ring
19 eqid ⊢ i ∈ LIdeal ⁡ R | i ≠ B ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i → a ⊆ i ∨ b ⊆ i = i ∈ LIdeal ⁡ R | i ≠ B ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i → a ⊆ i ∨ b ⊆ i
20 fvexd ⊢ R ∈ Ring → LIdeal ⁡ R ∈ V
21 19 20 rabexd ⊢ R ∈ Ring → i ∈ LIdeal ⁡ R | i ≠ B ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i → a ⊆ i ∨ b ⊆ i ∈ V
22 3 17 18 21 fvmptd3 Could not format ( R e. Ring -> ( PrmIdeal ` R ) = { i e. ( LIdeal ` R ) | ( i =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } ) : No typesetting found for |- ( R e. Ring -> ( PrmIdeal ` R ) = { i e. ( LIdeal ` R ) | ( i =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } ) with typecode |-