Metamath Proof Explorer


Theorem bj-isclm

Description: The predicate "is a subcomplex module". (Contributed by BJ, 6-Jan-2024)

Ref Expression
Hypotheses bj-isclm.scal φ F = Scalar W
bj-isclm.base φ K = Base F
Assertion bj-isclm φ W CMod W LMod F = fld 𝑠 K K SubRing fld

Proof

Step Hyp Ref Expression
1 bj-isclm.scal φ F = Scalar W
2 bj-isclm.base φ K = Base F
3 eqid Scalar W = Scalar W
4 eqid Base Scalar W = Base Scalar W
5 3 4 isclm W CMod W LMod Scalar W = fld 𝑠 Base Scalar W Base Scalar W SubRing fld
6 1 eqcomd φ Scalar W = F
7 fveq2 F = Scalar W Base F = Base Scalar W
8 eqtr K = Base F Base F = Base Scalar W K = Base Scalar W
9 8 eqcomd K = Base F Base F = Base Scalar W Base Scalar W = K
10 9 ex K = Base F Base F = Base Scalar W Base Scalar W = K
11 2 7 10 syl2im φ F = Scalar W Base Scalar W = K
12 1 11 mpd φ Base Scalar W = K
13 12 oveq2d φ fld 𝑠 Base Scalar W = fld 𝑠 K
14 6 13 eqeq12d φ Scalar W = fld 𝑠 Base Scalar W F = fld 𝑠 K
15 12 eleq1d φ Base Scalar W SubRing fld K SubRing fld
16 14 15 3anbi23d φ W LMod Scalar W = fld 𝑠 Base Scalar W Base Scalar W SubRing fld W LMod F = fld 𝑠 K K SubRing fld
17 5 16 syl5bb φ W CMod W LMod F = fld 𝑠 K K SubRing fld