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 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 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) → 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) )
114 113 elmaprd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) → 𝑎 : 𝐵 ⟶ 𝐺 )
115 114 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ 𝐻 ) → 𝑎 : 𝐵 ⟶ 𝐺 )
116 115 ffvelcdmda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑎 ‘ 𝑔 ) ∈ 𝐺 )
117 41 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ 𝐻 ) ∧ ¬ 𝑔 ∈ 𝐵 ) → ( 0g ‘ 𝐿 ) ∈ 𝐺 )
118 116 117 ifclda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ 𝐻 ) → if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ∈ 𝐺 )
119 118 fmpttd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) → ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) : 𝐻 ⟶ 𝐺 )
120 111 112 119 elmapdd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) → ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ∈ ( 𝐺 ↑m 𝐻 ) )
121 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) → ( 0g ‘ 𝐿 ) ∈ V )
122 119 ffund ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) → Fun ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) )
123 simprl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) → 𝑎 finSupp ( 0g ‘ 𝐿 ) )
124 114 ffnd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) → 𝑎 Fn 𝐵 )
125 124 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑔 ∈ 𝐵 ) → 𝑎 Fn 𝐵 )
126 12 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑔 ∈ 𝐵 ) → 𝐵 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
127 fvexd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑔 ∈ 𝐵 ) → ( 0g ‘ 𝐿 ) ∈ V )
128 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑔 ∈ 𝐵 ) → 𝑔 ∈ 𝐵 )
129 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑔 ∈ 𝐵 ) → 𝑔 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) )
130 129 eldifbd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑔 ∈ 𝐵 ) → ¬ 𝑔 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) )
131 128 130 eldifd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑔 ∈ 𝐵 ) → 𝑔 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) )
132 125 126 127 131 fvdifsupp ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑎 ‘ 𝑔 ) = ( 0g ‘ 𝐿 ) )
133 eqidd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ ¬ 𝑔 ∈ 𝐵 ) → ( 0g ‘ 𝐿 ) = ( 0g ‘ 𝐿 ) )
134 132 133 ifeqda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) ∧ 𝑔 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) = ( 0g ‘ 𝐿 ) )
135 134 112 suppss2 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) → ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) supp ( 0g ‘ 𝐿 ) ) ⊆ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) )
136 120 121 122 123 135 fsuppsssuppgd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) → ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) finSupp ( 0g ‘ 𝐿 ) )
137 eqid ⊢ ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) = ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) )
138 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ∧ 𝑔 = 𝑓 ) → 𝑔 = 𝑓 )
139 suppssdm ⊢ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ⊆ dom 𝑎
140 114 fdmd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) → dom 𝑎 = 𝐵 )
141 140 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → dom 𝑎 = 𝐵 )
142 139 141 sseqtrid ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ⊆ 𝐵 )
143 142 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) → 𝑓 ∈ 𝐵 )
144 143 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ∧ 𝑔 = 𝑓 ) → 𝑓 ∈ 𝐵 )
145 138 144 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ∧ 𝑔 = 𝑓 ) → 𝑔 ∈ 𝐵 )
146 145 iftrued ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ∧ 𝑔 = 𝑓 ) → if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) = ( 𝑎 ‘ 𝑔 ) )
147 fveq2 ⊢ ( 𝑔 = 𝑓 → ( 𝑎 ‘ 𝑔 ) = ( 𝑎 ‘ 𝑓 ) )
148 147 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ∧ 𝑔 = 𝑓 ) → ( 𝑎 ‘ 𝑔 ) = ( 𝑎 ‘ 𝑓 ) )
149 146 148 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ∧ 𝑔 = 𝑓 ) → if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) = ( 𝑎 ‘ 𝑓 ) )
150 80 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → 𝐵 ⊆ 𝐻 )
151 142 150 sstrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ⊆ 𝐻 )
152 151 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) → 𝑓 ∈ 𝐻 )
153 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) → ( 𝑎 ‘ 𝑓 ) ∈ V )
154 137 149 152 153 fvmptd2 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) → ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) = ( 𝑎 ‘ 𝑓 ) )
155 154 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) → ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) = ( ( 𝑎 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) )
156 155 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ↦ ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) = ( 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ↦ ( ( 𝑎 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) )
157 fveq2 ⊢ ( 𝑓 = 𝑣 → ( 𝑎 ‘ 𝑓 ) = ( 𝑎 ‘ 𝑣 ) )
158 id ⊢ ( 𝑓 = 𝑣 → 𝑓 = 𝑣 )
159 157 158 oveq12d ⊢ ( 𝑓 = 𝑣 → ( ( 𝑎 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) = ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) )
160 159 cbvmptv ⊢ ( 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ↦ ( ( 𝑎 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) = ( 𝑣 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) )
161 156 160 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ↦ ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) = ( 𝑣 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) )
162 161 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝐿 Σg ( 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ↦ ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) = ( 𝐿 Σg ( 𝑣 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) )
163 36 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → 𝐿 ∈ CMnd )
164 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → 𝐻 ∈ ( SubDRing ‘ 𝐿 ) )
165 eleq1w ⊢ ( 𝑔 = 𝑓 → ( 𝑔 ∈ 𝐵 ↔ 𝑓 ∈ 𝐵 ) )
166 165 147 ifbieq1d ⊢ ( 𝑔 = 𝑓 → if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) = if ( 𝑓 ∈ 𝐵 , ( 𝑎 ‘ 𝑓 ) , ( 0g ‘ 𝐿 ) ) )
167 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) )
168 167 eldifad ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → 𝑓 ∈ 𝐻 )
169 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → ( 𝑎 ‘ 𝑓 ) ∈ V )
170 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → ( 0g ‘ 𝐿 ) ∈ V )
171 169 170 ifcld ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → if ( 𝑓 ∈ 𝐵 , ( 𝑎 ‘ 𝑓 ) , ( 0g ‘ 𝐿 ) ) ∈ V )
172 137 166 168 171 fvmptd3 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) = if ( 𝑓 ∈ 𝐵 , ( 𝑎 ‘ 𝑓 ) , ( 0g ‘ 𝐿 ) ) )
173 172 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) = ( if ( 𝑓 ∈ 𝐵 , ( 𝑎 ‘ 𝑓 ) , ( 0g ‘ 𝐿 ) ) ( .r ‘ 𝐿 ) 𝑓 ) )
174 124 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑓 ∈ 𝐵 ) → 𝑎 Fn 𝐵 )
175 12 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑓 ∈ 𝐵 ) → 𝐵 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
176 fvexd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑓 ∈ 𝐵 ) → ( 0g ‘ 𝐿 ) ∈ V )
177 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑓 ∈ 𝐵 ) → 𝑓 ∈ 𝐵 )
178 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑓 ∈ 𝐵 ) → 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) )
179 178 eldifbd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑓 ∈ 𝐵 ) → ¬ 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) )
180 177 179 eldifd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑓 ∈ 𝐵 ) → 𝑓 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) )
181 174 175 176 180 fvdifsupp ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ 𝑓 ∈ 𝐵 ) → ( 𝑎 ‘ 𝑓 ) = ( 0g ‘ 𝐿 ) )
182 eqidd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) ∧ ¬ 𝑓 ∈ 𝐵 ) → ( 0g ‘ 𝐿 ) = ( 0g ‘ 𝐿 ) )
183 181 182 ifeqda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → if ( 𝑓 ∈ 𝐵 , ( 𝑎 ‘ 𝑓 ) , ( 0g ‘ 𝐿 ) ) = ( 0g ‘ 𝐿 ) )
184 183 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → ( if ( 𝑓 ∈ 𝐵 , ( 𝑎 ‘ 𝑓 ) , ( 0g ‘ 𝐿 ) ) ( .r ‘ 𝐿 ) 𝑓 ) = ( ( 0g ‘ 𝐿 ) ( .r ‘ 𝐿 ) 𝑓 ) )
185 35 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → 𝐿 ∈ Ring )
186 164 22 70 3syl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → 𝐻 ⊆ ( Base ‘ 𝐿 ) )
187 186 ssdifssd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ⊆ ( Base ‘ 𝐿 ) )
188 187 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → 𝑓 ∈ ( Base ‘ 𝐿 ) )
189 16 17 18 185 188 ringlzd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → ( ( 0g ‘ 𝐿 ) ( .r ‘ 𝐿 ) 𝑓 ) = ( 0g ‘ 𝐿 ) )
190 173 184 189 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ ( 𝐻 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) = ( 0g ‘ 𝐿 ) )
191 simpr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → 𝑎 finSupp ( 0g ‘ 𝐿 ) )
192 191 fsuppimpd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ∈ Fin )
193 35 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ 𝐻 ) → 𝐿 ∈ Ring )
194 26 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑔 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝐵 ) → 𝐺 ⊆ ( Base ‘ 𝐿 ) )
195 114 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑔 ∈ 𝐻 ) → 𝑎 : 𝐵 ⟶ 𝐺 )
196 195 ffvelcdmda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑔 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑎 ‘ 𝑔 ) ∈ 𝐺 )
197 194 196 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑔 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑎 ‘ 𝑔 ) ∈ ( Base ‘ 𝐿 ) )
198 26 41 sseldd ⊢ ( 𝜑 → ( 0g ‘ 𝐿 ) ∈ ( Base ‘ 𝐿 ) )
199 198 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑔 ∈ 𝐻 ) ∧ ¬ 𝑔 ∈ 𝐵 ) → ( 0g ‘ 𝐿 ) ∈ ( Base ‘ 𝐿 ) )
200 197 199 ifclda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑔 ∈ 𝐻 ) → if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ∈ ( Base ‘ 𝐿 ) )
201 200 fmpttd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) : 𝐻 ⟶ ( Base ‘ 𝐿 ) )
202 201 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ 𝐻 ) → ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ∈ ( Base ‘ 𝐿 ) )
203 186 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ 𝐻 ) → 𝑓 ∈ ( Base ‘ 𝐿 ) )
204 16 17 193 202 203 ringcld ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑓 ∈ 𝐻 ) → ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ∈ ( Base ‘ 𝐿 ) )
205 16 18 163 164 190 192 204 151 gsummptres2 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) = ( 𝐿 Σg ( 𝑓 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ↦ ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) )
206 12 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) → 𝐵 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
207 206 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → 𝐵 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
208 124 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → 𝑎 Fn 𝐵 )
209 207 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → 𝐵 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
210 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → ( 0g ‘ 𝐿 ) ∈ V )
211 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → 𝑣 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) )
212 208 209 210 211 fvdifsupp ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → ( 𝑎 ‘ 𝑣 ) = ( 0g ‘ 𝐿 ) )
213 212 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) = ( ( 0g ‘ 𝐿 ) ( .r ‘ 𝐿 ) 𝑣 ) )
214 35 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → 𝐿 ∈ Ring )
215 81 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → 𝐵 ⊆ ( Base ‘ 𝐿 ) )
216 215 ssdifssd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ⊆ ( Base ‘ 𝐿 ) )
217 216 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → 𝑣 ∈ ( Base ‘ 𝐿 ) )
218 16 17 18 214 217 ringlzd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → ( ( 0g ‘ 𝐿 ) ( .r ‘ 𝐿 ) 𝑣 ) = ( 0g ‘ 𝐿 ) )
219 213 218 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ ( 𝐵 ∖ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ) ) → ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) = ( 0g ‘ 𝐿 ) )
220 35 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ 𝐵 ) → 𝐿 ∈ Ring )
221 26 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ 𝐵 ) → 𝐺 ⊆ ( Base ‘ 𝐿 ) )
222 114 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → 𝑎 : 𝐵 ⟶ 𝐺 )
223 222 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ 𝐵 ) → ( 𝑎 ‘ 𝑣 ) ∈ 𝐺 )
224 221 223 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ 𝐵 ) → ( 𝑎 ‘ 𝑣 ) ∈ ( Base ‘ 𝐿 ) )
225 215 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ 𝐵 ) → 𝑣 ∈ ( Base ‘ 𝐿 ) )
226 16 17 220 224 225 ringcld ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑣 ∈ 𝐵 ) → ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ∈ ( Base ‘ 𝐿 ) )
227 16 18 163 207 219 192 226 142 gsummptres2 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) = ( 𝐿 Σg ( 𝑣 ∈ ( 𝑎 supp ( 0g ‘ 𝐿 ) ) ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) )
228 162 205 227 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) )
229 228 eqeq2d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) → ( 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ↔ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) )
230 229 biimpar ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐿 ) ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) → 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) )
231 230 anasss ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) → 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) )
232 136 231 jca ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) → ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( ( 𝑔 ∈ 𝐻 ↦ if ( 𝑔 ∈ 𝐵 , ( 𝑎 ‘ 𝑔 ) , ( 0g ‘ 𝐿 ) ) ) ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) )
233 110 120 232 rspcedvdw ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) → ∃ 𝑝 ∈ ( 𝐺 ↑m 𝐻 ) ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) )
234 233 r19.29an ⊢ ( ( 𝜑 ∧ ∃ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) → ∃ 𝑝 ∈ ( 𝐺 ↑m 𝐻 ) ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) )
235 103 234 impbida ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ( 𝐺 ↑m 𝐻 ) ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) ↔ ∃ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑣 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑣 ) ( .r ‘ 𝐿 ) 𝑣 ) ) ) ) ) )
236 59 84 235 3bitr4rd ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ( 𝐺 ↑m 𝐻 ) ( 𝑝 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑥 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑝 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) ) ↔ 𝑥 ∈ ( ( LSpan ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) ‘ 𝐵 ) ) )
237 15 24 236 3bitrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↔ 𝑥 ∈ ( ( LSpan ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) ‘ 𝐵 ) ) )
238 237 eqrdv ⊢ ( 𝜑 → 𝐶 = ( ( LSpan ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐺 ) ) ‘ 𝐵 ) )