Metamath Proof Explorer


Theorem elringlsmd

Description: Membership in a product of two subsets of a ring, one direction. (Contributed by Thierry Arnoux, 13-Apr-2024)

Ref Expression
Hypotheses elringlsm.1 B = Base R
elringlsm.2 · ˙ = R
elringlsm.3 G = mulGrp R
elringlsm.4 × ˙ = LSSum G
elringlsm.6 φ E B
elringlsm.7 φ F B
elringlsmd.1 φ X E
elringlsmd.2 φ Y F
Assertion elringlsmd φ X · ˙ Y E × ˙ F

Proof

Step Hyp Ref Expression
1 elringlsm.1 B = Base R
2 elringlsm.2 · ˙ = R
3 elringlsm.3 G = mulGrp R
4 elringlsm.4 × ˙ = LSSum G
5 elringlsm.6 φ E B
6 elringlsm.7 φ F B
7 elringlsmd.1 φ X E
8 elringlsmd.2 φ Y F
9 eqidd φ X · ˙ Y = X · ˙ Y
10 rspceov X E Y F X · ˙ Y = X · ˙ Y x E y F X · ˙ Y = x · ˙ y
11 7 8 9 10 syl3anc φ x E y F X · ˙ Y = x · ˙ y
12 1 2 3 4 5 6 elringlsm φ X · ˙ Y E × ˙ F x E y F X · ˙ Y = x · ˙ y
13 11 12 mpbird φ X · ˙ Y E × ˙ F