Metamath Proof Explorer


Theorem lsmsnidl

Description: The product of the ring with a single element is a principal ideal. (Contributed by Thierry Arnoux, 21-Jan-2024)

Ref Expression
Hypotheses lsmsnpridl.1 B = Base R
lsmsnpridl.2 G = mulGrp R
lsmsnpridl.3 × ˙ = LSSum G
lsmsnpridl.4 K = RSpan R
lsmsnpridl.5 φ R Ring
lsmsnpridl.6 φ X B
Assertion lsmsnidl φ B × ˙ X LPIdeal R

Proof

Step Hyp Ref Expression
1 lsmsnpridl.1 B = Base R
2 lsmsnpridl.2 G = mulGrp R
3 lsmsnpridl.3 × ˙ = LSSum G
4 lsmsnpridl.4 K = RSpan R
5 lsmsnpridl.5 φ R Ring
6 lsmsnpridl.6 φ X B
7 sneq y = X y = X
8 7 fveq2d y = X K y = K X
9 8 eqeq2d y = X B × ˙ X = K y B × ˙ X = K X
10 9 adantl φ y = X B × ˙ X = K y B × ˙ X = K X
11 1 2 3 4 5 6 lsmsnpridl φ B × ˙ X = K X
12 6 10 11 rspcedvd φ y B B × ˙ X = K y
13 eqid LPIdeal R = LPIdeal R
14 13 4 1 islpidl R Ring B × ˙ X LPIdeal R y B B × ˙ X = K y
15 5 14 syl φ B × ˙ X LPIdeal R y B B × ˙ X = K y
16 12 15 mpbird φ B × ˙ X LPIdeal R