Metamath Proof Explorer


Theorem lidlrsppropd

Description: The left ideals and ring span of a ring depend only on the ring components. Here W is expected to be either B (when closure is available) or _V (when strong equality is available). (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Hypotheses lidlpropd.1 φ B = Base K
lidlpropd.2 φ B = Base L
lidlpropd.3 φ B W
lidlpropd.4 φ x W y W x + K y = x + L y
lidlpropd.5 φ x B y B x K y W
lidlpropd.6 φ x B y B x K y = x L y
Assertion lidlrsppropd φ LIdeal K = LIdeal L RSpan K = RSpan L

Proof

Step Hyp Ref Expression
1 lidlpropd.1 φ B = Base K
2 lidlpropd.2 φ B = Base L
3 lidlpropd.3 φ B W
4 lidlpropd.4 φ x W y W x + K y = x + L y
5 lidlpropd.5 φ x B y B x K y W
6 lidlpropd.6 φ x B y B x K y = x L y
7 rlmbas Base K = Base ringLMod K
8 1 7 eqtrdi φ B = Base ringLMod K
9 rlmbas Base L = Base ringLMod L
10 2 9 eqtrdi φ B = Base ringLMod L
11 rlmplusg + K = + ringLMod K
12 11 oveqi x + K y = x + ringLMod K y
13 rlmplusg + L = + ringLMod L
14 13 oveqi x + L y = x + ringLMod L y
15 4 12 14 3eqtr3g φ x W y W x + ringLMod K y = x + ringLMod L y
16 rlmvsca K = ringLMod K
17 16 oveqi x K y = x ringLMod K y
18 17 5 eqeltrrid φ x B y B x ringLMod K y W
19 rlmvsca L = ringLMod L
20 19 oveqi x L y = x ringLMod L y
21 6 17 20 3eqtr3g φ x B y B x ringLMod K y = x ringLMod L y
22 baseid Base = Slot Base ndx
23 eqid Base K = Base K
24 22 23 strfvi Base K = Base I K
25 rlmsca2 I K = Scalar ringLMod K
26 25 fveq2i Base I K = Base Scalar ringLMod K
27 24 26 eqtri Base K = Base Scalar ringLMod K
28 1 27 eqtrdi φ B = Base Scalar ringLMod K
29 eqid Base L = Base L
30 22 29 strfvi Base L = Base I L
31 rlmsca2 I L = Scalar ringLMod L
32 31 fveq2i Base I L = Base Scalar ringLMod L
33 30 32 eqtri Base L = Base Scalar ringLMod L
34 2 33 eqtrdi φ B = Base Scalar ringLMod L
35 8 10 3 15 18 21 28 34 lsspropd φ LSubSp ringLMod K = LSubSp ringLMod L
36 lidlval LIdeal K = LSubSp ringLMod K
37 lidlval LIdeal L = LSubSp ringLMod L
38 35 36 37 3eqtr4g φ LIdeal K = LIdeal L
39 fvexd φ ringLMod K V
40 fvexd φ ringLMod L V
41 8 10 3 15 18 21 28 34 39 40 lsppropd φ LSpan ringLMod K = LSpan ringLMod L
42 rspval RSpan K = LSpan ringLMod K
43 rspval RSpan L = LSpan ringLMod L
44 41 42 43 3eqtr4g φ RSpan K = RSpan L
45 38 44 jca φ LIdeal K = LIdeal L RSpan K = RSpan L