fedgmul - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > fedgmul		Structured version Visualization version GIF version

Theorem fedgmul 31027

Description: The multiplicativity formula for degrees of field extensions. Given 𝐸 a field extension of 𝐹, itself a field extension of 𝐾, we have [𝐸:𝐾] = [𝐸:𝐹][𝐹:𝐾]. Proposition 1.2 of [Lang], p. 224. Here (dim‘𝐴) is the degree of the extension 𝐸 of 𝐾, (dim‘𝐵) is the degree of the extension 𝐸 of 𝐹, and (dim‘𝐶) is the degree of the extension 𝐹 of 𝐾. This proof is valid for infinite dimensions, and is actually valid for division ring extensions, not just field extensions. (Contributed by Thierry Arnoux, 25-Jul-2023.)

**Hypotheses**
Ref	Expression
fedgmul.a	⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑉)
fedgmul.b	⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
fedgmul.c	⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
fedgmul.f	⊢ 𝐹 = (𝐸 ↾_s 𝑈)
fedgmul.k	⊢ 𝐾 = (𝐸 ↾_s 𝑉)
fedgmul.1	⊢ (𝜑 → 𝐸 ∈ DivRing)
fedgmul.2	⊢ (𝜑 → 𝐹 ∈ DivRing)
fedgmul.3	⊢ (𝜑 → 𝐾 ∈ DivRing)
fedgmul.4	⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸))
fedgmul.5	⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐹))

**Assertion**
Ref	Expression
fedgmul	⊢ (𝜑 → (dim‘𝐴) = ((dim‘𝐵) ·_e (dim‘𝐶)))

