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