This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fldextrspunlsplem

Description: Lemma for fldextrspunlsp : First direction. 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 )
fldextrspunlsplem.2 ⊢ ( 𝜑 → 𝑃 : 𝐻 ⟶ 𝐺 )
fldextrspunlsplem.3 ⊢ ( 𝜑 → 𝑃 finSupp ( 0g ‘ 𝐿 ) )
fldextrspunlsplem.4 ⊢ ( 𝜑 → 𝑋 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) )
Assertion fldextrspunlsplem ( 𝜑 → ∃ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑋 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) )

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 fldextrspunlsplem.2 ⊢ ( 𝜑 → 𝑃 : 𝐻 ⟶ 𝐺 )
15 fldextrspunlsplem.3 ⊢ ( 𝜑 → 𝑃 finSupp ( 0g ‘ 𝐿 ) )
16 fldextrspunlsplem.4 ⊢ ( 𝜑 → 𝑋 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) )
17 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → 𝐺 ∈ ( SubDRing ‘ 𝐿 ) )
18 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → 𝐵 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
19 eqid ⊢ ( 0g ‘ 𝐿 ) = ( 0g ‘ 𝐿 )
20 4 flddrngd ⊢ ( 𝜑 → 𝐿 ∈ DivRing )
21 20 drngringd ⊢ ( 𝜑 → 𝐿 ∈ Ring )
22 21 ringcmnd ⊢ ( 𝜑 → 𝐿 ∈ CMnd )
23 22 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) → 𝐿 ∈ CMnd )
24 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) → 𝐻 ∈ ( SubDRing ‘ 𝐿 ) )
25 sdrgsubrg ⊢ ( 𝐺 ∈ ( SubDRing ‘ 𝐿 ) → 𝐺 ∈ ( SubRing ‘ 𝐿 ) )
26 7 25 syl ⊢ ( 𝜑 → 𝐺 ∈ ( SubRing ‘ 𝐿 ) )
27 subrgsubg ⊢ ( 𝐺 ∈ ( SubRing ‘ 𝐿 ) → 𝐺 ∈ ( SubGrp ‘ 𝐿 ) )
28 subgsubm ⊢ ( 𝐺 ∈ ( SubGrp ‘ 𝐿 ) → 𝐺 ∈ ( SubMnd ‘ 𝐿 ) )
29 26 27 28 3syl ⊢ ( 𝜑 → 𝐺 ∈ ( SubMnd ‘ 𝐿 ) )
30 29 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) → 𝐺 ∈ ( SubMnd ‘ 𝐿 ) )
31 eqid ⊢ ( .r ‘ 𝐿 ) = ( .r ‘ 𝐿 )
32 26 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑓 ∈ 𝐻 ) → 𝐺 ∈ ( SubRing ‘ 𝐿 ) )
33 14 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑓 ∈ 𝐻 ) → 𝑃 : 𝐻 ⟶ 𝐺 )
34 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑓 ∈ 𝐻 ) → 𝑓 ∈ 𝐻 )
35 33 34 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑓 ∈ 𝐻 ) → ( 𝑃 ‘ 𝑓 ) ∈ 𝐺 )
36 eqid ⊢ ( Base ‘ 𝐼 ) = ( Base ‘ 𝐼 )
37 36 sdrgss ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐼 ) → 𝐹 ⊆ ( Base ‘ 𝐼 ) )
38 5 37 syl ⊢ ( 𝜑 → 𝐹 ⊆ ( Base ‘ 𝐼 ) )
39 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
40 39 sdrgss ⊢ ( 𝐺 ∈ ( SubDRing ‘ 𝐿 ) → 𝐺 ⊆ ( Base ‘ 𝐿 ) )
41 7 40 syl ⊢ ( 𝜑 → 𝐺 ⊆ ( Base ‘ 𝐿 ) )
42 2 39 ressbas2 ⊢ ( 𝐺 ⊆ ( Base ‘ 𝐿 ) → 𝐺 = ( Base ‘ 𝐼 ) )
43 41 42 syl ⊢ ( 𝜑 → 𝐺 = ( Base ‘ 𝐼 ) )
44 38 43 sseqtrrd ⊢ ( 𝜑 → 𝐹 ⊆ 𝐺 )
45 44 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑓 ∈ 𝐻 ) → 𝐹 ⊆ 𝐺 )
46 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑓 ∈ 𝐻 ) → 𝐵 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
47 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑓 ∈ 𝐻 ) → 𝐹 ∈ ( SubDRing ‘ 𝐼 ) )
48 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑓 ∈ 𝐻 ) → 𝐻 ∈ ( SubDRing ‘ 𝐿 ) )
49 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑓 ∈ 𝐻 ) → ( 𝐹 ↑m 𝐵 ) ∈ V )
50 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑓 ∈ 𝐻 ) → 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) )
51 48 49 50 elmaprd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑓 ∈ 𝐻 ) → 𝑢 : 𝐻 ⟶ ( 𝐹 ↑m 𝐵 ) )
52 51 34 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑓 ∈ 𝐻 ) → ( 𝑢 ‘ 𝑓 ) ∈ ( 𝐹 ↑m 𝐵 ) )
53 46 47 52 elmaprd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑓 ∈ 𝐻 ) → ( 𝑢 ‘ 𝑓 ) : 𝐵 ⟶ 𝐹 )
54 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑓 ∈ 𝐻 ) → 𝑐 ∈ 𝐵 )
55 53 54 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑓 ∈ 𝐻 ) → ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ∈ 𝐹 )
56 45 55 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑓 ∈ 𝐻 ) → ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ∈ 𝐺 )
57 31 32 35 56 subrgmcld ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑓 ∈ 𝐻 ) → ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ∈ 𝐺 )
58 57 fmpttd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑐 ∈ 𝐵 ) → ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) : 𝐻 ⟶ 𝐺 )
59 58 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) → ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) : 𝐻 ⟶ 𝐺 )
60 fveq2 ⊢ ( 𝑓 = ℎ → ( 𝑃 ‘ 𝑓 ) = ( 𝑃 ‘ ℎ ) )
61 fveq2 ⊢ ( 𝑓 = ℎ → ( 𝑢 ‘ 𝑓 ) = ( 𝑢 ‘ ℎ ) )
62 61 fveq1d ⊢ ( 𝑓 = ℎ → ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) = ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) )
63 60 62 oveq12d ⊢ ( 𝑓 = ℎ → ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) = ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) )
64 63 cbvmptv ⊢ ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) = ( ℎ ∈ 𝐻 ↦ ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) )
65 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) → ( 0g ‘ 𝐿 ) ∈ V )
66 ssidd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) → 𝐻 ⊆ 𝐻 )
67 eqid ⊢ ( Base ‘ 𝐽 ) = ( Base ‘ 𝐽 )
68 67 sdrgss ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐽 ) → 𝐹 ⊆ ( Base ‘ 𝐽 ) )
69 6 68 syl ⊢ ( 𝜑 → 𝐹 ⊆ ( Base ‘ 𝐽 ) )
70 39 sdrgss ⊢ ( 𝐻 ∈ ( SubDRing ‘ 𝐿 ) → 𝐻 ⊆ ( Base ‘ 𝐿 ) )
71 8 70 syl ⊢ ( 𝜑 → 𝐻 ⊆ ( Base ‘ 𝐿 ) )
72 3 39 ressbas2 ⊢ ( 𝐻 ⊆ ( Base ‘ 𝐿 ) → 𝐻 = ( Base ‘ 𝐽 ) )
73 71 72 syl ⊢ ( 𝜑 → 𝐻 = ( Base ‘ 𝐽 ) )
74 69 73 sseqtrrd ⊢ ( 𝜑 → 𝐹 ⊆ 𝐻 )
75 74 71 sstrd ⊢ ( 𝜑 → 𝐹 ⊆ ( Base ‘ 𝐿 ) )
76 75 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) → 𝐹 ⊆ ( Base ‘ 𝐿 ) )
77 12 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) → 𝐵 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
78 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) → 𝐹 ∈ ( SubDRing ‘ 𝐽 ) )
79 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) → ( 𝐹 ↑m 𝐵 ) ∈ V )
80 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) → 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) )
81 24 79 80 elmaprd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) → 𝑢 : 𝐻 ⟶ ( 𝐹 ↑m 𝐵 ) )
82 81 ffvelcdmda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) → ( 𝑢 ‘ ℎ ) ∈ ( 𝐹 ↑m 𝐵 ) )
83 77 78 82 elmaprd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) → ( 𝑢 ‘ ℎ ) : 𝐵 ⟶ 𝐹 )
84 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) → 𝑐 ∈ 𝐵 )
85 83 84 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) → ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ∈ 𝐹 )
86 76 85 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) → ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ∈ ( Base ‘ 𝐿 ) )
87 14 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) → 𝑃 : 𝐻 ⟶ 𝐺 )
88 15 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) → 𝑃 finSupp ( 0g ‘ 𝐿 ) )
89 21 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑦 ∈ ( Base ‘ 𝐿 ) ) → 𝐿 ∈ Ring )
90 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑦 ∈ ( Base ‘ 𝐿 ) ) → 𝑦 ∈ ( Base ‘ 𝐿 ) )
91 39 31 19 89 90 ringlzd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑦 ∈ ( Base ‘ 𝐿 ) ) → ( ( 0g ‘ 𝐿 ) ( .r ‘ 𝐿 ) 𝑦 ) = ( 0g ‘ 𝐿 ) )
92 65 65 24 66 86 87 88 91 fisuppov1 ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) → ( ℎ ∈ 𝐻 ↦ ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ) finSupp ( 0g ‘ 𝐿 ) )
93 64 92 eqbrtrid ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) → ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) finSupp ( 0g ‘ 𝐿 ) )
94 19 23 24 30 59 93 gsumsubmcl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) → ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ∈ 𝐺 )
95 94 fmpttd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) : 𝐵 ⟶ 𝐺 )
96 17 18 95 elmapdd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) ∈ ( 𝐺 ↑m 𝐵 ) )
97 breq1 ⊢ ( 𝑎 = ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) → ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ↔ ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) finSupp ( 0g ‘ 𝐿 ) ) )
98 97 adantl ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑎 = ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) ) → ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ↔ ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) finSupp ( 0g ‘ 𝐿 ) ) )
99 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑎 = ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑎 = ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) )
100 99 fveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑎 = ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ‘ 𝑏 ) = ( ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) ‘ 𝑏 ) )
101 eqid ⊢ ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) = ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) )
102 fveq2 ⊢ ( 𝑐 = 𝑏 → ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) = ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) )
103 102 oveq2d ⊢ ( 𝑐 = 𝑏 → ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) = ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ) )
104 103 mpteq2dv ⊢ ( 𝑐 = 𝑏 → ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) = ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ) ) )
105 104 oveq2d ⊢ ( 𝑐 = 𝑏 → ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ) ) ) )
106 simpr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 )
107 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ) ) ) ∈ V )
108 101 105 106 107 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) ‘ 𝑏 ) = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ) ) ) )
109 108 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑎 = ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) ) ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) ‘ 𝑏 ) = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ) ) ) )
110 100 109 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑎 = ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ‘ 𝑏 ) = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ) ) ) )
111 110 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑎 = ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) ) ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑎 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) = ( ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ) ) ) ( .r ‘ 𝐿 ) 𝑏 ) )
112 111 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑎 = ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) ) → ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) = ( 𝑏 ∈ 𝐵 ↦ ( ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ) ) ) ( .r ‘ 𝐿 ) 𝑏 ) ) )
113 112 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑎 = ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) ) → ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ) ) ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) )
114 113 eqeq2d ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑎 = ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) ) → ( 𝑋 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ↔ 𝑋 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ) ) ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) )
115 98 114 anbi12d ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ 𝑎 = ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) ) → ( ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑋 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ↔ ( ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑋 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ) ) ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) )
116 115 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑎 = ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) ) → ( ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑋 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ↔ ( ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑋 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ) ) ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) )
117 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → 𝐵 ∈ Fin )
118 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) → ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ∈ V )
119 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → ( 0g ‘ 𝐿 ) ∈ V )
120 101 117 118 119 fsuppmptdm ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) finSupp ( 0g ‘ 𝐿 ) )
121 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → 𝑋 = ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) )
122 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → 𝐿 ∈ Ring )
123 122 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) → 𝐿 ∈ Ring )
124 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) → 𝐵 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
125 41 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) → 𝐺 ⊆ ( Base ‘ 𝐿 ) )
126 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → 𝑃 : 𝐻 ⟶ 𝐺 )
127 126 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) → ( 𝑃 ‘ ℎ ) ∈ 𝐺 )
128 125 127 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) → ( 𝑃 ‘ ℎ ) ∈ ( Base ‘ 𝐿 ) )
129 123 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) ∧ 𝑐 ∈ 𝐵 ) → 𝐿 ∈ Ring )
130 75 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) ∧ 𝑐 ∈ 𝐵 ) → 𝐹 ⊆ ( Base ‘ 𝐿 ) )
131 12 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) ∧ 𝑐 ∈ 𝐵 ) → 𝐵 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
132 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) ∧ 𝑐 ∈ 𝐵 ) → 𝐹 ∈ ( SubDRing ‘ 𝐽 ) )
133 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) ∧ 𝑐 ∈ 𝐵 ) → 𝐻 ∈ ( SubDRing ‘ 𝐿 ) )
134 ovexd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) ∧ 𝑐 ∈ 𝐵 ) → ( 𝐹 ↑m 𝐵 ) ∈ V )
135 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) ∧ 𝑐 ∈ 𝐵 ) → 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) )
136 133 134 135 elmaprd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) ∧ 𝑐 ∈ 𝐵 ) → 𝑢 : 𝐻 ⟶ ( 𝐹 ↑m 𝐵 ) )
137 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) ∧ 𝑐 ∈ 𝐵 ) → ℎ ∈ 𝐻 )
138 136 137 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) ∧ 𝑐 ∈ 𝐵 ) → ( 𝑢 ‘ ℎ ) ∈ ( 𝐹 ↑m 𝐵 ) )
139 131 132 138 elmaprd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) ∧ 𝑐 ∈ 𝐵 ) → ( 𝑢 ‘ ℎ ) : 𝐵 ⟶ 𝐹 )
140 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) ∧ 𝑐 ∈ 𝐵 ) → 𝑐 ∈ 𝐵 )
141 139 140 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) ∧ 𝑐 ∈ 𝐵 ) → ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ∈ 𝐹 )
142 130 141 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) ∧ 𝑐 ∈ 𝐵 ) → ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ∈ ( Base ‘ 𝐿 ) )
143 eqid ⊢ ( Base ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) = ( Base ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) )
144 eqid ⊢ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) = ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) )
145 143 144 lbsss ⊢ ( 𝐵 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) → 𝐵 ⊆ ( Base ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
146 12 145 syl ⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
147 eqidd ⊢ ( 𝜑 → ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) = ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) )
148 147 69 srabase ⊢ ( 𝜑 → ( Base ‘ 𝐽 ) = ( Base ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
149 73 148 eqtr2d ⊢ ( 𝜑 → ( Base ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) = 𝐻 )
150 146 149 sseqtrd ⊢ ( 𝜑 → 𝐵 ⊆ 𝐻 )
151 150 71 sstrd ⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ 𝐿 ) )
152 151 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) → 𝐵 ⊆ ( Base ‘ 𝐿 ) )
153 152 sselda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) ∧ 𝑐 ∈ 𝐵 ) → 𝑐 ∈ ( Base ‘ 𝐿 ) )
154 39 31 129 142 153 ringcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) ∧ 𝑐 ∈ 𝐵 ) → ( ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ( .r ‘ 𝐿 ) 𝑐 ) ∈ ( Base ‘ 𝐿 ) )
155 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) → ( 0g ‘ 𝐿 ) ∈ V )
156 ssidd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) → 𝐵 ⊆ 𝐵 )
157 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) → 𝐹 ∈ ( SubDRing ‘ 𝐽 ) )
158 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → 𝐻 ∈ ( SubDRing ‘ 𝐿 ) )
159 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → ( 𝐹 ↑m 𝐵 ) ∈ V )
160 simplr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) )
161 158 159 160 elmaprd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → 𝑢 : 𝐻 ⟶ ( 𝐹 ↑m 𝐵 ) )
162 161 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) → ( 𝑢 ‘ ℎ ) ∈ ( 𝐹 ↑m 𝐵 ) )
163 124 157 162 elmaprd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) → ( 𝑢 ‘ ℎ ) : 𝐵 ⟶ 𝐹 )
164 61 breq1d ⊢ ( 𝑓 = ℎ → ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ↔ ( 𝑢 ‘ ℎ ) finSupp ( 0g ‘ 𝐿 ) ) )
165 id ⊢ ( 𝑓 = ℎ → 𝑓 = ℎ )
166 61 fveq1d ⊢ ( 𝑓 = ℎ → ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) = ( ( 𝑢 ‘ ℎ ) ‘ 𝑏 ) )
167 166 oveq1d ⊢ ( 𝑓 = ℎ → ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) = ( ( ( 𝑢 ‘ ℎ ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) )
168 167 mpteq2dv ⊢ ( 𝑓 = ℎ → ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) = ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ ℎ ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) )
169 168 oveq2d ⊢ ( 𝑓 = ℎ → ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ ℎ ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) )
170 165 169 eqeq12d ⊢ ( 𝑓 = ℎ → ( 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ↔ ℎ = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ ℎ ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) )
171 164 170 anbi12d ⊢ ( 𝑓 = ℎ → ( ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ↔ ( ( 𝑢 ‘ ℎ ) finSupp ( 0g ‘ 𝐿 ) ∧ ℎ = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ ℎ ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) )
172 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) → ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) )
173 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) → ℎ ∈ 𝐻 )
174 171 172 173 rspcdva ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) → ( ( 𝑢 ‘ ℎ ) finSupp ( 0g ‘ 𝐿 ) ∧ ℎ = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ ℎ ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) )
175 174 simpld ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) → ( 𝑢 ‘ ℎ ) finSupp ( 0g ‘ 𝐿 ) )
176 123 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐿 ) ) → 𝐿 ∈ Ring )
177 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐿 ) ) → 𝑦 ∈ ( Base ‘ 𝐿 ) )
178 39 31 19 176 177 ringlzd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐿 ) ) → ( ( 0g ‘ 𝐿 ) ( .r ‘ 𝐿 ) 𝑦 ) = ( 0g ‘ 𝐿 ) )
179 155 155 124 156 153 163 175 178 fisuppov1 ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) → ( 𝑐 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ( .r ‘ 𝐿 ) 𝑐 ) ) finSupp ( 0g ‘ 𝐿 ) )
180 39 19 31 123 124 128 154 179 gsummulc2 ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) → ( 𝐿 Σg ( 𝑐 ∈ 𝐵 ↦ ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ( .r ‘ 𝐿 ) 𝑐 ) ) ) ) = ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( 𝐿 Σg ( 𝑐 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ( .r ‘ 𝐿 ) 𝑐 ) ) ) ) )
181 128 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) ∧ 𝑐 ∈ 𝐵 ) → ( 𝑃 ‘ ℎ ) ∈ ( Base ‘ 𝐿 ) )
182 39 31 129 181 142 153 ringassd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) ∧ 𝑐 ∈ 𝐵 ) → ( ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ( .r ‘ 𝐿 ) 𝑐 ) = ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ( .r ‘ 𝐿 ) 𝑐 ) ) )
183 182 mpteq2dva ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) → ( 𝑐 ∈ 𝐵 ↦ ( ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ( .r ‘ 𝐿 ) 𝑐 ) ) = ( 𝑐 ∈ 𝐵 ↦ ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ( .r ‘ 𝐿 ) 𝑐 ) ) ) )
184 183 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) → ( 𝐿 Σg ( 𝑐 ∈ 𝐵 ↦ ( ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ( .r ‘ 𝐿 ) 𝑐 ) ) ) = ( 𝐿 Σg ( 𝑐 ∈ 𝐵 ↦ ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ( .r ‘ 𝐿 ) 𝑐 ) ) ) ) )
185 174 simprd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) → ℎ = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ ℎ ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) )
186 fveq2 ⊢ ( 𝑏 = 𝑐 → ( ( 𝑢 ‘ ℎ ) ‘ 𝑏 ) = ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) )
187 id ⊢ ( 𝑏 = 𝑐 → 𝑏 = 𝑐 )
188 186 187 oveq12d ⊢ ( 𝑏 = 𝑐 → ( ( ( 𝑢 ‘ ℎ ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) = ( ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ( .r ‘ 𝐿 ) 𝑐 ) )
189 188 cbvmptv ⊢ ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ ℎ ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) = ( 𝑐 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ( .r ‘ 𝐿 ) 𝑐 ) )
190 189 oveq2i ⊢ ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ ℎ ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) = ( 𝐿 Σg ( 𝑐 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ( .r ‘ 𝐿 ) 𝑐 ) ) )
191 185 190 eqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) → ℎ = ( 𝐿 Σg ( 𝑐 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ( .r ‘ 𝐿 ) 𝑐 ) ) ) )
192 191 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) → ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ℎ ) = ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( 𝐿 Σg ( 𝑐 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ( .r ‘ 𝐿 ) 𝑐 ) ) ) ) )
193 180 184 192 3eqtr4rd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ℎ ∈ 𝐻 ) → ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ℎ ) = ( 𝐿 Σg ( 𝑐 ∈ 𝐵 ↦ ( ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ( .r ‘ 𝐿 ) 𝑐 ) ) ) )
194 193 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → ( ℎ ∈ 𝐻 ↦ ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ℎ ) ) = ( ℎ ∈ 𝐻 ↦ ( 𝐿 Σg ( 𝑐 ∈ 𝐵 ↦ ( ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ( .r ‘ 𝐿 ) 𝑐 ) ) ) ) )
195 194 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → ( 𝐿 Σg ( ℎ ∈ 𝐻 ↦ ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ℎ ) ) ) = ( 𝐿 Σg ( ℎ ∈ 𝐻 ↦ ( 𝐿 Σg ( 𝑐 ∈ 𝐵 ↦ ( ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ( .r ‘ 𝐿 ) 𝑐 ) ) ) ) ) )
196 60 165 oveq12d ⊢ ( 𝑓 = ℎ → ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) = ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ℎ ) )
197 196 cbvmptv ⊢ ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) = ( ℎ ∈ 𝐻 ↦ ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ℎ ) )
198 197 oveq2i ⊢ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) = ( 𝐿 Σg ( ℎ ∈ 𝐻 ↦ ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ℎ ) ) )
199 198 a1i ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) = ( 𝐿 Σg ( ℎ ∈ 𝐻 ↦ ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ℎ ) ) ) )
200 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → 𝐿 ∈ CMnd )
201 21 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) → 𝐿 ∈ Ring )
202 41 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) → 𝐺 ⊆ ( Base ‘ 𝐿 ) )
203 87 ffvelcdmda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) → ( 𝑃 ‘ ℎ ) ∈ 𝐺 )
204 202 203 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) → ( 𝑃 ‘ ℎ ) ∈ ( Base ‘ 𝐿 ) )
205 39 31 201 204 86 ringcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) → ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ∈ ( Base ‘ 𝐿 ) )
206 151 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → 𝐵 ⊆ ( Base ‘ 𝐿 ) )
207 206 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) → 𝑐 ∈ ( Base ‘ 𝐿 ) )
208 207 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) → 𝑐 ∈ ( Base ‘ 𝐿 ) )
209 39 31 201 205 208 ringcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) → ( ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ( .r ‘ 𝐿 ) 𝑐 ) ∈ ( Base ‘ 𝐿 ) )
210 209 anasss ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ( 𝑐 ∈ 𝐵 ∧ ℎ ∈ 𝐻 ) ) → ( ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ( .r ‘ 𝐿 ) 𝑐 ) ∈ ( Base ‘ 𝐿 ) )
211 15 fsuppimpd ⊢ ( 𝜑 → ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ∈ Fin )
212 211 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ∈ Fin )
213 suppssdm ⊢ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ⊆ dom 𝑃
214 213 14 fssdm ⊢ ( 𝜑 → ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ⊆ 𝐻 )
215 214 sseld ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) → 𝑓 ∈ 𝐻 ) )
216 215 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) → ( 𝑓 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) → 𝑓 ∈ 𝐻 ) )
217 simpr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ) → ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) )
218 217 fsuppimpd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ) → ( ( 𝑢 ‘ 𝑓 ) supp ( 0g ‘ 𝐿 ) ) ∈ Fin )
219 218 ex ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) → ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) → ( ( 𝑢 ‘ 𝑓 ) supp ( 0g ‘ 𝐿 ) ) ∈ Fin ) )
220 219 adantrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) → ( ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) → ( ( 𝑢 ‘ 𝑓 ) supp ( 0g ‘ 𝐿 ) ) ∈ Fin ) )
221 216 220 imim12d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) → ( ( 𝑓 ∈ 𝐻 → ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → ( 𝑓 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) → ( ( 𝑢 ‘ 𝑓 ) supp ( 0g ‘ 𝐿 ) ) ∈ Fin ) ) )
222 221 ralimdv2 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) → ( ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) → ∀ 𝑓 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( 𝑢 ‘ 𝑓 ) supp ( 0g ‘ 𝐿 ) ) ∈ Fin ) )
223 222 imp ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → ∀ 𝑓 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( 𝑢 ‘ 𝑓 ) supp ( 0g ‘ 𝐿 ) ) ∈ Fin )
224 fveq2 ⊢ ( 𝑓 = 𝑖 → ( 𝑢 ‘ 𝑓 ) = ( 𝑢 ‘ 𝑖 ) )
225 224 oveq1d ⊢ ( 𝑓 = 𝑖 → ( ( 𝑢 ‘ 𝑓 ) supp ( 0g ‘ 𝐿 ) ) = ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) )
226 225 eleq1d ⊢ ( 𝑓 = 𝑖 → ( ( ( 𝑢 ‘ 𝑓 ) supp ( 0g ‘ 𝐿 ) ) ∈ Fin ↔ ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) ∈ Fin ) )
227 226 cbvralvw ⊢ ( ∀ 𝑓 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( 𝑢 ‘ 𝑓 ) supp ( 0g ‘ 𝐿 ) ) ∈ Fin ↔ ∀ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) ∈ Fin )
228 223 227 sylib ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → ∀ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) ∈ Fin )
229 iunfi ⊢ ( ( ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ∈ Fin ∧ ∀ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) ∈ Fin ) → ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) ∈ Fin )
230 212 228 229 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) ∈ Fin )
231 xpfi ⊢ ( ( ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) ∈ Fin ∧ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ∈ Fin ) → ( ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) ∈ Fin )
232 230 212 231 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → ( ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) ∈ Fin )
233 snssi ⊢ ( 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) → { 𝑖 } ⊆ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) )
234 233 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) → { 𝑖 } ⊆ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) )
235 234 iunxpssiun1 ⊢ ( 𝜑 → ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ⊆ ( ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) )
236 235 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ⊆ ( ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) )
237 232 236 ssfid ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ∈ Fin )
238 14 ffnd ⊢ ( 𝜑 → 𝑃 Fn 𝐻 )
239 238 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) → 𝑃 Fn 𝐻 )
240 8 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) → 𝐻 ∈ ( SubDRing ‘ 𝐿 ) )
241 fvexd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) → ( 0g ‘ 𝐿 ) ∈ V )
242 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) → ℎ ∈ 𝐻 )
243 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) → ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) )
244 242 243 eldifd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) → ℎ ∈ ( 𝐻 ∖ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) )
245 239 240 241 244 fvdifsupp ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) → ( 𝑃 ‘ ℎ ) = ( 0g ‘ 𝐿 ) )
246 245 oveq1d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) → ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) = ( ( 0g ‘ 𝐿 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) )
247 21 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) → 𝐿 ∈ Ring )
248 75 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) → 𝐹 ⊆ ( Base ‘ 𝐿 ) )
249 12 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) → 𝐵 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
250 6 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) → 𝐹 ∈ ( SubDRing ‘ 𝐽 ) )
251 ovexd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) → ( 𝐹 ↑m 𝐵 ) ∈ V )
252 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) → 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) )
253 240 251 252 elmaprd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) → 𝑢 : 𝐻 ⟶ ( 𝐹 ↑m 𝐵 ) )
254 253 242 ffvelcdmd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) → ( 𝑢 ‘ ℎ ) ∈ ( 𝐹 ↑m 𝐵 ) )
255 249 250 254 elmaprd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) → ( 𝑢 ‘ ℎ ) : 𝐵 ⟶ 𝐹 )
256 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) → 𝑐 ∈ 𝐵 )
257 255 256 ffvelcdmd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) → ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ∈ 𝐹 )
258 248 257 sseldd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) → ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ∈ ( Base ‘ 𝐿 ) )
259 39 31 19 247 258 ringlzd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) → ( ( 0g ‘ 𝐿 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) = ( 0g ‘ 𝐿 ) )
260 246 259 eqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ) → ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) = ( 0g ‘ 𝐿 ) )
261 12 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) → 𝐵 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
262 6 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) → 𝐹 ∈ ( SubDRing ‘ 𝐽 ) )
263 8 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) → 𝐻 ∈ ( SubDRing ‘ 𝐿 ) )
264 ovexd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) → ( 𝐹 ↑m 𝐵 ) ∈ V )
265 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) → 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) )
266 263 264 265 elmaprd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) → 𝑢 : 𝐻 ⟶ ( 𝐹 ↑m 𝐵 ) )
267 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) → ℎ ∈ 𝐻 )
268 266 267 ffvelcdmd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) → ( 𝑢 ‘ ℎ ) ∈ ( 𝐹 ↑m 𝐵 ) )
269 261 262 268 elmaprd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) → ( 𝑢 ‘ ℎ ) : 𝐵 ⟶ 𝐹 )
270 269 ffnd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) → ( 𝑢 ‘ ℎ ) Fn 𝐵 )
271 fvexd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) → ( 0g ‘ 𝐿 ) ∈ V )
272 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) → 𝑐 ∈ 𝐵 )
273 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) → ¬ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) )
274 272 273 eldifd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) → 𝑐 ∈ ( 𝐵 ∖ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) )
275 270 261 271 274 fvdifsupp ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) → ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) = ( 0g ‘ 𝐿 ) )
276 275 oveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) → ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) = ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( 0g ‘ 𝐿 ) ) )
277 201 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) → 𝐿 ∈ Ring )
278 204 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) → ( 𝑃 ‘ ℎ ) ∈ ( Base ‘ 𝐿 ) )
279 39 31 19 277 278 ringrzd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) → ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( 0g ‘ 𝐿 ) ) = ( 0g ‘ 𝐿 ) )
280 276 279 eqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ¬ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) → ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) = ( 0g ‘ 𝐿 ) )
281 df-br ⊢ ( 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ↔ ⟨ 𝑐 , ℎ ⟩ ∈ ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) )
282 fveq2 ⊢ ( ℎ = 𝑖 → ( 𝑢 ‘ ℎ ) = ( 𝑢 ‘ 𝑖 ) )
283 282 oveq1d ⊢ ( ℎ = 𝑖 → ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) = ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) )
284 sneq ⊢ ( ℎ = 𝑖 → { ℎ } = { 𝑖 } )
285 283 284 xpeq12d ⊢ ( ℎ = 𝑖 → ( ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) × { ℎ } ) = ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) )
286 285 cbviunv ⊢ ∪ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) × { ℎ } ) = ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } )
287 286 eleq2i ⊢ ( ⟨ 𝑐 , ℎ ⟩ ∈ ∪ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) × { ℎ } ) ↔ ⟨ 𝑐 , ℎ ⟩ ∈ ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) )
288 opeliun2xp ⊢ ( ⟨ 𝑐 , ℎ ⟩ ∈ ∪ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) × { ℎ } ) ↔ ( ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ∧ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) )
289 281 287 288 3bitr2i ⊢ ( 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ↔ ( ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ∧ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) )
290 289 notbii ⊢ ( ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ↔ ¬ ( ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ∧ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) )
291 ianor ⊢ ( ¬ ( ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ∧ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) ↔ ( ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ∨ ¬ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) )
292 290 291 sylbb ⊢ ( ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ → ( ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ∨ ¬ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) )
293 292 adantl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) → ( ¬ ℎ ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ∨ ¬ 𝑐 ∈ ( ( 𝑢 ‘ ℎ ) supp ( 0g ‘ 𝐿 ) ) ) )
294 260 280 293 mpjaodan ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) → ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) = ( 0g ‘ 𝐿 ) )
295 294 oveq1d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) → ( ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ( .r ‘ 𝐿 ) 𝑐 ) = ( ( 0g ‘ 𝐿 ) ( .r ‘ 𝐿 ) 𝑐 ) )
296 122 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) → 𝐿 ∈ Ring )
297 207 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) → 𝑐 ∈ ( Base ‘ 𝐿 ) )
298 39 31 19 296 297 ringlzd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) → ( ( 0g ‘ 𝐿 ) ( .r ‘ 𝐿 ) 𝑐 ) = ( 0g ‘ 𝐿 ) )
299 295 298 eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) → ( ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ( .r ‘ 𝐿 ) 𝑐 ) = ( 0g ‘ 𝐿 ) )
300 299 an42ds ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ℎ ∈ 𝐻 ) ∧ 𝑐 ∈ 𝐵 ) → ( ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ( .r ‘ 𝐿 ) 𝑐 ) = ( 0g ‘ 𝐿 ) )
301 300 an32s ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ 𝑐 ∈ 𝐵 ) ∧ ℎ ∈ 𝐻 ) → ( ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ( .r ‘ 𝐿 ) 𝑐 ) = ( 0g ‘ 𝐿 ) )
302 301 anasss ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ∧ ( 𝑐 ∈ 𝐵 ∧ ℎ ∈ 𝐻 ) ) → ( ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ( .r ‘ 𝐿 ) 𝑐 ) = ( 0g ‘ 𝐿 ) )
303 302 an32s ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ( 𝑐 ∈ 𝐵 ∧ ℎ ∈ 𝐻 ) ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) → ( ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ( .r ‘ 𝐿 ) 𝑐 ) = ( 0g ‘ 𝐿 ) )
304 303 anasss ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ ( ( 𝑐 ∈ 𝐵 ∧ ℎ ∈ 𝐻 ) ∧ ¬ 𝑐 ∪ 𝑖 ∈ ( 𝑃 supp ( 0g ‘ 𝐿 ) ) ( ( ( 𝑢 ‘ 𝑖 ) supp ( 0g ‘ 𝐿 ) ) × { 𝑖 } ) ℎ ) ) → ( ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ( .r ‘ 𝐿 ) 𝑐 ) = ( 0g ‘ 𝐿 ) )
305 39 19 200 18 158 210 237 304 gsumcom3 ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → ( 𝐿 Σg ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( ℎ ∈ 𝐻 ↦ ( ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ( .r ‘ 𝐿 ) 𝑐 ) ) ) ) ) = ( 𝐿 Σg ( ℎ ∈ 𝐻 ↦ ( 𝐿 Σg ( 𝑐 ∈ 𝐵 ↦ ( ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ( .r ‘ 𝐿 ) 𝑐 ) ) ) ) ) )
306 195 199 305 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) 𝑓 ) ) ) = ( 𝐿 Σg ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( ℎ ∈ 𝐻 ↦ ( ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ( .r ‘ 𝐿 ) 𝑐 ) ) ) ) ) )
307 122 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) → 𝐿 ∈ Ring )
308 39 19 31 307 24 207 205 92 gsummulc1 ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) ∧ 𝑐 ∈ 𝐵 ) → ( 𝐿 Σg ( ℎ ∈ 𝐻 ↦ ( ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ( .r ‘ 𝐿 ) 𝑐 ) ) ) = ( ( 𝐿 Σg ( ℎ ∈ 𝐻 ↦ ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ) ) ( .r ‘ 𝐿 ) 𝑐 ) )
309 308 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( ℎ ∈ 𝐻 ↦ ( ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ( .r ‘ 𝐿 ) 𝑐 ) ) ) ) = ( 𝑐 ∈ 𝐵 ↦ ( ( 𝐿 Σg ( ℎ ∈ 𝐻 ↦ ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ) ) ( .r ‘ 𝐿 ) 𝑐 ) ) )
310 309 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → ( 𝐿 Σg ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( ℎ ∈ 𝐻 ↦ ( ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ( .r ‘ 𝐿 ) 𝑐 ) ) ) ) ) = ( 𝐿 Σg ( 𝑐 ∈ 𝐵 ↦ ( ( 𝐿 Σg ( ℎ ∈ 𝐻 ↦ ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ) ) ( .r ‘ 𝐿 ) 𝑐 ) ) ) )
311 121 306 310 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → 𝑋 = ( 𝐿 Σg ( 𝑐 ∈ 𝐵 ↦ ( ( 𝐿 Σg ( ℎ ∈ 𝐻 ↦ ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ) ) ( .r ‘ 𝐿 ) 𝑐 ) ) ) )
312 60 166 oveq12d ⊢ ( 𝑓 = ℎ → ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ) = ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑏 ) ) )
313 312 cbvmptv ⊢ ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ) ) = ( ℎ ∈ 𝐻 ↦ ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑏 ) ) )
314 186 oveq2d ⊢ ( 𝑏 = 𝑐 → ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑏 ) ) = ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) )
315 314 mpteq2dv ⊢ ( 𝑏 = 𝑐 → ( ℎ ∈ 𝐻 ↦ ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑏 ) ) ) = ( ℎ ∈ 𝐻 ↦ ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ) )
316 313 315 eqtrid ⊢ ( 𝑏 = 𝑐 → ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ) ) = ( ℎ ∈ 𝐻 ↦ ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ) )
317 316 oveq2d ⊢ ( 𝑏 = 𝑐 → ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ) ) ) = ( 𝐿 Σg ( ℎ ∈ 𝐻 ↦ ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ) ) )
318 317 187 oveq12d ⊢ ( 𝑏 = 𝑐 → ( ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ) ) ) ( .r ‘ 𝐿 ) 𝑏 ) = ( ( 𝐿 Σg ( ℎ ∈ 𝐻 ↦ ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ) ) ( .r ‘ 𝐿 ) 𝑐 ) )
319 318 cbvmptv ⊢ ( 𝑏 ∈ 𝐵 ↦ ( ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ) ) ) ( .r ‘ 𝐿 ) 𝑏 ) ) = ( 𝑐 ∈ 𝐵 ↦ ( ( 𝐿 Σg ( ℎ ∈ 𝐻 ↦ ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ) ) ( .r ‘ 𝐿 ) 𝑐 ) )
320 319 oveq2i ⊢ ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ) ) ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) = ( 𝐿 Σg ( 𝑐 ∈ 𝐵 ↦ ( ( 𝐿 Σg ( ℎ ∈ 𝐻 ↦ ( ( 𝑃 ‘ ℎ ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ ℎ ) ‘ 𝑐 ) ) ) ) ( .r ‘ 𝐿 ) 𝑐 ) ) )
321 311 320 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → 𝑋 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ) ) ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) )
322 120 321 jca ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → ( ( 𝑐 ∈ 𝐵 ↦ ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑐 ) ) ) ) ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑋 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝐿 Σg ( 𝑓 ∈ 𝐻 ↦ ( ( 𝑃 ‘ 𝑓 ) ( .r ‘ 𝐿 ) ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ) ) ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) )
323 96 116 322 rspcedvd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ) ∧ ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) → ∃ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑋 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) )
324 breq1 ⊢ ( 𝑒 = ( 𝑢 ‘ 𝑓 ) → ( 𝑒 finSupp ( 0g ‘ 𝐿 ) ↔ ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ) )
325 fveq1 ⊢ ( 𝑒 = ( 𝑢 ‘ 𝑓 ) → ( 𝑒 ‘ 𝑏 ) = ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) )
326 325 oveq1d ⊢ ( 𝑒 = ( 𝑢 ‘ 𝑓 ) → ( ( 𝑒 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) = ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) )
327 326 mpteq2dv ⊢ ( 𝑒 = ( 𝑢 ‘ 𝑓 ) → ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) = ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) )
328 327 oveq2d ⊢ ( 𝑒 = ( 𝑢 ‘ 𝑓 ) → ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) )
329 328 eqeq2d ⊢ ( 𝑒 = ( 𝑢 ‘ 𝑓 ) → ( 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ↔ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) )
330 324 329 anbi12d ⊢ ( 𝑒 = ( 𝑢 ‘ 𝑓 ) → ( ( 𝑒 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ↔ ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) )
331 ovexd ⊢ ( 𝜑 → ( 𝐹 ↑m 𝐵 ) ∈ V )
332 eqid ⊢ ( LSpan ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) = ( LSpan ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) )
333 143 144 332 lbssp ⊢ ( 𝐵 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) → ( ( LSpan ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ‘ 𝐵 ) = ( Base ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
334 12 333 syl ⊢ ( 𝜑 → ( ( LSpan ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ‘ 𝐵 ) = ( Base ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
335 148 73 334 3eqtr4rd ⊢ ( 𝜑 → ( ( LSpan ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ‘ 𝐵 ) = 𝐻 )
336 335 eleq2d ⊢ ( 𝜑 → ( 𝑓 ∈ ( ( LSpan ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ‘ 𝐵 ) ↔ 𝑓 ∈ 𝐻 ) )
337 eqid ⊢ ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) = ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
338 eqid ⊢ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) = ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) )
339 eqid ⊢ ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) = ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
340 eqid ⊢ ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) = ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) )
341 sdrgsubrg ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐽 ) → 𝐹 ∈ ( SubRing ‘ 𝐽 ) )
342 6 341 syl ⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐽 ) )
343 eqid ⊢ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) = ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 )
344 343 sralmod ⊢ ( 𝐹 ∈ ( SubRing ‘ 𝐽 ) → ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ∈ LMod )
345 342 344 syl ⊢ ( 𝜑 → ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ∈ LMod )
346 332 143 337 338 339 340 345 146 ellspds ⊢ ( 𝜑 → ( 𝑓 ∈ ( ( LSpan ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ‘ 𝐵 ) ↔ ∃ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ( 𝑒 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑓 = ( ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) 𝑏 ) ) ) ) ) )
347 336 346 bitr3d ⊢ ( 𝜑 → ( 𝑓 ∈ 𝐻 ↔ ∃ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ( 𝑒 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑓 = ( ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) 𝑏 ) ) ) ) ) )
348 347 biimpa ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐻 ) → ∃ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ( 𝑒 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑓 = ( ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) 𝑏 ) ) ) ) )
349 eqid ⊢ ( 𝐽 ↾s 𝐹 ) = ( 𝐽 ↾s 𝐹 )
350 349 67 ressbas2 ⊢ ( 𝐹 ⊆ ( Base ‘ 𝐽 ) → 𝐹 = ( Base ‘ ( 𝐽 ↾s 𝐹 ) ) )
351 69 350 syl ⊢ ( 𝜑 → 𝐹 = ( Base ‘ ( 𝐽 ↾s 𝐹 ) ) )
352 147 69 srasca ⊢ ( 𝜑 → ( 𝐽 ↾s 𝐹 ) = ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
353 352 fveq2d ⊢ ( 𝜑 → ( Base ‘ ( 𝐽 ↾s 𝐹 ) ) = ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) )
354 351 353 eqtr2d ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) = 𝐹 )
355 354 oveq1d ⊢ ( 𝜑 → ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) = ( 𝐹 ↑m 𝐵 ) )
356 sdrgsubrg ⊢ ( 𝐻 ∈ ( SubDRing ‘ 𝐿 ) → 𝐻 ∈ ( SubRing ‘ 𝐿 ) )
357 8 356 syl ⊢ ( 𝜑 → 𝐻 ∈ ( SubRing ‘ 𝐿 ) )
358 subrgsubg ⊢ ( 𝐻 ∈ ( SubRing ‘ 𝐿 ) → 𝐻 ∈ ( SubGrp ‘ 𝐿 ) )
359 3 19 subg0 ⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐿 ) → ( 0g ‘ 𝐿 ) = ( 0g ‘ 𝐽 ) )
360 357 358 359 3syl ⊢ ( 𝜑 → ( 0g ‘ 𝐿 ) = ( 0g ‘ 𝐽 ) )
361 3 sdrgdrng ⊢ ( 𝐻 ∈ ( SubDRing ‘ 𝐿 ) → 𝐽 ∈ DivRing )
362 8 361 syl ⊢ ( 𝜑 → 𝐽 ∈ DivRing )
363 362 drngringd ⊢ ( 𝜑 → 𝐽 ∈ Ring )
364 363 ringcmnd ⊢ ( 𝜑 → 𝐽 ∈ CMnd )
365 364 cmnmndd ⊢ ( 𝜑 → 𝐽 ∈ Mnd )
366 subrgsubg ⊢ ( 𝐹 ∈ ( SubRing ‘ 𝐽 ) → 𝐹 ∈ ( SubGrp ‘ 𝐽 ) )
367 eqid ⊢ ( 0g ‘ 𝐽 ) = ( 0g ‘ 𝐽 )
368 367 subg0cl ⊢ ( 𝐹 ∈ ( SubGrp ‘ 𝐽 ) → ( 0g ‘ 𝐽 ) ∈ 𝐹 )
369 342 366 368 3syl ⊢ ( 𝜑 → ( 0g ‘ 𝐽 ) ∈ 𝐹 )
370 349 67 367 ress0g ⊢ ( ( 𝐽 ∈ Mnd ∧ ( 0g ‘ 𝐽 ) ∈ 𝐹 ∧ 𝐹 ⊆ ( Base ‘ 𝐽 ) ) → ( 0g ‘ 𝐽 ) = ( 0g ‘ ( 𝐽 ↾s 𝐹 ) ) )
371 365 369 69 370 syl3anc ⊢ ( 𝜑 → ( 0g ‘ 𝐽 ) = ( 0g ‘ ( 𝐽 ↾s 𝐹 ) ) )
372 352 fveq2d ⊢ ( 𝜑 → ( 0g ‘ ( 𝐽 ↾s 𝐹 ) ) = ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) )
373 360 371 372 3eqtrrd ⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) = ( 0g ‘ 𝐿 ) )
374 373 breq2d ⊢ ( 𝜑 → ( 𝑒 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↔ 𝑒 finSupp ( 0g ‘ 𝐿 ) ) )
375 374 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) → ( 𝑒 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↔ 𝑒 finSupp ( 0g ‘ 𝐿 ) ) )
376 12 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) → 𝐵 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
377 subgsubm ⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐿 ) → 𝐻 ∈ ( SubMnd ‘ 𝐿 ) )
378 357 358 377 3syl ⊢ ( 𝜑 → 𝐻 ∈ ( SubMnd ‘ 𝐿 ) )
379 378 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) → 𝐻 ∈ ( SubMnd ‘ 𝐿 ) )
380 3 31 ressmulr ⊢ ( 𝐻 ∈ ( SubDRing ‘ 𝐿 ) → ( .r ‘ 𝐿 ) = ( .r ‘ 𝐽 ) )
381 8 380 syl ⊢ ( 𝜑 → ( .r ‘ 𝐿 ) = ( .r ‘ 𝐽 ) )
382 147 69 sravsca ⊢ ( 𝜑 → ( .r ‘ 𝐽 ) = ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
383 381 382 eqtrd ⊢ ( 𝜑 → ( .r ‘ 𝐿 ) = ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
384 383 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( .r ‘ 𝐿 ) = ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) )
385 384 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑒 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) = ( ( 𝑒 ‘ 𝑏 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) 𝑏 ) )
386 357 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝐻 ∈ ( SubRing ‘ 𝐿 ) )
387 74 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝐹 ⊆ 𝐻 )
388 5 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) → 𝐹 ∈ ( SubDRing ‘ 𝐼 ) )
389 355 eleq2d ⊢ ( 𝜑 → ( 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ↔ 𝑒 ∈ ( 𝐹 ↑m 𝐵 ) ) )
390 389 biimpa ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) → 𝑒 ∈ ( 𝐹 ↑m 𝐵 ) )
391 376 388 390 elmaprd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) → 𝑒 : 𝐵 ⟶ 𝐹 )
392 391 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑒 ‘ 𝑏 ) ∈ 𝐹 )
393 387 392 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑒 ‘ 𝑏 ) ∈ 𝐻 )
394 150 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) → 𝐵 ⊆ 𝐻 )
395 394 sselda ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐻 )
396 31 386 393 395 subrgmcld ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑒 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ∈ 𝐻 )
397 385 396 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑒 ‘ 𝑏 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) 𝑏 ) ∈ 𝐻 )
398 397 fmpttd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) → ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) 𝑏 ) ) : 𝐵 ⟶ 𝐻 )
399 376 379 398 3 gsumsubm ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) → ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) 𝑏 ) ) ) = ( 𝐽 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) 𝑏 ) ) ) )
400 381 382 eqtr2d ⊢ ( 𝜑 → ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) = ( .r ‘ 𝐿 ) )
401 400 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) → ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) = ( .r ‘ 𝐿 ) )
402 401 oveqd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) → ( ( 𝑒 ‘ 𝑏 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) 𝑏 ) = ( ( 𝑒 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) )
403 402 mpteq2dv ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) → ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) 𝑏 ) ) = ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) )
404 403 oveq2d ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) → ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) 𝑏 ) ) ) = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) )
405 12 mptexd ⊢ ( 𝜑 → ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) 𝑏 ) ) ∈ V )
406 fvexd ⊢ ( 𝜑 → ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ∈ V )
407 343 405 362 406 69 gsumsra ⊢ ( 𝜑 → ( 𝐽 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) 𝑏 ) ) ) = ( ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) 𝑏 ) ) ) )
408 407 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) → ( 𝐽 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) 𝑏 ) ) ) = ( ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) 𝑏 ) ) ) )
409 399 404 408 3eqtr3rd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) → ( ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) 𝑏 ) ) ) = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) )
410 409 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) → ( 𝑓 = ( ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) 𝑏 ) ) ) ↔ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) )
411 375 410 anbi12d ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ) → ( ( 𝑒 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑓 = ( ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) 𝑏 ) ) ) ) ↔ ( 𝑒 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) )
412 355 411 rexeqbidva ⊢ ( 𝜑 → ( ∃ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ( 𝑒 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑓 = ( ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) 𝑏 ) ) ) ) ↔ ∃ 𝑒 ∈ ( 𝐹 ↑m 𝐵 ) ( 𝑒 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) )
413 412 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐻 ) → ( ∃ 𝑒 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ↑m 𝐵 ) ( 𝑒 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑓 = ( ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐽 ) ‘ 𝐹 ) ) 𝑏 ) ) ) ) ↔ ∃ 𝑒 ∈ ( 𝐹 ↑m 𝐵 ) ( 𝑒 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) ) )
414 348 413 mpbid ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐻 ) → ∃ 𝑒 ∈ ( 𝐹 ↑m 𝐵 ) ( 𝑒 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑒 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) )
415 330 8 331 414 ac6mapd ⊢ ( 𝜑 → ∃ 𝑢 ∈ ( ( 𝐹 ↑m 𝐵 ) ↑m 𝐻 ) ∀ 𝑓 ∈ 𝐻 ( ( 𝑢 ‘ 𝑓 ) finSupp ( 0g ‘ 𝐿 ) ∧ 𝑓 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( ( 𝑢 ‘ 𝑓 ) ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) )
416 323 415 r19.29a ⊢ ( 𝜑 → ∃ 𝑎 ∈ ( 𝐺 ↑m 𝐵 ) ( 𝑎 finSupp ( 0g ‘ 𝐿 ) ∧ 𝑋 = ( 𝐿 Σg ( 𝑏 ∈ 𝐵 ↦ ( ( 𝑎 ‘ 𝑏 ) ( .r ‘ 𝐿 ) 𝑏 ) ) ) ) )