Metamath Proof Explorer


Theorem elrgspnlem3

Description: Lemma for elrgspn . (Contributed by Thierry Arnoux, 5-Oct-2025)

Ref Expression
Hypotheses elrgspn.b B = Base R
elrgspn.m M = mulGrp R
elrgspn.x · ˙ = R
elrgspn.n N = RingSpan R
elrgspn.f F = f Word A | finSupp 0 f
elrgspn.r φ R Ring
elrgspn.a φ A B
elrgspnlem1.1 S = ran g F R w Word A g w · ˙ M w
Assertion elrgspnlem3 φ A S

Proof

Step Hyp Ref Expression
1 elrgspn.b B = Base R
2 elrgspn.m M = mulGrp R
3 elrgspn.x · ˙ = R
4 elrgspn.n N = RingSpan R
5 elrgspn.f F = f Word A | finSupp 0 f
6 elrgspn.r φ R Ring
7 elrgspn.a φ A B
8 elrgspnlem1.1 S = ran g F R w Word A g w · ˙ M w
9 eqid g F R w Word A g w · ˙ M w = g F R w Word A g w · ˙ M w
10 fveq1 g = v Word A if v = ⟨“ x ”⟩ 1 0 g w = v Word A if v = ⟨“ x ”⟩ 1 0 w
11 10 oveq1d g = v Word A if v = ⟨“ x ”⟩ 1 0 g w · ˙ M w = v Word A if v = ⟨“ x ”⟩ 1 0 w · ˙ M w
12 11 mpteq2dv g = v Word A if v = ⟨“ x ”⟩ 1 0 w Word A g w · ˙ M w = w Word A v Word A if v = ⟨“ x ”⟩ 1 0 w · ˙ M w
13 12 oveq2d g = v Word A if v = ⟨“ x ”⟩ 1 0 R w Word A g w · ˙ M w = R w Word A v Word A if v = ⟨“ x ”⟩ 1 0 w · ˙ M w
14 13 eqeq2d g = v Word A if v = ⟨“ x ”⟩ 1 0 x = R w Word A g w · ˙ M w x = R w Word A v Word A if v = ⟨“ x ”⟩ 1 0 w · ˙ M w
15 breq1 f = v Word A if v = ⟨“ x ”⟩ 1 0 finSupp 0 f finSupp 0 v Word A if v = ⟨“ x ”⟩ 1 0
16 zex V
17 16 a1i φ x A V
18 1 fvexi B V
19 18 a1i φ B V
20 19 7 ssexd φ A V
21 wrdexg A V Word A V
22 20 21 syl φ Word A V
23 22 adantr φ x A Word A V
24 1zzd φ x A v Word A v = ⟨“ x ”⟩ 1
25 0zd φ x A v Word A ¬ v = ⟨“ x ”⟩ 0
26 24 25 ifclda φ x A v Word A if v = ⟨“ x ”⟩ 1 0
27 26 fmpttd φ x A v Word A if v = ⟨“ x ”⟩ 1 0 : Word A
28 17 23 27 elmapdd φ x A v Word A if v = ⟨“ x ”⟩ 1 0 Word A
29 28 elexd φ x A v Word A if v = ⟨“ x ”⟩ 1 0 V
30 27 ffund φ x A Fun v Word A if v = ⟨“ x ”⟩ 1 0
31 0zd φ x A 0
32 snfi ⟨“ x ”⟩ Fin
33 32 a1i φ x A ⟨“ x ”⟩ Fin
34 eldifsni v Word A ⟨“ x ”⟩ v ⟨“ x ”⟩
35 34 adantl φ x A v Word A ⟨“ x ”⟩ v ⟨“ x ”⟩
36 35 neneqd φ x A v Word A ⟨“ x ”⟩ ¬ v = ⟨“ x ”⟩
37 36 iffalsed φ x A v Word A ⟨“ x ”⟩ if v = ⟨“ x ”⟩ 1 0 = 0
38 37 23 suppss2 φ x A v Word A if v = ⟨“ x ”⟩ 1 0 supp 0 ⟨“ x ”⟩
39 suppssfifsupp v Word A if v = ⟨“ x ”⟩ 1 0 V Fun v Word A if v = ⟨“ x ”⟩ 1 0 0 ⟨“ x ”⟩ Fin v Word A if v = ⟨“ x ”⟩ 1 0 supp 0 ⟨“ x ”⟩ finSupp 0 v Word A if v = ⟨“ x ”⟩ 1 0
40 29 30 31 33 38 39 syl32anc φ x A finSupp 0 v Word A if v = ⟨“ x ”⟩ 1 0
41 15 28 40 elrabd φ x A v Word A if v = ⟨“ x ”⟩ 1 0 f Word A | finSupp 0 f
42 41 5 eleqtrrdi φ x A v Word A if v = ⟨“ x ”⟩ 1 0 F
43 eqeq2 x = if w = ⟨“ x ”⟩ x 0 R v Word A if v = ⟨“ x ”⟩ 1 0 w · ˙ M w = x v Word A if v = ⟨“ x ”⟩ 1 0 w · ˙ M w = if w = ⟨“ x ”⟩ x 0 R
44 eqeq2 0 R = if w = ⟨“ x ”⟩ x 0 R v Word A if v = ⟨“ x ”⟩ 1 0 w · ˙ M w = 0 R v Word A if v = ⟨“ x ”⟩ 1 0 w · ˙ M w = if w = ⟨“ x ”⟩ x 0 R
45 eqid v Word A if v = ⟨“ x ”⟩ 1 0 = v Word A if v = ⟨“ x ”⟩ 1 0
46 simpr φ x A w Word A w = ⟨“ x ”⟩ v = w v = w
47 simplr φ x A w Word A w = ⟨“ x ”⟩ v = w w = ⟨“ x ”⟩
48 46 47 eqtrd φ x A w Word A w = ⟨“ x ”⟩ v = w v = ⟨“ x ”⟩
49 48 iftrued φ x A w Word A w = ⟨“ x ”⟩ v = w if v = ⟨“ x ”⟩ 1 0 = 1
50 simplr φ x A w Word A w = ⟨“ x ”⟩ w Word A
51 1zzd φ x A w Word A w = ⟨“ x ”⟩ 1
52 45 49 50 51 fvmptd2 φ x A w Word A w = ⟨“ x ”⟩ v Word A if v = ⟨“ x ”⟩ 1 0 w = 1
53 simpr φ x A w Word A w = ⟨“ x ”⟩ w = ⟨“ x ”⟩
54 53 oveq2d φ x A w Word A w = ⟨“ x ”⟩ M w = M ⟨“ x ”⟩
55 7 sselda φ x A x B
56 55 ad2antrr φ x A w Word A w = ⟨“ x ”⟩ x B
57 2 1 mgpbas B = Base M
58 57 gsumws1 x B M ⟨“ x ”⟩ = x
59 56 58 syl φ x A w Word A w = ⟨“ x ”⟩ M ⟨“ x ”⟩ = x
60 54 59 eqtrd φ x A w Word A w = ⟨“ x ”⟩ M w = x
61 52 60 oveq12d φ x A w Word A w = ⟨“ x ”⟩ v Word A if v = ⟨“ x ”⟩ 1 0 w · ˙ M w = 1 · ˙ x
62 1 3 mulg1 x B 1 · ˙ x = x
63 56 62 syl φ x A w Word A w = ⟨“ x ”⟩ 1 · ˙ x = x
64 61 63 eqtrd φ x A w Word A w = ⟨“ x ”⟩ v Word A if v = ⟨“ x ”⟩ 1 0 w · ˙ M w = x
65 eqeq1 v = w v = ⟨“ x ”⟩ w = ⟨“ x ”⟩
66 65 notbid v = w ¬ v = ⟨“ x ”⟩ ¬ w = ⟨“ x ”⟩
67 66 biimparc ¬ w = ⟨“ x ”⟩ v = w ¬ v = ⟨“ x ”⟩
68 67 adantll φ x A w Word A ¬ w = ⟨“ x ”⟩ v = w ¬ v = ⟨“ x ”⟩
69 68 iffalsed φ x A w Word A ¬ w = ⟨“ x ”⟩ v = w if v = ⟨“ x ”⟩ 1 0 = 0
70 simplr φ x A w Word A ¬ w = ⟨“ x ”⟩ w Word A
71 0zd φ x A w Word A ¬ w = ⟨“ x ”⟩ 0
72 45 69 70 71 fvmptd2 φ x A w Word A ¬ w = ⟨“ x ”⟩ v Word A if v = ⟨“ x ”⟩ 1 0 w = 0
73 72 oveq1d φ x A w Word A ¬ w = ⟨“ x ”⟩ v Word A if v = ⟨“ x ”⟩ 1 0 w · ˙ M w = 0 · ˙ M w
74 2 ringmgp R Ring M Mnd
75 6 74 syl φ M Mnd
76 75 ad3antrrr φ x A w Word A ¬ w = ⟨“ x ”⟩ M Mnd
77 sswrd A B Word A Word B
78 7 77 syl φ Word A Word B
79 78 adantr φ x A Word A Word B
80 79 sselda φ x A w Word A w Word B
81 80 adantr φ x A w Word A ¬ w = ⟨“ x ”⟩ w Word B
82 57 gsumwcl M Mnd w Word B M w B
83 76 81 82 syl2anc φ x A w Word A ¬ w = ⟨“ x ”⟩ M w B
84 eqid 0 R = 0 R
85 1 84 3 mulg0 M w B 0 · ˙ M w = 0 R
86 83 85 syl φ x A w Word A ¬ w = ⟨“ x ”⟩ 0 · ˙ M w = 0 R
87 73 86 eqtrd φ x A w Word A ¬ w = ⟨“ x ”⟩ v Word A if v = ⟨“ x ”⟩ 1 0 w · ˙ M w = 0 R
88 43 44 64 87 ifbothda φ x A w Word A v Word A if v = ⟨“ x ”⟩ 1 0 w · ˙ M w = if w = ⟨“ x ”⟩ x 0 R
89 88 mpteq2dva φ x A w Word A v Word A if v = ⟨“ x ”⟩ 1 0 w · ˙ M w = w Word A if w = ⟨“ x ”⟩ x 0 R
90 89 oveq2d φ x A R w Word A v Word A if v = ⟨“ x ”⟩ 1 0 w · ˙ M w = R w Word A if w = ⟨“ x ”⟩ x 0 R
91 ringmnd R Ring R Mnd
92 6 91 syl φ R Mnd
93 92 adantr φ x A R Mnd
94 simpr φ x A x A
95 94 s1cld φ x A ⟨“ x ”⟩ Word A
96 eqid w Word A if w = ⟨“ x ”⟩ x 0 R = w Word A if w = ⟨“ x ”⟩ x 0 R
97 7 1 sseqtrdi φ A Base R
98 97 sselda φ x A x Base R
99 84 93 23 95 96 98 gsummptif1n0 φ x A R w Word A if w = ⟨“ x ”⟩ x 0 R = x
100 90 99 eqtr2d φ x A x = R w Word A v Word A if v = ⟨“ x ”⟩ 1 0 w · ˙ M w
101 14 42 100 rspcedvdw φ x A g F x = R w Word A g w · ˙ M w
102 9 101 94 elrnmptd φ x A x ran g F R w Word A g w · ˙ M w
103 102 8 eleqtrrdi φ x A x S
104 103 ex φ x A x S
105 104 ssrdv φ A S