Metamath Proof Explorer

Theorem fldextrspunlsp

Description: Lemma for fldextrspunfld . The subring generated by the union of two field extensions G and H is the vector sub- G space generated by a basis B of H . Part of the proof of Proposition 5, Chapter 5, of BourbakiAlg2 p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025)

Ref Expression
Hypotheses fldextrspunfld.k ⊢ 𝐾 = ( 𝐿 ↾s 𝐹 )
fldextrspunfld.i ⊢ 𝐼 = ( 𝐿 ↾s 𝐺 )
fldextrspunfld.j ⊢ 𝐽 = ( 𝐿 ↾s 𝐻 )
fldextrspunfld.2 ⊢ ( 𝜑 → 𝐿 ∈ Field )
fldextrspunfld.3 ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐼 ) )
fldextrspunfld.4 ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐽 ) )
fldextrspunfld.5 ⊢ ( 𝜑 → 𝐺 ∈ ( SubDRing ‘ 𝐿 ) )
fldextrspunfld.6 ⊢ ( 𝜑 → 𝐻 ∈ ( SubDRing ‘ 𝐿 ) )
fldextrspunlsp.n ⊢ 𝑁 = ( RingSpan ‘ 𝐿 )
fldextrspunlsp.c ⊢ 𝐶 = ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) )
fldextrspunlsp.e ⊢ 𝐸 = ( 𝐿 ↾s 𝐶 )
fldextrspunlsp.1 ⊢ ( 𝜑 → 𝐵 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
fldextrspunlsp.2 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
Assertion fldextrspunlsp ( 𝜑 → 𝐶 = ( ( LSpan ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fldextrspunfld.k ⊢ 𝐾 = ( 𝐿 ↾s 𝐹 )
2 fldextrspunfld.i ⊢ 𝐼 = ( 𝐿 ↾s 𝐺 )
3 fldextrspunfld.j ⊢ 𝐽 = ( 𝐿 ↾s 𝐻 )
4 fldextrspunfld.2 ⊢ ( 𝜑 → 𝐿 ∈ Field )
5 fldextrspunfld.3 ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐼 ) )
6 fldextrspunfld.4 ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐽 ) )
7 fldextrspunfld.5 ⊢ ( 𝜑 → 𝐺 ∈ ( SubDRing ‘ 𝐿 ) )
8 fldextrspunfld.6 ⊢ ( 𝜑 → 𝐻 ∈ ( SubDRing ‘ 𝐿 ) )
9 fldextrspunlsp.n ⊢ 𝑁 = ( RingSpan ‘ 𝐿 )
10 fldextrspunlsp.c ⊢ 𝐶 = ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) )
11 fldextrspunlsp.e ⊢ 𝐸 = ( 𝐿 ↾s 𝐶 )
12 fldextrspunlsp.1 ⊢ ( 𝜑 → 𝐵 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
13 fldextrspunlsp.2 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
14 10 a1i ⊢ ( 𝜑 → 𝐶 = ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) )
15 14 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↔ 𝑥 ∈ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) ) )
16 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
17 eqid ⊢ ( .r ‘ 𝐿 ) = ( .r ‘ 𝐿 )
18 eqid ⊢ ( 0g ‘ 𝐿 ) = ( 0g ‘ 𝐿 )
19 4 fldcrngd ⊢ ( 𝜑 → 𝐿 ∈ CRing )
20 sdrgsubrg ⊢ ( 𝐺 ∈ ( SubDRing ‘ 𝐿 ) → 𝐺 ∈ ( SubRing ‘ 𝐿 ) )
21 7 20 syl ⊢ ( 𝜑 → 𝐺 ∈ ( SubRing ‘ 𝐿 ) )
22 sdrgsubrg ⊢ ( 𝐻 ∈ ( SubDRing ‘ 𝐿 ) → 𝐻 ∈ ( SubRing ‘ 𝐿 ) )
23 8 22 syl ⊢ ( 𝜑 → 𝐻 ∈ ( SubRing ‘ 𝐿 ) )
24 16 17 18 9 19 21 23 elrgspnsubrun ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) ↔ ∃ 𝑝 ∈ ( 𝐺 ↑m 𝐻 ) ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) ) )
25 16 subrgss ⊢ ( 𝐺 ∈ ( SubRing ‘ 𝐿 ) → 𝐺 ⊆ ( Base ‘ 𝐿 ) )
26 21 25 syl ⊢ ( 𝜑 → 𝐺 ⊆ ( Base ‘ 𝐿 ) )
27 eqid ⊢ ( 𝐿 ↾s 𝐺 ) = ( 𝐿 ↾s 𝐺 )
28 27 16 ressbas2 ⊢ ( 𝐺 ⊆ ( Base ‘ 𝐿 ) → 𝐺 = ( Base ‘ ( 𝐿 ↾s 𝐺 ) ) )
29 26 28 syl ⊢ ( 𝜑 → 𝐺 = ( Base ‘ ( 𝐿 ↾s 𝐺 ) ) )
30 eqidd ⊢ ( 𝜑 → ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) = ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) )
31 30 26 srasca ⊢ ( 𝜑 → ( 𝐿 ↾s 𝐺 ) = ( Scalar ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) )
32 31 fveq2d ⊢ ( 𝜑 → ( Base ‘ ( 𝐿 ↾s 𝐺 ) ) = ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) ) )
33 29 32 eqtr2d ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) ) = 𝐺 )
34 33 oveq1d ⊢ ( 𝜑 → ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) ) ↑m 𝐵 ) = ( 𝐺 ↑m 𝐵 ) )
35 19 crngringd ⊢ ( 𝜑 → 𝐿 ∈ Ring )
36 35 ringcmnd ⊢ ( 𝜑 → 𝐿 ∈ CMnd )
37 36 cmnmndd ⊢ ( 𝜑 → 𝐿 ∈ Mnd )
38 subrgsubg ⊢ ( 𝐺 ∈ ( SubRing ‘ 𝐿 ) → 𝐺 ∈ ( SubGrp ‘ 𝐿 ) )
39 21 38 syl ⊢ ( 𝜑 → 𝐺 ∈ ( SubGrp ‘ 𝐿 ) )
40 18 subg0cl ⊢ ( 𝐺 ∈ ( SubGrp ‘ 𝐿 ) → ( 0g ‘ 𝐿 ) ∈ 𝐺 )
41 39 40 syl ⊢ ( 𝜑 → ( 0g ‘ 𝐿 ) ∈ 𝐺 )
42 27 16 18 ress0g ⊢ ( ( 𝐿 ∈ Mnd ∧ ( 0g ‘ 𝐿 ) ∈ 𝐺 ∧ 𝐺 ⊆ ( Base ‘ 𝐿 ) ) → ( 0g ‘ 𝐿 ) = ( 0g ‘ ( 𝐿 ↾s 𝐺 ) ) )
43 37 41 26 42 syl3anc ⊢ ( 𝜑 → ( 0g ‘ 𝐿 ) = ( 0g ‘ ( 𝐿 ↾s 𝐺 ) ) )
44 31 fveq2d ⊢ ( 𝜑 → ( 0g ‘ ( 𝐿 ↾s 𝐺 ) ) = ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) ) )
45 43 44 eqtr2d ⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) ) = ( 0g ‘ 𝐿 ) )
46 45 breq2d ⊢ ( 𝜑 → ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) ) ↔ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) )
47 eqid ⊢ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) = ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 )
48 12 mptexd ⊢ ( 𝜑 → ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ∈ V )
49 47 sralmod ⊢ ( 𝐺 ∈ ( SubRing ‘ 𝐿 ) → ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ∈ LMod )
50 21 49 syl ⊢ ( 𝜑 → ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ∈ LMod )
51 47 48 4 50 26 gsumsra ⊢ ( 𝜑 → ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) = ( ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) )
52 30 26 sravsca ⊢ ( 𝜑 → ( .r ‘ 𝐿 ) = ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) )
53 52 oveqd ⊢ ( 𝜑 → ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) = ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) 𝑣 ) )
54 53 mpteq2dv ⊢ ( 𝜑 → ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) = ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) 𝑣 ) ) )
55 54 oveq2d ⊢ ( 𝜑 → ( ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) = ( ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) 𝑣 ) ) ) )
56 51 55 eqtr2d ⊢ ( 𝜑 → ( ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) 𝑣 ) ) ) = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) )
57 56 eqeq2d ⊢ ( 𝜑 → ( 𝑥 = ( ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) 𝑣 ) ) ) ↔ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) )
58 46 57 anbi12d ⊢ ( 𝜑 → ( ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) ) ∧ 𝑥 = ( ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) 𝑣 ) ) ) ) ↔ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) )
59 34 58 rexeqbidv ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) ) ↑m 𝐵 ) ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) ) ∧ 𝑥 = ( ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) 𝑣 ) ) ) ) ↔ ∃ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) )
60 eqid ⊢ ( LSpan ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) = ( LSpan ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) )
61 eqid ⊢ ( Base ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) = ( Base ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) )
62 eqid ⊢ ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) ) = ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) )
63 eqid ⊢ ( Scalar ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) = ( Scalar ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) )
64 eqid ⊢ ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) ) = ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) )
65 eqid ⊢ ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) = ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) )
66 eqid ⊢ ( Base ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) = ( Base ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) )
67 eqid ⊢ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) = ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) )
68 66 67 lbsss ⊢ ( 𝐵 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) → 𝐵 ⊆ ( Base ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
69 12 68 syl ⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
70 16 subrgss ⊢ ( 𝐻 ∈ ( SubRing ‘ 𝐿 ) → 𝐻 ⊆ ( Base ‘ 𝐿 ) )
71 23 70 syl ⊢ ( 𝜑 → 𝐻 ⊆ ( Base ‘ 𝐿 ) )
72 3 16 ressbas2 ⊢ ( 𝐻 ⊆ ( Base ‘ 𝐿 ) → 𝐻 = ( Base ‘ 𝐽 ) )
73 71 72 syl ⊢ ( 𝜑 → 𝐻 = ( Base ‘ 𝐽 ) )
74 eqidd ⊢ ( 𝜑 → ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) = ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) )
75 eqid ⊢ ( Base ‘ 𝐽 ) = ( Base ‘ 𝐽 )
76 75 sdrgss ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐽 ) → 𝐹 ⊆ ( Base ‘ 𝐽 ) )
77 6 76 syl ⊢ ( 𝜑 → 𝐹 ⊆ ( Base ‘ 𝐽 ) )
78 74 77 srabase ⊢ ( 𝜑 → ( Base ‘ 𝐽 ) = ( Base ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
79 73 78 eqtrd ⊢ ( 𝜑 → 𝐻 = ( Base ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
80 69 79 sseqtrrd ⊢ ( 𝜑 → 𝐵 ⊆ 𝐻 )
81 80 71 sstrd ⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ 𝐿 ) )
82 30 26 srabase ⊢ ( 𝜑 → ( Base ‘ 𝐿 ) = ( Base ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) )
83 81 82 sseqtrd ⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) )
84 60 61 62 63 64 65 50 83 ellspds ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( LSpan ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) ‘ 𝐵 ) ↔ ∃ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) ) ↑m 𝐵 ) ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) ) ∧ 𝑥 = ( ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) 𝑣 ) ) ) ) ) )
85 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐺 ↑m 𝐻 ) ) ∧ ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) ) → 𝐿 ∈ Field )
86 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐺 ↑m 𝐻 ) ) ∧ ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) ) → 𝐹 ∈ ( SubDRing ‘ 𝐼 ) )
87 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐺 ↑m 𝐻 ) ) ∧ ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) ) → 𝐹 ∈ ( SubDRing ‘ 𝐽 ) )
88 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐺 ↑m 𝐻 ) ) ∧ ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) ) → 𝐺 ∈ ( SubDRing ‘ 𝐿 ) )
89 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐺 ↑m 𝐻 ) ) ∧ ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) ) → 𝐻 ∈ ( SubDRing ‘ 𝐿 ) )
90 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐺 ↑m 𝐻 ) ) ∧ ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) ) → 𝐵 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
91 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐺 ↑m 𝐻 ) ) ∧ ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) ) → 𝐵 ∈ Fin )
92 simplr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐺 ↑m 𝐻 ) ) ∧ ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) ) → 𝑝 ∈ ( 𝐺 ↑m 𝐻 ) )
93 89 88 92 elmaprd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐺 ↑m 𝐻 ) ) ∧ ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) ) → 𝑝 : 𝐻 ⟶ 𝐺 )
94 simprl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐺 ↑m 𝐻 ) ) ∧ ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) ) → 𝑝 finSupp ( 0g ‘ 𝐿 ) )
95 simprr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐺 ↑m 𝐻 ) ) ∧ ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) ) → 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) )
96 fveq2 ⊢ ( 𝑓 = ℎ → ( 𝑝 ‘ 𝑓 ) = ( 𝑝 ‘ ℎ ) )
97 id ⊢ ( 𝑓 = ℎ → 𝑓 = ℎ )
98 96 97 oveq12d ⊢ ( 𝑓 = ℎ → ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) = ( ( 𝑝 ‘ ℎ ) ( .r ‘ 𝐿 ) ℎ ) )
99 98 cbvmptv ⊢ ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) = ( ℎ ∈ 𝐻 ↦ ( ( 𝑝 ‘ ℎ ) ( .r ‘ 𝐿 ) ℎ ) )
100 99 oveq2i ⊢ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) = ( 𝐿 Σg ( ℎ ∈ 𝐻 ↦ ( ( 𝑝 ‘ ℎ ) ( .r ‘ 𝐿 ) ℎ ) ) )
101 95 100 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐺 ↑m 𝐻 ) ) ∧ ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) ) → 𝑥 = ( 𝐿 Σg ( ℎ ∈ 𝐻 ↦ ( ( 𝑝 ‘ ℎ ) ( .r ‘ 𝐿 ) ℎ ) ) ) )
102 1 2 3 85 86 87 88 89 9 10 11 90 91 93 94 101 fldextrspunlsplem ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐺 ↑m 𝐻 ) ) ∧ ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) ) → ∃ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) )
103 102 r19.29an ⊢ ( ( 𝜑 ∧ ∃ 𝑝 ∈ ( 𝐺 ↑m 𝐻 ) ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) ) → ∃ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) )
104 breq1 ⊢ ( 𝑝 = ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) → ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ↔ ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) finSupp ( 0g ‘ 𝐿 ) ) )
105 fveq1 ⊢ ( 𝑝 = ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) → ( 𝑝 ‘ 𝑓 ) = ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) )
106 105 oveq1d ⊢ ( 𝑝 = ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) → ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) = ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) )
107 106 mpteq2dv ⊢ ( 𝑝 = ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) → ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) = ( 𝑓 ∈ 𝐻 ↦ ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) )
108 107 oveq2d ⊢ ( 𝑝 = ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) → ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) )
109 108 eqeq2d ⊢ ( 𝑝 = ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) → ( 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ↔ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) )
110 104 109 anbi12d ⊢ ( 𝑝 = ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) → ( ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) ↔ ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) ) )
111 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) → 𝐺 ∈ ( SubDRing ‘ 𝐿 ) )
112 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) → 𝐻 ∈ ( SubDRing ‘ 𝐿 ) )
113 12 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) → 𝐵 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
114 7 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) → 𝐺 ∈ ( SubDRing ‘ 𝐿 ) )
115 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) → 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) )
116 113 114 115 elmaprd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) → 𝑎 : 𝐵 ⟶ 𝐺 )
117 116 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ 𝐻 ) → 𝑎 : 𝐵 ⟶ 𝐺 )
118 117 ffvelcdmda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑎 ‘ 𝑔 ) ∈ 𝐺 )
119 41 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ 𝐻 ) ∧ ¬ 𝑔 ∈ 𝐵 ) → ( 0g ‘ 𝐿 ) ∈ 𝐺 )
120 118 119 ifclda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ 𝐻 ) → if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ∈ 𝐺 )
121 120 fmpttd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) → ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) : 𝐻 ⟶ 𝐺 )
122 111 112 121 elmapdd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) → ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ∈ ( 𝐺 ↑m 𝐻 ) )
123 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) → ( 0g ‘ 𝐿 ) ∈ V )
124 121 ffund ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) → Fun ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) )
125 simprl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) → 𝑎 finSupp ( 0g ‘ 𝐿 ) )
126 116 ffnd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) → 𝑎 Fn 𝐵 )
127 126 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑔 ∈ 𝐵 ) → 𝑎 Fn 𝐵 )
128 12 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑔 ∈ 𝐵 ) → 𝐵 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
129 fvexd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑔 ∈ 𝐵 ) → ( 0g ‘ 𝐿 ) ∈ V )
130 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑔 ∈ 𝐵 ) → 𝑔 ∈ 𝐵 )
131 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑔 ∈ 𝐵 ) → 𝑔 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) )
132 131 eldifbd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑔 ∈ 𝐵 ) → ¬ 𝑔 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) )
133 130 132 eldifd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑔 ∈ 𝐵 ) → 𝑔 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) )
134 127 128 129 133 fvdifsupp ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑎 ‘ 𝑔 ) = ( 0g ‘ 𝐿 ) )
135 eqidd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ ¬ 𝑔 ∈ 𝐵 ) → ( 0g ‘ 𝐿 ) = ( 0g ‘ 𝐿 ) )
136 134 135 ifeqda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) = ( 0g ‘ 𝐿 ) )
137 136 112 suppss2 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) → ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) supp ( 0g ‘ 𝐿 ) ) ⊆ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) )
138 122 123 124 125 137 fsuppsssuppgd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) → ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) finSupp ( 0g ‘ 𝐿 ) )
139 eqid ⊢ ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) = ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) )
140 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ∧ 𝑔 = 𝑓 ) → 𝑔 = 𝑓 )
141 suppssdm ⊢ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ⊆ dom 𝑎
142 116 fdmd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) → dom 𝑎 = 𝐵 )
143 142 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → dom 𝑎 = 𝐵 )
144 141 143 sseqtrid ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ⊆ 𝐵 )
145 144 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) → 𝑓 ∈ 𝐵 )
146 145 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ∧ 𝑔 = 𝑓 ) → 𝑓 ∈ 𝐵 )
147 140 146 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ∧ 𝑔 = 𝑓 ) → 𝑔 ∈ 𝐵 )
148 147 iftrued ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ∧ 𝑔 = 𝑓 ) → if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) = ( 𝑎 ‘ 𝑔 ) )
149 fveq2 ⊢ ( 𝑔 = 𝑓 → ( 𝑎 ‘ 𝑔 ) = ( 𝑎 ‘ 𝑓 ) )
150 149 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ∧ 𝑔 = 𝑓 ) → ( 𝑎 ‘ 𝑔 ) = ( 𝑎 ‘ 𝑓 ) )
151 148 150 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ∧ 𝑔 = 𝑓 ) → if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) = ( 𝑎 ‘ 𝑓 ) )
152 80 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → 𝐵 ⊆ 𝐻 )
153 144 152 sstrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ⊆ 𝐻 )
154 153 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) → 𝑓 ∈ 𝐻 )
155 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) → ( 𝑎 ‘ 𝑓 ) ∈ V )
156 139 151 154 155 fvmptd2 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) → ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) = ( 𝑎 ‘ 𝑓 ) )
157 156 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) → ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) = ( ( 𝑎 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) )
158 157 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ↦ ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) = ( 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ↦ ( ( 𝑎 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) )
159 fveq2 ⊢ ( 𝑓 = 𝑣 → ( 𝑎 ‘ 𝑓 ) = ( 𝑎 ‘ 𝑣 ) )
160 id ⊢ ( 𝑓 = 𝑣 → 𝑓 = 𝑣 )
161 159 160 oveq12d ⊢ ( 𝑓 = 𝑣 → ( ( 𝑎 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) = ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) )
162 161 cbvmptv ⊢ ( 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ↦ ( ( 𝑎 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) = ( 𝑣 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) )
163 158 162 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ↦ ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) = ( 𝑣 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) )
164 163 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝐿 Σg ( 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ↦ ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) = ( 𝐿 Σg ( 𝑣 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) )
165 36 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → 𝐿 ∈ CMnd )
166 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → 𝐻 ∈ ( SubDRing ‘ 𝐿 ) )
167 eleq1w ⊢ ( 𝑔 = 𝑓 → ( 𝑔 ∈ 𝐵 ↔ 𝑓 ∈ 𝐵 ) )
168 167 149 ifbieq1d ⊢ ( 𝑔 = 𝑓 → if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) = if ( 𝑓 ∈ 𝐵 , ( 𝑎 ‘ 𝑓 ) , ( 0g ‘ 𝐿 ) ) )
169 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) )
170 169 eldifad ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → 𝑓 ∈ 𝐻 )
171 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → ( 𝑎 ‘ 𝑓 ) ∈ V )
172 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → ( 0g ‘ 𝐿 ) ∈ V )
173 171 172 ifcld ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → if ( 𝑓 ∈ 𝐵 , ( 𝑎 ‘ 𝑓 ) , ( 0g ‘ 𝐿 ) ) ∈ V )
174 139 168 170 173 fvmptd3 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) = if ( 𝑓 ∈ 𝐵 , ( 𝑎 ‘ 𝑓 ) , ( 0g ‘ 𝐿 ) ) )
175 174 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) = ( if ( 𝑓 ∈ 𝐵 , ( 𝑎 ‘ 𝑓 ) , ( 0g ‘ 𝐿 ) ) ( .r ‘ 𝐿 ) 𝑓 ) )
176 126 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑓 ∈ 𝐵 ) → 𝑎 Fn 𝐵 )
177 12 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑓 ∈ 𝐵 ) → 𝐵 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
178 fvexd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑓 ∈ 𝐵 ) → ( 0g ‘ 𝐿 ) ∈ V )
179 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑓 ∈ 𝐵 ) → 𝑓 ∈ 𝐵 )
180 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑓 ∈ 𝐵 ) → 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) )
181 180 eldifbd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑓 ∈ 𝐵 ) → ¬ 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) )
182 179 181 eldifd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑓 ∈ 𝐵 ) → 𝑓 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) )
183 176 177 178 182 fvdifsupp ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑓 ∈ 𝐵 ) → ( 𝑎 ‘ 𝑓 ) = ( 0g ‘ 𝐿 ) )
184 eqidd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ ¬ 𝑓 ∈ 𝐵 ) → ( 0g ‘ 𝐿 ) = ( 0g ‘ 𝐿 ) )
185 183 184 ifeqda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → if ( 𝑓 ∈ 𝐵 , ( 𝑎 ‘ 𝑓 ) , ( 0g ‘ 𝐿 ) ) = ( 0g ‘ 𝐿 ) )
186 185 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → ( if ( 𝑓 ∈ 𝐵 , ( 𝑎 ‘ 𝑓 ) , ( 0g ‘ 𝐿 ) ) ( .r ‘ 𝐿 ) 𝑓 ) = ( ( 0g ‘ 𝐿 ) ( .r ‘ 𝐿 ) 𝑓 ) )
187 35 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → 𝐿 ∈ Ring )
188 166 22 70 3syl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → 𝐻 ⊆ ( Base ‘ 𝐿 ) )
189 188 ssdifssd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ⊆ ( Base ‘ 𝐿 ) )
190 189 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → 𝑓 ∈ ( Base ‘ 𝐿 ) )
191 16 17 18 187 190 ringlzd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → ( ( 0g ‘ 𝐿 ) ( .r ‘ 𝐿 ) 𝑓 ) = ( 0g ‘ 𝐿 ) )
192 175 186 191 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) = ( 0g ‘ 𝐿 ) )
193 simpr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → 𝑎 finSupp ( 0g ‘ 𝐿 ) )
194 193 fsuppimpd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ∈ Fin )
195 35 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ 𝐻 ) → 𝐿 ∈ Ring )
196 26 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑔 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝐵 ) → 𝐺 ⊆ ( Base ‘ 𝐿 ) )
197 116 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑔 ∈ 𝐻 ) → 𝑎 : 𝐵 ⟶ 𝐺 )
198 197 ffvelcdmda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑔 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑎 ‘ 𝑔 ) ∈ 𝐺 )
199 196 198 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑔 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑎 ‘ 𝑔 ) ∈ ( Base ‘ 𝐿 ) )
200 26 41 sseldd ⊢ ( 𝜑 → ( 0g ‘ 𝐿 ) ∈ ( Base ‘ 𝐿 ) )
201 200 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑔 ∈ 𝐻 ) ∧ ¬ 𝑔 ∈ 𝐵 ) → ( 0g ‘ 𝐿 ) ∈ ( Base ‘ 𝐿 ) )
202 199 201 ifclda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑔 ∈ 𝐻 ) → if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ∈ ( Base ‘ 𝐿 ) )
203 202 fmpttd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) : 𝐻 ⟶ ( Base ‘ 𝐿 ) )
204 203 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ 𝐻 ) → ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ∈ ( Base ‘ 𝐿 ) )
205 188 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ 𝐻 ) → 𝑓 ∈ ( Base ‘ 𝐿 ) )
206 16 17 195 204 205 ringcld ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ 𝐻 ) → ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ∈ ( Base ‘ 𝐿 ) )
207 16 18 165 166 192 194 206 153 gsummptres2 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) = ( 𝐿 Σg ( 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ↦ ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) )
208 113 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → 𝐵 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
209 126 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → 𝑎 Fn 𝐵 )
210 208 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → 𝐵 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
211 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → ( 0g ‘ 𝐿 ) ∈ V )
212 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → 𝑣 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) )
213 209 210 211 212 fvdifsupp ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → ( 𝑎 ‘ 𝑣 ) = ( 0g ‘ 𝐿 ) )
214 213 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) = ( ( 0g ‘ 𝐿 ) ( .r ‘ 𝐿 ) 𝑣 ) )
215 35 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → 𝐿 ∈ Ring )
216 81 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → 𝐵 ⊆ ( Base ‘ 𝐿 ) )
217 216 ssdifssd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ⊆ ( Base ‘ 𝐿 ) )
218 217 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → 𝑣 ∈ ( Base ‘ 𝐿 ) )
219 16 17 18 215 218 ringlzd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → ( ( 0g ‘ 𝐿 ) ( .r ‘ 𝐿 ) 𝑣 ) = ( 0g ‘ 𝐿 ) )
220 214 219 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) = ( 0g ‘ 𝐿 ) )
221 35 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ 𝐵 ) → 𝐿 ∈ Ring )
222 26 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ 𝐵 ) → 𝐺 ⊆ ( Base ‘ 𝐿 ) )
223 116 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → 𝑎 : 𝐵 ⟶ 𝐺 )
224 223 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ 𝐵 ) → ( 𝑎 ‘ 𝑣 ) ∈ 𝐺 )
225 222 224 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ 𝐵 ) → ( 𝑎 ‘ 𝑣 ) ∈ ( Base ‘ 𝐿 ) )
226 216 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ 𝐵 ) → 𝑣 ∈ ( Base ‘ 𝐿 ) )
227 16 17 221 225 226 ringcld ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ 𝐵 ) → ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ∈ ( Base ‘ 𝐿 ) )
228 16 18 165 208 220 194 227 144 gsummptres2 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) = ( 𝐿 Σg ( 𝑣 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) )
229 164 207 228 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) )
230 229 eqeq2d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ↔ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) )
231 230 biimpar ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) → 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) )
232 231 anasss ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) → 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) )
233 138 232 jca ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) → ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) )
234 110 122 233 rspcedvdw ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) → ∃ 𝑝 ∈ ( 𝐺 ↑m 𝐻 ) ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) )
235 234 r19.29an ⊢ ( ( 𝜑 ∧ ∃ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) → ∃ 𝑝 ∈ ( 𝐺 ↑m 𝐻 ) ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) )
236 103 235 impbida ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ( 𝐺 ↑m 𝐻 ) ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) ↔ ∃ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) )
237 59 84 236 3bitr4rd ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ( 𝐺 ↑m 𝐻 ) ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) ↔ 𝑥 ∈ ( ( LSpan ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) ‘ 𝐵 ) ) )
238 15 24 237 3bitrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↔ 𝑥 ∈ ( ( LSpan ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) ‘ 𝐵 ) ) )
239 238 eqrdv ⊢ ( 𝜑 → 𝐶 = ( ( LSpan ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) ‘ 𝐵 ) )