Proof of Theorem fedgmul Dummy variables 𝑎 𝑐 𝑓 𝑢 𝑥 𝑦 𝑧 𝑖 𝑗 𝑤 𝑏 𝑣 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fedgmul.2	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ DivRing)
2		fedgmul.4	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸))
3		fedgmul.5	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐹))
4		fedgmul.f	. . . . . . . . . . . 12 ⊢ 𝐹 = (𝐸 ↾_s 𝑈)
5	4	subsubrg 19561	. . . . . . . . . . 11 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (𝑉 ∈ (SubRing‘𝐹) ↔ (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈)))
6	5	biimpa 479	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ∈ (SubRing‘𝐹)) → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))
7	2, 3, 6	syl2anc 586	. . . . . . . . 9 ⊢ (𝜑 → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))
8	7	simprd 498	. . . . . . . 8 ⊢ (𝜑 → 𝑉 ⊆ 𝑈)
9		ressabs 16563	. . . . . . . 8 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈) → ((𝐸 ↾_s 𝑈) ↾_s 𝑉) = (𝐸 ↾_s 𝑉))
10	2, 8, 9	syl2anc 586	. . . . . . 7 ⊢ (𝜑 → ((𝐸 ↾_s 𝑈) ↾_s 𝑉) = (𝐸 ↾_s 𝑉))
11	4	oveq1i 7166	. . . . . . 7 ⊢ (𝐹 ↾_s 𝑉) = ((𝐸 ↾_s 𝑈) ↾_s 𝑉)
12		fedgmul.k	. . . . . . 7 ⊢ 𝐾 = (𝐸 ↾_s 𝑉)
13	10, 11, 12	3eqtr4g 2881	. . . . . 6 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) = 𝐾)
14		fedgmul.3	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ DivRing)
15	13, 14	eqeltrd 2913	. . . . 5 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) ∈ DivRing)
16		fedgmul.c	. . . . . 6 ⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
17		eqid 2821	. . . . . 6 ⊢ (𝐹 ↾_s 𝑉) = (𝐹 ↾_s 𝑉)
18	16, 17	sralvec 30990	. . . . 5 ⊢ ((𝐹 ∈ DivRing ∧ (𝐹 ↾_s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
19	1, 15, 3, 18	syl3anc 1367	. . . 4 ⊢ (𝜑 → 𝐶 ∈ LVec)
20		eqid 2821	. . . . 5 ⊢ (LBasis‘𝐶) = (LBasis‘𝐶)
21	20	lbsex 19937	. . . 4 ⊢ (𝐶 ∈ LVec → (LBasis‘𝐶) ≠ ∅)
22	19, 21	syl 17	. . 3 ⊢ (𝜑 → (LBasis‘𝐶) ≠ ∅)
23		n0 4310	. . 3 ⊢ ((LBasis‘𝐶) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (LBasis‘𝐶))
24	22, 23	sylib 220	. 2 ⊢ (𝜑 → ∃𝑥 𝑥 ∈ (LBasis‘𝐶))
25		fedgmul.1	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ DivRing)
26		fedgmul.b	. . . . . . . 8 ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
27	26, 4	sralvec 30990	. . . . . . 7 ⊢ ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐵 ∈ LVec)
28	25, 1, 2, 27	syl3anc 1367	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ LVec)
29		eqid 2821	. . . . . . 7 ⊢ (LBasis‘𝐵) = (LBasis‘𝐵)
30	29	lbsex 19937	. . . . . 6 ⊢ (𝐵 ∈ LVec → (LBasis‘𝐵) ≠ ∅)
31	28, 30	syl 17	. . . . 5 ⊢ (𝜑 → (LBasis‘𝐵) ≠ ∅)
32		n0 4310	. . . . 5 ⊢ ((LBasis‘𝐵) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (LBasis‘𝐵))
33	31, 32	sylib 220	. . . 4 ⊢ (𝜑 → ∃𝑦 𝑦 ∈ (LBasis‘𝐵))
34	33	adantr 483	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) → ∃𝑦 𝑦 ∈ (LBasis‘𝐵))
35		drngring 19509	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
36	25, 35	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ∈ Ring)
37	36	ad4antr 730	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝐸 ∈ Ring)
38		simplr 767	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ∈ (LBasis‘𝐶))
39		eqid 2821	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝐶) = (Base‘𝐶)
40	39, 20	lbsss 19849	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (LBasis‘𝐶) → 𝑥 ⊆ (Base‘𝐶))
41	38, 40	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ⊆ (Base‘𝐶))
42		eqid 2821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Base‘𝐸) = (Base‘𝐸)
43	42	subrgss 19536	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
44	2, 43	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐸))
45	4, 42	ressbas2 16555	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
46	44, 45	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑈 = (Base‘𝐹))
47	16	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐶 = ((subringAlg ‘𝐹)‘𝑉))
48		eqid 2821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Base‘𝐹) = (Base‘𝐹)
49	48	subrgss 19536	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
50	3, 49	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐹))
51	47, 50	srabase 19950	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Base‘𝐹) = (Base‘𝐶))
52	46, 51	eqtrd 2856	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 = (Base‘𝐶))
53	52, 44	eqsstrrd 4006	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
54	53	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘𝐶) ⊆ (Base‘𝐸))
55	41, 54	sstrd 3977	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ⊆ (Base‘𝐸))
56	55	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑥 ⊆ (Base‘𝐸))
57		simpr 487	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑖 ∈ 𝑥)
58	56, 57	sseldd 3968	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑖 ∈ (Base‘𝐸))
59		simpr 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ∈ (LBasis‘𝐵))
60		eqid 2821	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝐵) = (Base‘𝐵)
61	60, 29	lbsss 19849	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (LBasis‘𝐵) → 𝑦 ⊆ (Base‘𝐵))
62	59, 61	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ⊆ (Base‘𝐵))
63	26	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 = ((subringAlg ‘𝐸)‘𝑈))
64	63, 44	srabase 19950	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐵))
65	64	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘𝐸) = (Base‘𝐵))
66	62, 65	sseqtrrd 4008	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ⊆ (Base‘𝐸))
67	66	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑦 ⊆ (Base‘𝐸))
68		simplr 767	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑗 ∈ 𝑦)
69	67, 68	sseldd 3968	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑗 ∈ (Base‘𝐸))
70		eqid 2821	. . . . . . . . . . . . . 14 ⊢ (._r‘𝐸) = (._r‘𝐸)
71	42, 70	ringcl 19311	. . . . . . . . . . . . 13 ⊢ ((𝐸 ∈ Ring ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸)) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐸))
72	37, 58, 69, 71	syl3anc 1367	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐸))
73		fedgmul.a	. . . . . . . . . . . . . . 15 ⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑉)
74	73	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝐸)‘𝑉))
75	7	simpld 497	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐸))
76	42	subrgss 19536	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
77	75, 76	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐸))
78	74, 77	srabase 19950	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐴))
79	78	ad4antr 730	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (Base‘𝐸) = (Base‘𝐴))
80	72, 79	eleqtrd 2915	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴))
81	80	anasss 469	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴))
82	81	ralrimivva 3191	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴))
83		oveq2 7164	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑗 → (𝑡(._r‘𝐸)𝑤) = (𝑡(._r‘𝐸)𝑗))
84		oveq1 7163	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑖 → (𝑡(._r‘𝐸)𝑗) = (𝑖(._r‘𝐸)𝑗))
85	83, 84	cbvmpov 7249	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) = (𝑗 ∈ 𝑦, 𝑖 ∈ 𝑥 ↦ (𝑖(._r‘𝐸)𝑗))
86	85	fmpo 7766	. . . . . . . . 9 ⊢ (∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴) ↔ (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴))
87	82, 86	sylib 220	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴))
88		eqid 2821	. . . . . . . . . . . . . 14 ⊢ (Base‘(Scalar‘𝐵)) = (Base‘(Scalar‘𝐵))
89		eqid 2821	. . . . . . . . . . . . . 14 ⊢ ( ·_𝑠 ‘𝐵) = ( ·_𝑠 ‘𝐵)
90		eqid 2821	. . . . . . . . . . . . . 14 ⊢ (+_g‘𝐵) = (+_g‘𝐵)
91		eqid 2821	. . . . . . . . . . . . . 14 ⊢ (0_g‘(Scalar‘𝐵)) = (0_g‘(Scalar‘𝐵))
92	28	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐵 ∈ LVec)
93	92	ad5antr 732	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝐵 ∈ LVec)
94	29	lbslinds 20977	. . . . . . . . . . . . . . . 16 ⊢ (LBasis‘𝐵) ⊆ (LIndS‘𝐵)
95	94, 59	sseldi 3965	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ∈ (LIndS‘𝐵))
96	95	ad5antr 732	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑦 ∈ (LIndS‘𝐵))
97	68	ad3antrrr 728	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑗 ∈ 𝑦)
98		simpllr 774	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑣 ∈ 𝑦)
99	63, 44	srasca 19953	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ↾_s 𝑈) = (Scalar‘𝐵))
100	4, 99	syl5eq 2868	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 = (Scalar‘𝐵))
101	100	fveq2d 6674	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Base‘𝐹) = (Base‘(Scalar‘𝐵)))
102	101, 51	eqtr3d 2858	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Base‘(Scalar‘𝐵)) = (Base‘𝐶))
103	102	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘(Scalar‘𝐵)) = (Base‘𝐶))
104	41, 103	sseqtrrd 4008	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ⊆ (Base‘(Scalar‘𝐵)))
105	104	ad5antr 732	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑥 ⊆ (Base‘(Scalar‘𝐵)))
106		simp-4r 782	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑖 ∈ 𝑥)
107	105, 106	sseldd 3968	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑖 ∈ (Base‘(Scalar‘𝐵)))
108		simplr 767	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑢 ∈ 𝑥)
109	105, 108	sseldd 3968	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑢 ∈ (Base‘(Scalar‘𝐵)))
110	19	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐶 ∈ LVec)
111		eqid 2821	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (LSpan‘𝐶) = (LSpan‘𝐶)
112	39, 20, 111	islbs4 20976	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (LBasis‘𝐶) ↔ (𝑥 ∈ (LIndS‘𝐶) ∧ ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶)))
113	38, 112	sylib 220	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑥 ∈ (LIndS‘𝐶) ∧ ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶)))
114	113	simpld 497	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ∈ (LIndS‘𝐶))
115		eqid 2821	. . . . . . . . . . . . . . . . . . 19 ⊢ (0_g‘𝐶) = (0_g‘𝐶)
116	115	0nellinds 30935	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐶 ∈ LVec ∧ 𝑥 ∈ (LIndS‘𝐶)) → ¬ (0_g‘𝐶) ∈ 𝑥)
117	110, 114, 116	syl2anc 586	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ¬ (0_g‘𝐶) ∈ 𝑥)
118	117	ad5antr 732	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → ¬ (0_g‘𝐶) ∈ 𝑥)
119		nelne2 3115	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ 𝑥 ∧ ¬ (0_g‘𝐶) ∈ 𝑥) → 𝑖 ≠ (0_g‘𝐶))
120	106, 118, 119	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑖 ≠ (0_g‘𝐶))
121	100	fveq2d 6674	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0_g‘𝐹) = (0_g‘(Scalar‘𝐵)))
122	16, 1, 3	drgext0g 30992	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0_g‘𝐹) = (0_g‘𝐶))
123	121, 122	eqtr3d 2858	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0_g‘(Scalar‘𝐵)) = (0_g‘𝐶))
124	123	ad7antr 736	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (0_g‘(Scalar‘𝐵)) = (0_g‘𝐶))
125	120, 124	neeqtrrd 3090	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑖 ≠ (0_g‘(Scalar‘𝐵)))
126		simpr 487	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢))
127		ovexd 7191	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑖(._r‘𝐸)𝑗) ∈ V)
128	85	ovmpt4g 7297	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥 ∧ (𝑖(._r‘𝐸)𝑗) ∈ V) → (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑖(._r‘𝐸)𝑗))
129	97, 106, 127, 128	syl3anc 1367	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑖(._r‘𝐸)𝑗))
130	26, 25, 2	drgextvsca 30993	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (._r‘𝐸) = ( ·_𝑠 ‘𝐵))
131	130	oveqd 7173	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑖(._r‘𝐸)𝑗) = (𝑖( ·_𝑠 ‘𝐵)𝑗))
132	131	ad7antr 736	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑖(._r‘𝐸)𝑗) = (𝑖( ·_𝑠 ‘𝐵)𝑗))
133	129, 132	eqtrd 2856	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑖( ·_𝑠 ‘𝐵)𝑗))
134	85	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) = (𝑗 ∈ 𝑦, 𝑖 ∈ 𝑥 ↦ (𝑖(._r‘𝐸)𝑗)))
135		simprr 771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)) → 𝑖 = 𝑢)
136		simprl 769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)) → 𝑗 = 𝑣)
137	135, 136	oveq12d 7174	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)) → (𝑖(._r‘𝐸)𝑗) = (𝑢(._r‘𝐸)𝑣))
138		simplr 767	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → 𝑣 ∈ 𝑦)
139		simpr 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → 𝑢 ∈ 𝑥)
140		ovexd 7191	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑢(._r‘𝐸)𝑣) ∈ V)
141	134, 137, 138, 139, 140	ovmpod 7302	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) = (𝑢(._r‘𝐸)𝑣))
142	141	adantllr 717	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) = (𝑢(._r‘𝐸)𝑣))
143	142	adantl3r 748	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) = (𝑢(._r‘𝐸)𝑣))
144	143	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) = (𝑢(._r‘𝐸)𝑣))
145	130	oveqd 7173	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑢(._r‘𝐸)𝑣) = (𝑢( ·_𝑠 ‘𝐵)𝑣))
146	145	ad7antr 736	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑢(._r‘𝐸)𝑣) = (𝑢( ·_𝑠 ‘𝐵)𝑣))
147	144, 146	eqtrd 2856	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) = (𝑢( ·_𝑠 ‘𝐵)𝑣))
148	126, 133, 147	3eqtr3d 2864	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑖( ·_𝑠 ‘𝐵)𝑗) = (𝑢( ·_𝑠 ‘𝐵)𝑣))
149	88, 89, 90, 91, 93, 96, 97, 98, 107, 109, 125, 148	linds2eq 30941	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢))
150	149	ex 415	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
151	150	anasss 469	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ (𝑣 ∈ 𝑦 ∧ 𝑢 ∈ 𝑥)) → ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
152	151	ralrimivva 3191	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → ∀𝑣 ∈ 𝑦 ∀𝑢 ∈ 𝑥 ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
153	152	anasss 469	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → ∀𝑣 ∈ 𝑦 ∀𝑢 ∈ 𝑥 ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
154	153	ralrimivva 3191	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 ∀𝑣 ∈ 𝑦 ∀𝑢 ∈ 𝑥 ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
155		f1opr 7210	. . . . . . . 8 ⊢ ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)–1-1→(Base‘𝐴) ↔ ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴) ∧ ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 ∀𝑣 ∈ 𝑦 ∀𝑢 ∈ 𝑥 ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢))))
156	87, 154, 155	sylanbrc 585	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)–1-1→(Base‘𝐴))
157	59, 38	xpexd 7474	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑦 × 𝑥) ∈ V)
158		f1rnen 30374	. . . . . . 7 ⊢ (((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)–1-1→(Base‘𝐴) ∧ (𝑦 × 𝑥) ∈ V) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ≈ (𝑦 × 𝑥))
159	156, 157, 158	syl2anc 586	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ≈ (𝑦 × 𝑥))
160		hasheni 13709	. . . . . 6 ⊢ (ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ≈ (𝑦 × 𝑥) → (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = (♯‘(𝑦 × 𝑥)))
161	159, 160	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = (♯‘(𝑦 × 𝑥)))
162		hashxpe 30529	. . . . . 6 ⊢ ((𝑦 ∈ (LBasis‘𝐵) ∧ 𝑥 ∈ (LBasis‘𝐶)) → (♯‘(𝑦 × 𝑥)) = ((♯‘𝑦) ·_e (♯‘𝑥)))
163	59, 38, 162	syl2anc 586	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (♯‘(𝑦 × 𝑥)) = ((♯‘𝑦) ·_e (♯‘𝑥)))
164	161, 163	eqtrd 2856	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = ((♯‘𝑦) ·_e (♯‘𝑥)))
165	73, 12	sralvec 30990	. . . . . . 7 ⊢ ((𝐸 ∈ DivRing ∧ 𝐾 ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec)
166	25, 14, 75, 165	syl3anc 1367	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ LVec)
167	166	ad2antrr 724	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐴 ∈ LVec)
168		lveclmod 19878	. . . . . . . . 9 ⊢ (𝐴 ∈ LVec → 𝐴 ∈ LMod)
169	166, 168	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ LMod)
170	169	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐴 ∈ LMod)
171	25	ad4antr 730	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝐸 ∈ DivRing)
172	1	ad4antr 730	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝐹 ∈ DivRing)
173	14	ad4antr 730	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝐾 ∈ DivRing)
174	2	ad4antr 730	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝑈 ∈ (SubRing‘𝐸))
175	3	ad4antr 730	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝑉 ∈ (SubRing‘𝐹))
176		fveq2 6670	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑗 → (𝑓‘𝑤) = (𝑓‘𝑗))
177	176	fveq1d 6672	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑗 → ((𝑓‘𝑤)‘𝑣) = ((𝑓‘𝑗)‘𝑣))
178		fveq2 6670	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑖 → ((𝑓‘𝑗)‘𝑣) = ((𝑓‘𝑗)‘𝑖))
179	177, 178	cbvmpov 7249	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) = (𝑗 ∈ 𝑦, 𝑖 ∈ 𝑥 ↦ ((𝑓‘𝑗)‘𝑖))
180		simp-4r 782	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝑥 ∈ (LBasis‘𝐶))
181		simpllr 774	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝑦 ∈ (LBasis‘𝐵))
182		simplr 767	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥))))
183		simpr 487	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴))
184	73, 26, 16, 4, 12, 171, 172, 173, 174, 175, 85, 179, 180, 181, 182, 183	fedgmullem2 31026	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝑐 = ((𝑦 × 𝑥) × {(0_g‘(Scalar‘𝐴))}))
185	184	ex 415	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) → ((𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0_g‘(Scalar‘𝐴))})))
186	185	ralrimiva 3182	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))((𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0_g‘(Scalar‘𝐴))})))
187		eqid 2821	. . . . . . . . 9 ⊢ (Base‘𝐴) = (Base‘𝐴)
188		eqid 2821	. . . . . . . . 9 ⊢ (Scalar‘𝐴) = (Scalar‘𝐴)
189		eqid 2821	. . . . . . . . 9 ⊢ ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘𝐴)
190		eqid 2821	. . . . . . . . 9 ⊢ (0_g‘𝐴) = (0_g‘𝐴)
191		eqid 2821	. . . . . . . . 9 ⊢ (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐴))
192		eqid 2821	. . . . . . . . 9 ⊢ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥))) = (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))
193	187, 188, 189, 190, 191, 192	islindf4 20982	. . . . . . . 8 ⊢ ((𝐴 ∈ LMod ∧ (𝑦 × 𝑥) ∈ V ∧ (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴)) → ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) LIndF 𝐴 ↔ ∀𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))((𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0_g‘(Scalar‘𝐴))}))))
194	193	biimpar 480	. . . . . . 7 ⊢ (((𝐴 ∈ LMod ∧ (𝑦 × 𝑥) ∈ V ∧ (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴)) ∧ ∀𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))((𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0_g‘(Scalar‘𝐴))}))) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) LIndF 𝐴)
195	170, 157, 87, 186, 194	syl31anc 1369	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) LIndF 𝐴)
196	72	anasss 469	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐸))
197	196	ralrimivva 3191	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐸))
198	85	rnmposs 30419	. . . . . . . . . 10 ⊢ (∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐸) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ⊆ (Base‘𝐸))
199	197, 198	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ⊆ (Base‘𝐸))
200	78	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘𝐸) = (Base‘𝐴))
201	199, 200	sseqtrd 4007	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ⊆ (Base‘𝐴))
202		eqid 2821	. . . . . . . . 9 ⊢ (LSpan‘𝐴) = (LSpan‘𝐴)
203	187, 202	lspssv 19755	. . . . . . . 8 ⊢ ((𝐴 ∈ LMod ∧ ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ⊆ (Base‘𝐴)) → ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) ⊆ (Base‘𝐴))
204	170, 201, 203	syl2anc 586	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) ⊆ (Base‘𝐴))
205		simpl 485	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)))
206	205	ad4antr 730	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → ((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)))
207		elmapi 8428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦) → 𝑎:𝑦⟶(Base‘(Scalar‘𝐵)))
208	207	ad4antlr 731	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → 𝑎:𝑦⟶(Base‘(Scalar‘𝐵)))
209		simpr 487	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → 𝑗 ∈ 𝑦)
210	208, 209	ffvelrnd 6852	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → (𝑎‘𝑗) ∈ (Base‘(Scalar‘𝐵)))
211	113	simprd 498	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶))
212	206, 211	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶))
213	102	ad7antr 736	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → (Base‘(Scalar‘𝐵)) = (Base‘𝐶))
214	212, 213	eqtr4d 2859	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → ((LSpan‘𝐶)‘𝑥) = (Base‘(Scalar‘𝐵)))
215	210, 214	eleqtrrd 2916	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → (𝑎‘𝑗) ∈ ((LSpan‘𝐶)‘𝑥))
216		eqid 2821	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
217		eqid 2821	. . . . . . . . . . . . . . . . 17 ⊢ (Scalar‘𝐶) = (Scalar‘𝐶)
218		eqid 2821	. . . . . . . . . . . . . . . . 17 ⊢ (0_g‘(Scalar‘𝐶)) = (0_g‘(Scalar‘𝐶))
219		eqid 2821	. . . . . . . . . . . . . . . . 17 ⊢ ( ·_𝑠 ‘𝐶) = ( ·_𝑠 ‘𝐶)
220		lveclmod 19878	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 ∈ LVec → 𝐶 ∈ LMod)
221	19, 220	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐶 ∈ LMod)
222	221	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐶 ∈ LMod)
223	111, 39, 216, 217, 218, 219, 222, 41	ellspds 30933	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((𝑎‘𝑗) ∈ ((LSpan‘𝐶)‘𝑥) ↔ ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))))
224	223	biimpa 479	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑎‘𝑗) ∈ ((LSpan‘𝐶)‘𝑥)) → ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
225	206, 215, 224	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
226	225	ralrimiva 3182	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) → ∀𝑗 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
227		fveq2 6670	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑗 → (𝑎‘𝑤) = (𝑎‘𝑗))
228		fveq2 6670	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑖 → (𝑏‘𝑣) = (𝑏‘𝑖))
229		id 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑖 → 𝑣 = 𝑖)
230	228, 229	oveq12d 7174	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = 𝑖 → ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣) = ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖))
231	230	cbvmptv 5169	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)) = (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖))
232	231	oveq2i 7167	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))
233	232	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑗 → (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))
234	227, 233	eqeq12d 2837	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑗 → ((𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) ↔ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
235	234	anbi2d 630	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑗 → ((𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) ↔ (𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))))
236	235	rexbidv 3297	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑗 → (∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) ↔ ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))))
237	236	cbvralvw 3449	. . . . . . . . . . . . . 14 ⊢ (∀𝑤 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) ↔ ∀𝑗 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
238		vex 3497	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
239		breq1 5069	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑓‘𝑤) → (𝑏 finSupp (0_g‘(Scalar‘𝐶)) ↔ (𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶))))
240		fveq1 6669	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (𝑓‘𝑤) → (𝑏‘𝑣) = ((𝑓‘𝑤)‘𝑣))
241	240	oveq1d 7171	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑓‘𝑤) → ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣) = (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))
242	241	mpteq2dv 5162	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑓‘𝑤) → (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)) = (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))
243	242	oveq2d 7172	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑓‘𝑤) → (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))
244	243	eqeq2d 2832	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑓‘𝑤) → ((𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) ↔ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))))
245	239, 244	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑓‘𝑤) → ((𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) ↔ ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))))
246	238, 245	ac6s 9906	. . . . . . . . . . . . . 14 ⊢ (∀𝑤 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) → ∃𝑓(𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))))
247	237, 246	sylbir 237	. . . . . . . . . . . . 13 ⊢ (∀𝑗 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))) → ∃𝑓(𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))))
248	226, 247	syl 17	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) → ∃𝑓(𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))))
249		simpllr 774	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥))
250		simplr 767	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑗 ∈ 𝑦)
251	249, 250	ffvelrnd 6852	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (𝑓‘𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥))
252		elmapi 8428	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓‘𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥) → (𝑓‘𝑗):𝑥⟶(Base‘(Scalar‘𝐶)))
253	251, 252	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (𝑓‘𝑗):𝑥⟶(Base‘(Scalar‘𝐶)))
254	253	anasss 469	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → (𝑓‘𝑗):𝑥⟶(Base‘(Scalar‘𝐶)))
255		simprr 771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → 𝑖 ∈ 𝑥)
256	254, 255	ffvelrnd 6852	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → ((𝑓‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐶)))
257	74, 77	srasca 19953	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐸 ↾_s 𝑉) = (Scalar‘𝐴))
258	12, 257	syl5eq 2868	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐴))
259	47, 50	srasca 19953	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) = (Scalar‘𝐶))
260	13, 259	eqtr3d 2858	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐶))
261	258, 260	eqtr3d 2858	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
262	261	fveq2d 6674	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
263	262	ad4antr 730	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
264	256, 263	eleqtrrd 2916	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → ((𝑓‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
265	264	ralrimivva 3191	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) → ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 ((𝑓‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
266	179	fmpo 7766	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 ((𝑓‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)) ↔ (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)):(𝑦 × 𝑥)⟶(Base‘(Scalar‘𝐴)))
267	265, 266	sylib 220	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) → (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)):(𝑦 × 𝑥)⟶(Base‘(Scalar‘𝐴)))
268		fvexd 6685	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) → (Base‘(Scalar‘𝐴)) ∈ V)
269	157	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) → (𝑦 × 𝑥) ∈ V)
270	268, 269	elmapd 8420	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) → ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥)) ↔ (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)):(𝑦 × 𝑥)⟶(Base‘(Scalar‘𝐴))))
271	267, 270	mpbird 259	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) → (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥)))
272	271	ad5ant15 757	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) → (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥)))
273	272	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥)))
274	273	adantl3r 748	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥)))
275		simpr 487	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) ∧ 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣))) → 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)))
276	275	breq1d 5076	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) ∧ 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣))) → (𝑐 finSupp (0_g‘(Scalar‘𝐴)) ↔ (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) finSupp (0_g‘(Scalar‘𝐴))))
277	275	oveq1d 7171	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) ∧ 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣))) → (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))
278	277	oveq2d 7172	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) ∧ 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣))) → (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (𝐴 Σ_g ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))))
279	278	eqeq2d 2832	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) ∧ 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣))) → (𝑧 = (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) ↔ 𝑧 = (𝐴 Σ_g ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))))
280	276, 279	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) ∧ 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣))) → ((𝑐 finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))) ↔ ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))))))
281	25	ad8antr 738	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝐸 ∈ DivRing)
282	1	ad8antr 738	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝐹 ∈ DivRing)
283	14	ad8antr 738	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝐾 ∈ DivRing)
284	2	ad8antr 738	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑈 ∈ (SubRing‘𝐸))
285	3	ad8antr 738	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑉 ∈ (SubRing‘𝐹))
286	38	ad6antr 734	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑥 ∈ (LBasis‘𝐶))
287	59	ad6antr 734	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑦 ∈ (LBasis‘𝐵))
288		simpr 487	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ (Base‘𝐴))
289	288	ad5antr 732	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑧 ∈ (Base‘𝐴))
290	207	ad5antlr 733	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑎:𝑦⟶(Base‘(Scalar‘𝐵)))
291		simp-4r 782	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑎 finSupp (0_g‘(Scalar‘𝐵)))
292		simpllr 774	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤))))
293		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑗 → 𝑤 = 𝑗)
294	227, 293	oveq12d 7174	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑗 → ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤) = ((𝑎‘𝑗)( ·_𝑠 ‘𝐵)𝑗))
295	294	cbvmptv 5169	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)) = (𝑗 ∈ 𝑦 ↦ ((𝑎‘𝑗)( ·_𝑠 ‘𝐵)𝑗))
296	295	oveq2i 7167	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤))) = (𝐵 Σ_g (𝑗 ∈ 𝑦 ↦ ((𝑎‘𝑗)( ·_𝑠 ‘𝐵)𝑗)))
297	292, 296	syl6eq 2872	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑧 = (𝐵 Σ_g (𝑗 ∈ 𝑦 ↦ ((𝑎‘𝑗)( ·_𝑠 ‘𝐵)𝑗))))
298		simplr 767	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥))
299		simpr 487	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))))
300	176	breq1d 5076	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑗 → ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ↔ (𝑓‘𝑗) finSupp (0_g‘(Scalar‘𝐶))))
301		fveq2 6670	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = 𝑖 → ((𝑓‘𝑤)‘𝑣) = ((𝑓‘𝑤)‘𝑖))
302	301, 229	oveq12d 7174	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 = 𝑖 → (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣) = (((𝑓‘𝑤)‘𝑖)( ·_𝑠 ‘𝐶)𝑖))
303	302	cbvmptv 5169	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)) = (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑖)( ·_𝑠 ‘𝐶)𝑖))
304	176	fveq1d 6672	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 𝑗 → ((𝑓‘𝑤)‘𝑖) = ((𝑓‘𝑗)‘𝑖))
305	304	oveq1d 7171	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 𝑗 → (((𝑓‘𝑤)‘𝑖)( ·_𝑠 ‘𝐶)𝑖) = (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖))
306	305	mpteq2dv 5162	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑗 → (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)) = (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))
307	303, 306	syl5eq 2868	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑗 → (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)) = (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))
308	307	oveq2d 7172	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑗 → (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))
309	227, 308	eqeq12d 2837	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑗 → ((𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) ↔ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
310	300, 309	anbi12d 632	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑗 → (((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) ↔ ((𝑓‘𝑗) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))))
311	310	cbvralvw 3449	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) ↔ ∀𝑗 ∈ 𝑦 ((𝑓‘𝑗) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
312	299, 311	sylib 220	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → ∀𝑗 ∈ 𝑦 ((𝑓‘𝑗) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
313	312	r19.21bi 3208	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) ∧ 𝑗 ∈ 𝑦) → ((𝑓‘𝑗) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
314	313	simpld 497	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) ∧ 𝑗 ∈ 𝑦) → (𝑓‘𝑗) finSupp (0_g‘(Scalar‘𝐶)))
315	313	simprd 498	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) ∧ 𝑗 ∈ 𝑦) → (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))
316	73, 26, 16, 4, 12, 281, 282, 283, 284, 285, 85, 179, 286, 287, 289, 290, 291, 297, 298, 314, 315	fedgmullem1 31025	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))))
317	274, 280, 316	rspcedvd 3626	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥))(𝑐 finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))))
318	317	anasss 469	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ (𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))))) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥))(𝑐 finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))))
319	248, 318	exlimddv 1936	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥))(𝑐 finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))))
320	319	anasss 469	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ (𝑎 finSupp (0_g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤))))) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥))(𝑐 finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))))
321		eqid 2821	. . . . . . . . . . . . . . . . 17 ⊢ (LSpan‘𝐵) = (LSpan‘𝐵)
322	60, 29, 321	islbs4 20976	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (LBasis‘𝐵) ↔ (𝑦 ∈ (LIndS‘𝐵) ∧ ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵)))
323	59, 322	sylib 220	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑦 ∈ (LIndS‘𝐵) ∧ ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵)))
324	323	simprd 498	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵))
325	324	adantr 483	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵))
326	78, 64	eqtr3d 2858	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Base‘𝐴) = (Base‘𝐵))
327	326	ad3antrrr 728	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → (Base‘𝐴) = (Base‘𝐵))
328	325, 327	eqtr4d 2859	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((LSpan‘𝐵)‘𝑦) = (Base‘𝐴))
329	288, 328	eleqtrrd 2916	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ ((LSpan‘𝐵)‘𝑦))
330		eqid 2821	. . . . . . . . . . . . 13 ⊢ (Scalar‘𝐵) = (Scalar‘𝐵)
331		lveclmod 19878	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ LVec → 𝐵 ∈ LMod)
332	28, 331	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ LMod)
333	332	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐵 ∈ LMod)
334	321, 60, 88, 330, 91, 89, 333, 62	ellspds 30933	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑧 ∈ ((LSpan‘𝐵)‘𝑦) ↔ ∃𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)(𝑎 finSupp (0_g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤))))))
335	334	biimpa 479	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ ((LSpan‘𝐵)‘𝑦)) → ∃𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)(𝑎 finSupp (0_g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))))
336	205, 329, 335	syl2anc 586	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ∃𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)(𝑎 finSupp (0_g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))))
337	320, 336	r19.29a 3289	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥))(𝑐 finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))))
338		eqid 2821	. . . . . . . . . . 11 ⊢ (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴))
339	202, 187, 338, 188, 191, 189, 87, 170, 157	ellspd 20946	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑧 ∈ ((LSpan‘𝐴)‘((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) “ (𝑦 × 𝑥))) ↔ ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥))(𝑐 finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))))))
340	339	adantr 483	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑧 ∈ ((LSpan‘𝐴)‘((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) “ (𝑦 × 𝑥))) ↔ ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥))(𝑐 finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))))))
341	337, 340	mpbird 259	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ ((LSpan‘𝐴)‘((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) “ (𝑦 × 𝑥))))
342	87	ffnd 6515	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) Fn (𝑦 × 𝑥))
343	342	adantr 483	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) Fn (𝑦 × 𝑥))
344		fnima 6478	. . . . . . . . . 10 ⊢ ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) Fn (𝑦 × 𝑥) → ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) “ (𝑦 × 𝑥)) = ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))
345	343, 344	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) “ (𝑦 × 𝑥)) = ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))
346	345	fveq2d 6674	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((LSpan‘𝐴)‘((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) “ (𝑦 × 𝑥))) = ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))
347	341, 346	eleqtrd 2915	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))
348	204, 347	eqelssd 3988	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = (Base‘𝐴))
349		eqid 2821	. . . . . . 7 ⊢ (Base‘(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = (Base‘(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))
350		drngnzr 20035	. . . . . . . . . 10 ⊢ (𝐾 ∈ DivRing → 𝐾 ∈ NzRing)
351	14, 350	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ NzRing)
352	258, 351	eqeltrrd 2914	. . . . . . . 8 ⊢ (𝜑 → (Scalar‘𝐴) ∈ NzRing)
353	352	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Scalar‘𝐴) ∈ NzRing)
354	187, 349, 188, 189, 190, 191, 202, 170, 353, 157, 156	lindflbs 30940	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ∈ (LBasis‘𝐴) ↔ ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) LIndF 𝐴 ∧ ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = (Base‘𝐴))))
355	195, 348, 354	mpbir2and 711	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ∈ (LBasis‘𝐴))
356		eqid 2821	. . . . . 6 ⊢ (LBasis‘𝐴) = (LBasis‘𝐴)
357	356	dimval 31001	. . . . 5 ⊢ ((𝐴 ∈ LVec ∧ ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ∈ (LBasis‘𝐴)) → (dim‘𝐴) = (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))
358	167, 355, 357	syl2anc 586	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐴) = (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))
359	29	dimval 31001	. . . . . 6 ⊢ ((𝐵 ∈ LVec ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐵) = (♯‘𝑦))
360	92, 59, 359	syl2anc 586	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐵) = (♯‘𝑦))
361	20	dimval 31001	. . . . . 6 ⊢ ((𝐶 ∈ LVec ∧ 𝑥 ∈ (LBasis‘𝐶)) → (dim‘𝐶) = (♯‘𝑥))
362	110, 38, 361	syl2anc 586	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐶) = (♯‘𝑥))
363	360, 362	oveq12d 7174	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((dim‘𝐵) ·_e (dim‘𝐶)) = ((♯‘𝑦) ·_e (♯‘𝑥)))
364	164, 358, 363	3eqtr4d 2866	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐴) = ((dim‘𝐵) ·_e (dim‘𝐶)))
365	34, 364	exlimddv 1936	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) → (dim‘𝐴) = ((dim‘𝐵) ·_e (dim‘𝐶)))
366	24, 365	exlimddv 1936	1 ⊢ (𝜑 → (dim‘𝐴) = ((dim‘𝐵) ·_e (dim‘𝐶)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1537 ∃wex 1780 ∈ wcel 2114 ≠ wne 3016 ∀wral 3138 ∃wrex 3139 Vcvv 3494 ⊆ wss 3936 ∅c0 4291 {csn 4567 class class class wbr 5066 ↦ cmpt 5146 × cxp 5553 ran crn 5556 “ cima 5558 Fn wfn 6350 ⟶wf 6351 –1-1→wf1 6352 ‘cfv 6355 (class class class)co 7156 ∈ cmpo 7158 ∘_f cof 7407 ↑_m cmap 8406 ≈ cen 8506 finSupp cfsupp 8833 ·_e cxmu 12507 ♯chash 13691 Basecbs 16483 ↾_s cress 16484 +_gcplusg 16565 ._rcmulr 16566 Scalarcsca 16568 ·_𝑠 cvsca 16569 0_gc0g 16713 Σ_g cgsu 16714 Ringcrg 19297 DivRingcdr 19502 SubRingcsubrg 19531 LModclmod 19634 LSpanclspn 19743 LBasisclbs 19846 LVecclvec 19874 subringAlg csra 19940 NzRingcnzr 20030 freeLMod cfrlm 20890 LIndF clindf 20948 LIndSclinds 20949 dimcldim 30999

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-rep 5190 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-reg 9056 ax-inf2 9104 ax-ac2 9885 ax-cnex 10593 ax-resscn 10594 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-addrcl 10598 ax-mulcl 10599 ax-mulrcl 10600 ax-mulcom 10601 ax-addass 10602 ax-mulass 10603 ax-distr 10604 ax-i2m1 10605 ax-1ne0 10606 ax-1rid 10607 ax-rnegex 10608 ax-rrecex 10609 ax-cnre 10610 ax-pre-lttri 10611 ax-pre-lttrn 10612 ax-pre-ltadd 10613 ax-pre-mulgt0 10614

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-fal 1550 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-int 4877 df-iun 4921 df-iin 4922 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-se 5515 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-isom 6364 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-of 7409 df-rpss 7449 df-om 7581 df-1st 7689 df-2nd 7690 df-supp 7831 df-tpos 7892 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-1o 8102 df-oadd 8106 df-er 8289 df-map 8408 df-ixp 8462 df-en 8510 df-dom 8511 df-sdom 8512 df-fin 8513 df-fsupp 8834 df-sup 8906 df-oi 8974 df-r1 9193 df-rank 9194 df-dju 9330 df-card 9368 df-acn 9371 df-ac 9542 df-pnf 10677 df-mnf 10678 df-xr 10679 df-ltxr 10680 df-le 10681 df-sub 10872 df-neg 10873 df-nn 11639 df-2 11701 df-3 11702 df-4 11703 df-5 11704 df-6 11705 df-7 11706 df-8 11707 df-9 11708 df-n0 11899 df-xnn0 11969 df-z 11983 df-dec 12100 df-uz 12245 df-xmul 12510 df-fz 12894 df-fzo 13035 df-seq 13371 df-hash 13692 df-struct 16485 df-ndx 16486 df-slot 16487 df-base 16489 df-sets 16490 df-ress 16491 df-plusg 16578 df-mulr 16579 df-sca 16581 df-vsca 16582 df-ip 16583 df-tset 16584 df-ple 16585 df-ocomp 16586 df-ds 16587 df-hom 16589 df-cco 16590 df-0g 16715 df-gsum 16716 df-prds 16721 df-pws 16723 df-mre 16857 df-mrc 16858 df-mri 16859 df-acs 16860 df-proset 17538 df-drs 17539 df-poset 17556 df-ipo 17762 df-mgm 17852 df-sgrp 17901 df-mnd 17912 df-mhm 17956 df-submnd 17957 df-grp 18106 df-minusg 18107 df-sbg 18108 df-mulg 18225 df-subg 18276 df-ghm 18356 df-cntz 18447 df-cmn 18908 df-abl 18909 df-mgp 19240 df-ur 19252 df-ring 19299 df-oppr 19373 df-dvdsr 19391 df-unit 19392 df-invr 19422 df-drng 19504 df-subrg 19533 df-lmod 19636 df-lss 19704 df-lsp 19744 df-lmhm 19794 df-lbs 19847 df-lvec 19875 df-sra 19944 df-rgmod 19945 df-nzr 20031 df-dsmm 20876 df-frlm 20891 df-uvc 20927 df-lindf 20950 df-linds 20951 df-dim 31000

This theorem is referenced by: extdgmul 31051

W3C validator