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 34367

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.) Remove dependency on ax-reg 9621. (Revised by Timothy J. O'Malley, 15-Oct-2026.)

**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	. . . 4 ⊢ (𝜑 → 𝐹 ∈ DivRing)
2		fedgmul.4	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸))
3		fedgmul.5	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐹))
4		fedgmul.f	. . . . . . . . . . 11 ⊢ 𝐹 = (𝐸 ↾_s 𝑈)
5	4	subsubrg 20892	. . . . . . . . . 10 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (𝑉 ∈ (SubRing‘𝐹) ↔ (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈)))
6	5	biimpa 482	. . . . . . . . 9 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ∈ (SubRing‘𝐹)) → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))
7	2, 3, 6	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))
8	7	simprd 501	. . . . . . 7 ⊢ (𝜑 → 𝑉 ⊆ 𝑈)
9		ressabs 17467	. . . . . . 7 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈) → ((𝐸 ↾_s 𝑈) ↾_s 𝑉) = (𝐸 ↾_s 𝑉))
10	2, 8, 9	syl2anc 596	. . . . . 6 ⊢ (𝜑 → ((𝐸 ↾_s 𝑈) ↾_s 𝑉) = (𝐸 ↾_s 𝑉))
11	4	oveq1i 7459	. . . . . 6 ⊢ (𝐹 ↾_s 𝑉) = ((𝐸 ↾_s 𝑈) ↾_s 𝑉)
12		fedgmul.k	. . . . . 6 ⊢ 𝐾 = (𝐸 ↾_s 𝑉)
13	10, 11, 12	3eqtr4g 2823	. . . . 5 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) = 𝐾)
14		fedgmul.3	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ DivRing)
15	13, 14	eqeltrd 2864	. . . 4 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) ∈ DivRing)
16		fedgmul.c	. . . . 5 ⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
17		eqid 2763	. . . . 5 ⊢ (𝐹 ↾_s 𝑉) = (𝐹 ↾_s 𝑉)
18	16, 17	sralvec 34321	. . . 4 ⊢ ((𝐹 ∈ DivRing ∧ (𝐹 ↾_s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
19	1, 15, 3, 18	syl3anc 1399	. . 3 ⊢ (𝜑 → 𝐶 ∈ LVec)
20		eqid 2763	. . . 4 ⊢ (LBasis‘𝐶) = (LBasis‘𝐶)
21	20	lbsex 21485	. . 3 ⊢ (𝐶 ∈ LVec → (LBasis‘𝐶) ≠ ∅)
22	19, 21	syl 18	. 2 ⊢ (𝜑 → (LBasis‘𝐶) ≠ ∅)
23		fedgmul.1	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ DivRing)
24		fedgmul.b	. . . . . . . 8 ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
25	24, 4	sralvec 34321	. . . . . . 7 ⊢ ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐵 ∈ LVec)
26	23, 1, 2, 25	syl3anc 1399	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ LVec)
27		eqid 2763	. . . . . . 7 ⊢ (LBasis‘𝐵) = (LBasis‘𝐵)
28	27	lbsex 21485	. . . . . 6 ⊢ (𝐵 ∈ LVec → (LBasis‘𝐵) ≠ ∅)
29	26, 28	syl 18	. . . . 5 ⊢ (𝜑 → (LBasis‘𝐵) ≠ ∅)
30		n0 4303	. . . . 5 ⊢ ((LBasis‘𝐵) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (LBasis‘𝐵))
31	29, 30	sylib 221	. . . 4 ⊢ (𝜑 → ∃𝑦 𝑦 ∈ (LBasis‘𝐵))
32	31	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) → ∃𝑦 𝑦 ∈ (LBasis‘𝐵))
33		eqid 2763	. . . . . . . . . . . . 13 ⊢ (Base‘𝐸) = (Base‘𝐸)
34		eqid 2763	. . . . . . . . . . . . 13 ⊢ (._r‘𝐸) = (._r‘𝐸)
35	23	drngringd 21030	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ∈ Ring)
36	35	ad4antr 745	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝐸 ∈ Ring)
37		simplr 781	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ∈ (LBasis‘𝐶))
38		eqid 2763	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝐶) = (Base‘𝐶)
39	38, 20	lbsss 21394	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (LBasis‘𝐶) → 𝑥 ⊆ (Base‘𝐶))
40	37, 39	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ⊆ (Base‘𝐶))
41	33	subrgss 20866	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
42	2, 41	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐸))
43	4, 33	ressbas2 17457	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
44	42, 43	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑈 = (Base‘𝐹))
45	16	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐶 = ((subringAlg ‘𝐹)‘𝑉))
46		eqid 2763	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Base‘𝐹) = (Base‘𝐹)
47	46	subrgss 20866	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
48	3, 47	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐹))
49	45, 48	srabase 21494	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Base‘𝐹) = (Base‘𝐶))
50	44, 49	eqtrd 2798	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 = (Base‘𝐶))
51	50, 42	eqsstrrd 3948	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
52	51	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘𝐶) ⊆ (Base‘𝐸))
53	40, 52	sstrd 3923	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ⊆ (Base‘𝐸))
54	53	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑥 ⊆ (Base‘𝐸))
55		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑖 ∈ 𝑥)
56	54, 55	sseldd 3914	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑖 ∈ (Base‘𝐸))
57		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ∈ (LBasis‘𝐵))
58		eqid 2763	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝐵) = (Base‘𝐵)
59	58, 27	lbsss 21394	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (LBasis‘𝐵) → 𝑦 ⊆ (Base‘𝐵))
60	57, 59	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ⊆ (Base‘𝐵))
61	24	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 = ((subringAlg ‘𝐸)‘𝑈))
62	61, 42	srabase 21494	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐵))
63	62	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘𝐸) = (Base‘𝐵))
64	60, 63	sseqtrrd 3950	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ⊆ (Base‘𝐸))
65	64	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑦 ⊆ (Base‘𝐸))
66		simplr 781	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑗 ∈ 𝑦)
67	65, 66	sseldd 3914	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑗 ∈ (Base‘𝐸))
68	33, 34, 36, 56, 67	ringcld 20526	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐸))
69		fedgmul.a	. . . . . . . . . . . . . . 15 ⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑉)
70	69	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝐸)‘𝑉))
71	7	simpld 500	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐸))
72	33	subrgss 20866	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
73	71, 72	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐸))
74	70, 73	srabase 21494	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐴))
75	74	ad4antr 745	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (Base‘𝐸) = (Base‘𝐴))
76	68, 75	eleqtrd 2866	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴))
77	76	anasss 472	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴))
78	77	ralrimivva 3209	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴))
79		oveq2 7457	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑗 → (𝑡(._r‘𝐸)𝑤) = (𝑡(._r‘𝐸)𝑗))
80		oveq1 7456	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑖 → (𝑡(._r‘𝐸)𝑗) = (𝑖(._r‘𝐸)𝑗))
81	79, 80	cbvmpov 7544	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) = (𝑗 ∈ 𝑦, 𝑖 ∈ 𝑥 ↦ (𝑖(._r‘𝐸)𝑗))
82	81	fmpo 8112	. . . . . . . . 9 ⊢ (∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴) ↔ (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴))
83	78, 82	sylib 221	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴))
84		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (Base‘(Scalar‘𝐵)) = (Base‘(Scalar‘𝐵))
85		eqid 2763	. . . . . . . . . . . . . 14 ⊢ ( ·_𝑠 ‘𝐵) = ( ·_𝑠 ‘𝐵)
86		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (+_g‘𝐵) = (+_g‘𝐵)
87		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (0_g‘(Scalar‘𝐵)) = (0_g‘(Scalar‘𝐵))
88	26	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐵 ∈ LVec)
89	88	ad5antr 747	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝐵 ∈ LVec)
90	27	lbslinds 22183	. . . . . . . . . . . . . . . 16 ⊢ (LBasis‘𝐵) ⊆ (LIndS‘𝐵)
91	90, 57	sselid 3911	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ∈ (LIndS‘𝐵))
92	91	ad5antr 747	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑦 ∈ (LIndS‘𝐵))
93	66	ad3antrrr 743	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑗 ∈ 𝑦)
94		simpllr 788	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑣 ∈ 𝑦)
95	61, 42	srasca 21497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ↾_s 𝑈) = (Scalar‘𝐵))
96	4, 95	eqtrid 2810	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 = (Scalar‘𝐵))
97	96	fveq2d 6918	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Base‘𝐹) = (Base‘(Scalar‘𝐵)))
98	97, 49	eqtr3d 2800	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Base‘(Scalar‘𝐵)) = (Base‘𝐶))
99	98	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘(Scalar‘𝐵)) = (Base‘𝐶))
100	40, 99	sseqtrrd 3950	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ⊆ (Base‘(Scalar‘𝐵)))
101	100	ad5antr 747	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑥 ⊆ (Base‘(Scalar‘𝐵)))
102		simp-4r 796	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑖 ∈ 𝑥)
103	101, 102	sseldd 3914	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑖 ∈ (Base‘(Scalar‘𝐵)))
104		simplr 781	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑢 ∈ 𝑥)
105	101, 104	sseldd 3914	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑢 ∈ (Base‘(Scalar‘𝐵)))
106	19	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐶 ∈ LVec)
107		eqid 2763	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (LSpan‘𝐶) = (LSpan‘𝐶)
108	38, 20, 107	islbs4 22182	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (LBasis‘𝐶) ↔ (𝑥 ∈ (LIndS‘𝐶) ∧ ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶)))
109	37, 108	sylib 221	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑥 ∈ (LIndS‘𝐶) ∧ ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶)))
110	109	simpld 500	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ∈ (LIndS‘𝐶))
111		eqid 2763	. . . . . . . . . . . . . . . . . . 19 ⊢ (0_g‘𝐶) = (0_g‘𝐶)
112	111	0nellinds 34023	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐶 ∈ LVec ∧ 𝑥 ∈ (LIndS‘𝐶)) → ¬ (0_g‘𝐶) ∈ 𝑥)
113	106, 110, 112	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ¬ (0_g‘𝐶) ∈ 𝑥)
114	113	ad5antr 747	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → ¬ (0_g‘𝐶) ∈ 𝑥)
115		nelne2 3057	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ 𝑥 ∧ ¬ (0_g‘𝐶) ∈ 𝑥) → 𝑖 ≠ (0_g‘𝐶))
116	102, 114, 115	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑖 ≠ (0_g‘𝐶))
117	96	fveq2d 6918	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0_g‘𝐹) = (0_g‘(Scalar‘𝐵)))
118	16, 1, 3	drgext0g 34326	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0_g‘𝐹) = (0_g‘𝐶))
119	117, 118	eqtr3d 2800	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0_g‘(Scalar‘𝐵)) = (0_g‘𝐶))
120	119	ad7antr 751	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (0_g‘(Scalar‘𝐵)) = (0_g‘𝐶))
121	116, 120	neeqtrrd 3033	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑖 ≠ (0_g‘(Scalar‘𝐵)))
122		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢))
123		ovexd 7484	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑖(._r‘𝐸)𝑗) ∈ V)
124	81	ovmpt4g 7597	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥 ∧ (𝑖(._r‘𝐸)𝑗) ∈ V) → (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑖(._r‘𝐸)𝑗))
125	93, 102, 123, 124	syl3anc 1399	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑖(._r‘𝐸)𝑗))
126	24, 23, 2	drgextvsca 34327	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (._r‘𝐸) = ( ·_𝑠 ‘𝐵))
127	126	oveqd 7466	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑖(._r‘𝐸)𝑗) = (𝑖( ·_𝑠 ‘𝐵)𝑗))
128	127	ad7antr 751	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑖(._r‘𝐸)𝑗) = (𝑖( ·_𝑠 ‘𝐵)𝑗))
129	125, 128	eqtrd 2798	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑖( ·_𝑠 ‘𝐵)𝑗))
130	81	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) = (𝑗 ∈ 𝑦, 𝑖 ∈ 𝑥 ↦ (𝑖(._r‘𝐸)𝑗)))
131		simprr 785	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)) → 𝑖 = 𝑢)
132		simprl 783	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)) → 𝑗 = 𝑣)
133	131, 132	oveq12d 7467	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)) → (𝑖(._r‘𝐸)𝑗) = (𝑢(._r‘𝐸)𝑣))
134		simplr 781	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → 𝑣 ∈ 𝑦)
135		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → 𝑢 ∈ 𝑥)
136		ovexd 7484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑢(._r‘𝐸)𝑣) ∈ V)
137	130, 133, 134, 135, 136	ovmpod 7602	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) = (𝑢(._r‘𝐸)𝑣))
138	137	adantllr 732	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) = (𝑢(._r‘𝐸)𝑣))
139	138	adantl3r 763	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) = (𝑢(._r‘𝐸)𝑣))
140	139	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) = (𝑢(._r‘𝐸)𝑣))
141	126	oveqd 7466	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑢(._r‘𝐸)𝑣) = (𝑢( ·_𝑠 ‘𝐵)𝑣))
142	141	ad7antr 751	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑢(._r‘𝐸)𝑣) = (𝑢( ·_𝑠 ‘𝐵)𝑣))
143	140, 142	eqtrd 2798	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) = (𝑢( ·_𝑠 ‘𝐵)𝑣))
144	122, 129, 143	3eqtr3d 2806	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑖( ·_𝑠 ‘𝐵)𝑗) = (𝑢( ·_𝑠 ‘𝐵)𝑣))
145	84, 85, 86, 87, 89, 92, 93, 94, 103, 105, 121, 144	linds2eq 34033	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢))
146	145	ex 418	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
147	146	anasss 472	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ (𝑣 ∈ 𝑦 ∧ 𝑢 ∈ 𝑥)) → ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
148	147	ralrimivva 3209	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → ∀𝑣 ∈ 𝑦 ∀𝑢 ∈ 𝑥 ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
149	148	anasss 472	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → ∀𝑣 ∈ 𝑦 ∀𝑢 ∈ 𝑥 ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
150	149	ralrimivva 3209	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 ∀𝑣 ∈ 𝑦 ∀𝑢 ∈ 𝑥 ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
151		f1opr 7505	. . . . . . . 8 ⊢ ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶1-1(Base‘𝐴) ↔ ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴) ∧ ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 ∀𝑣 ∈ 𝑦 ∀𝑢 ∈ 𝑥 ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢))))
152	83, 150, 151	sylanbrc 595	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶1-1(Base‘𝐴))
153	57, 37	xpexd 7795	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑦 × 𝑥) ∈ V)
154		f1rnen 33310	. . . . . . 7 ⊢ (((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶1-1(Base‘𝐴) ∧ (𝑦 × 𝑥) ∈ V) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ≈ (𝑦 × 𝑥))
155	152, 153, 154	syl2anc 596	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ≈ (𝑦 × 𝑥))
156		hasheni 14531	. . . . . 6 ⊢ (ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ≈ (𝑦 × 𝑥) → (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = (♯‘(𝑦 × 𝑥)))
157	155, 156	syl 18	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = (♯‘(𝑦 × 𝑥)))
158		hashxpe 33485	. . . . . 6 ⊢ ((𝑦 ∈ (LBasis‘𝐵) ∧ 𝑥 ∈ (LBasis‘𝐶)) → (♯‘(𝑦 × 𝑥)) = ((♯‘𝑦) ·_e (♯‘𝑥)))
159	57, 37, 158	syl2anc 596	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (♯‘(𝑦 × 𝑥)) = ((♯‘𝑦) ·_e (♯‘𝑥)))
160	157, 159	eqtrd 2798	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = ((♯‘𝑦) ·_e (♯‘𝑥)))
161	69, 12	sralvec 34321	. . . . . . 7 ⊢ ((𝐸 ∈ DivRing ∧ 𝐾 ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec)
162	23, 14, 71, 161	syl3anc 1399	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ LVec)
163	162	ad2antrr 739	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐴 ∈ LVec)
164	162	lveclmodd 21424	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ LMod)
165	164	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐴 ∈ LMod)
166	23	ad4antr 745	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝐸 ∈ DivRing)
167	1	ad4antr 745	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝐹 ∈ DivRing)
168	14	ad4antr 745	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝐾 ∈ DivRing)
169	2	ad4antr 745	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝑈 ∈ (SubRing‘𝐸))
170	3	ad4antr 745	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝑉 ∈ (SubRing‘𝐹))
171		fveq2 6914	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑗 → (𝑓‘𝑤) = (𝑓‘𝑗))
172	171	fveq1d 6916	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑗 → ((𝑓‘𝑤)‘𝑣) = ((𝑓‘𝑗)‘𝑣))
173		fveq2 6914	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑖 → ((𝑓‘𝑗)‘𝑣) = ((𝑓‘𝑗)‘𝑖))
174	172, 173	cbvmpov 7544	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) = (𝑗 ∈ 𝑦, 𝑖 ∈ 𝑥 ↦ ((𝑓‘𝑗)‘𝑖))
175		simp-4r 796	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝑥 ∈ (LBasis‘𝐶))
176		simpllr 788	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝑦 ∈ (LBasis‘𝐵))
177		simplr 781	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥))))
178		simpr 490	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴))
179	69, 24, 16, 4, 12, 166, 167, 168, 169, 170, 81, 174, 175, 176, 177, 178	fedgmullem2 34366	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝑐 = ((𝑦 × 𝑥) × {(0_g‘(Scalar‘𝐴))}))
180	179	ex 418	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) → ((𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0_g‘(Scalar‘𝐴))})))
181	180	ralrimiva 3158	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))((𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0_g‘(Scalar‘𝐴))})))
182		eqid 2763	. . . . . . . . 9 ⊢ (Base‘𝐴) = (Base‘𝐴)
183		eqid 2763	. . . . . . . . 9 ⊢ (Scalar‘𝐴) = (Scalar‘𝐴)
184		eqid 2763	. . . . . . . . 9 ⊢ ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘𝐴)
185		eqid 2763	. . . . . . . . 9 ⊢ (0_g‘𝐴) = (0_g‘𝐴)
186		eqid 2763	. . . . . . . . 9 ⊢ (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐴))
187		eqid 2763	. . . . . . . . 9 ⊢ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥))) = (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))
188	182, 183, 184, 185, 186, 187	islindf4 22188	. . . . . . . 8 ⊢ ((𝐴 ∈ LMod ∧ (𝑦 × 𝑥) ∈ V ∧ (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴)) → ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) LIndF 𝐴 ↔ ∀𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))((𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0_g‘(Scalar‘𝐴))}))))
189	188	biimpar 483	. . . . . . 7 ⊢ (((𝐴 ∈ LMod ∧ (𝑦 × 𝑥) ∈ V ∧ (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴)) ∧ ∀𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))((𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0_g‘(Scalar‘𝐴))}))) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) LIndF 𝐴)
190	165, 153, 83, 181, 189	syl31anc 1401	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) LIndF 𝐴)
191	68	anasss 472	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐸))
192	191	ralrimivva 3209	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐸))
193	81	rnmposs 7584	. . . . . . . . . 10 ⊢ (∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐸) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ⊆ (Base‘𝐸))
194	192, 193	syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ⊆ (Base‘𝐸))
195	74	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘𝐸) = (Base‘𝐴))
196	194, 195	sseqtrd 3949	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ⊆ (Base‘𝐴))
197		eqid 2763	. . . . . . . . 9 ⊢ (LSpan‘𝐴) = (LSpan‘𝐴)
198	182, 197	lspssv 21300	. . . . . . . 8 ⊢ ((𝐴 ∈ LMod ∧ ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ⊆ (Base‘𝐴)) → ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) ⊆ (Base‘𝐴))
199	165, 196, 198	syl2anc 596	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) ⊆ (Base‘𝐴))
200		simpl 488	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)))
201	200	ad4antr 745	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → ((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)))
202		elmapi 8905	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦) → 𝑎:𝑦⟶(Base‘(Scalar‘𝐵)))
203	202	ad4antlr 746	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → 𝑎:𝑦⟶(Base‘(Scalar‘𝐵)))
204		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → 𝑗 ∈ 𝑦)
205	203, 204	ffvelcdmd 7115	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → (𝑎‘𝑗) ∈ (Base‘(Scalar‘𝐵)))
206	109	simprd 501	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶))
207	201, 206	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶))
208	98	ad7antr 751	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → (Base‘(Scalar‘𝐵)) = (Base‘𝐶))
209	207, 208	eqtr4d 2801	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → ((LSpan‘𝐶)‘𝑥) = (Base‘(Scalar‘𝐵)))
210	205, 209	eleqtrrd 2867	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → (𝑎‘𝑗) ∈ ((LSpan‘𝐶)‘𝑥))
211		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
212		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (Scalar‘𝐶) = (Scalar‘𝐶)
213		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (0_g‘(Scalar‘𝐶)) = (0_g‘(Scalar‘𝐶))
214		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ ( ·_𝑠 ‘𝐶) = ( ·_𝑠 ‘𝐶)
215	19	lveclmodd 21424	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐶 ∈ LMod)
216	215	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐶 ∈ LMod)
217	107, 38, 211, 212, 213, 214, 216, 40	ellspds 34021	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((𝑎‘𝑗) ∈ ((LSpan‘𝐶)‘𝑥) ↔ ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))))
218	217	biimpa 482	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑎‘𝑗) ∈ ((LSpan‘𝐶)‘𝑥)) → ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
219	201, 210, 218	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
220	219	ralrimiva 3158	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) → ∀𝑗 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
221		fveq2 6914	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑗 → (𝑎‘𝑤) = (𝑎‘𝑗))
222		fveq2 6914	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑖 → (𝑏‘𝑣) = (𝑏‘𝑖))
223		id 23	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑖 → 𝑣 = 𝑖)
224	222, 223	oveq12d 7467	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = 𝑖 → ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣) = ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖))
225	224	cbvmptv 5213	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)) = (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖))
226	225	oveq2i 7460	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))
227	226	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑗 → (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))
228	221, 227	eqeq12d 2779	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑗 → ((𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) ↔ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
229	228	anbi2d 642	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑗 → ((𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) ↔ (𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))))
230	229	rexbidv 3190	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑗 → (∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) ↔ ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))))
231	230	cbvralvw 3244	. . . . . . . . . . . . . 14 ⊢ (∀𝑤 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) ↔ ∀𝑗 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
232		vex 3458	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
233		ovex 7482	. . . . . . . . . . . . . . 15 ⊢ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥) ∈ V
234		breq1 5109	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑓‘𝑤) → (𝑏 finSupp (0_g‘(Scalar‘𝐶)) ↔ (𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶))))
235		fveq1 6913	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (𝑓‘𝑤) → (𝑏‘𝑣) = ((𝑓‘𝑤)‘𝑣))
236	235	oveq1d 7464	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (𝑓‘𝑤) → ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣) = (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))
237	236	mpteq2dv 5203	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑓‘𝑤) → (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)) = (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))
238	237	oveq2d 7465	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑓‘𝑤) → (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))
239	238	eqeq2d 2774	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑓‘𝑤) → ((𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) ↔ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))))
240	234, 239	anbi12d 644	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑓‘𝑤) → ((𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) ↔ ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))))
241	240	ac6 10595	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ V ∧ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥) ∈ V ∧ ∀𝑤 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → ∃𝑓(𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))))
242	232, 233, 241	mp3an12 1481	. . . . . . . . . . . . . 14 ⊢ (∀𝑤 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) → ∃𝑓(𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))))
243	231, 242	sylbir 238	. . . . . . . . . . . . 13 ⊢ (∀𝑗 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))) → ∃𝑓(𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))))
244	220, 243	syl 18	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) → ∃𝑓(𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))))
245		fvexd 6929	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) → (Base‘(Scalar‘𝐴)) ∈ V)
246	153	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) → (𝑦 × 𝑥) ∈ V)
247		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥))
248		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑗 ∈ 𝑦)
249	247, 248	ffvelcdmd 7115	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (𝑓‘𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥))
250	249	elmaprd 8906	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (𝑓‘𝑗):𝑥⟶(Base‘(Scalar‘𝐶)))
251	250	anasss 472	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → (𝑓‘𝑗):𝑥⟶(Base‘(Scalar‘𝐶)))
252		simprr 785	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → 𝑖 ∈ 𝑥)
253	251, 252	ffvelcdmd 7115	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → ((𝑓‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐶)))
254	70, 73	srasca 21497	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐸 ↾_s 𝑉) = (Scalar‘𝐴))
255	12, 254	eqtrid 2810	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐴))
256	45, 48	srasca 21497	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) = (Scalar‘𝐶))
257	13, 256	eqtr3d 2800	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐶))
258	255, 257	eqtr3d 2800	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
259	258	fveq2d 6918	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
260	259	ad4antr 745	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
261	253, 260	eleqtrrd 2867	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → ((𝑓‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
262	261	ralrimivva 3209	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) → ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 ((𝑓‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
263	174	fmpo 8112	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 ((𝑓‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)) ↔ (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)):(𝑦 × 𝑥)⟶(Base‘(Scalar‘𝐴)))
264	262, 263	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) → (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)):(𝑦 × 𝑥)⟶(Base‘(Scalar‘𝐴)))
265	245, 246, 264	elmapdd 8897	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) → (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥)))
266	265	ad5ant15 771	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) → (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥)))
267	266	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥)))
268	267	adantl3r 763	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥)))
269		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) ∧ 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣))) → 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)))
270	269	breq1d 5116	. . . . . . . . . . . . . . 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‘𝐴))))
271	269	oveq1d 7464	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) ∧ 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣))) → (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))
272	271	oveq2d 7465	. . . . . . . . . . . . . . . 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‘𝐸)𝑤)))))
273	272	eqeq2d 2774	. . . . . . . . . . . . . . 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‘𝐸)𝑤))))))
274	270, 273	anbi12d 644	. . . . . . . . . . . . . 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‘𝐸)𝑤)))))))
275	23	ad8antr 753	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝐸 ∈ DivRing)
276	1	ad8antr 753	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝐹 ∈ DivRing)
277	14	ad8antr 753	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝐾 ∈ DivRing)
278	2	ad8antr 753	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑈 ∈ (SubRing‘𝐸))
279	3	ad8antr 753	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑉 ∈ (SubRing‘𝐹))
280	37	ad6antr 749	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑥 ∈ (LBasis‘𝐶))
281	57	ad6antr 749	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑦 ∈ (LBasis‘𝐵))
282		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ (Base‘𝐴))
283	282	ad5antr 747	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑧 ∈ (Base‘𝐴))
284	202	ad5antlr 748	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑎:𝑦⟶(Base‘(Scalar‘𝐵)))
285		simp-4r 796	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑎 finSupp (0_g‘(Scalar‘𝐵)))
286		simpllr 788	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤))))
287		id 23	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑗 → 𝑤 = 𝑗)
288	221, 287	oveq12d 7467	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑗 → ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤) = ((𝑎‘𝑗)( ·_𝑠 ‘𝐵)𝑗))
289	288	cbvmptv 5213	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)) = (𝑗 ∈ 𝑦 ↦ ((𝑎‘𝑗)( ·_𝑠 ‘𝐵)𝑗))
290	289	oveq2i 7460	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤))) = (𝐵 Σ_g (𝑗 ∈ 𝑦 ↦ ((𝑎‘𝑗)( ·_𝑠 ‘𝐵)𝑗)))
291	286, 290	eqtrdi 2814	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑧 = (𝐵 Σ_g (𝑗 ∈ 𝑦 ↦ ((𝑎‘𝑗)( ·_𝑠 ‘𝐵)𝑗))))
292		simplr 781	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥))
293	171	breq1d 5116	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑗 → ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ↔ (𝑓‘𝑗) finSupp (0_g‘(Scalar‘𝐶))))
294		fveq2 6914	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = 𝑖 → ((𝑓‘𝑤)‘𝑣) = ((𝑓‘𝑤)‘𝑖))
295	294, 223	oveq12d 7467	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 = 𝑖 → (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣) = (((𝑓‘𝑤)‘𝑖)( ·_𝑠 ‘𝐶)𝑖))
296	295	cbvmptv 5213	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)) = (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑖)( ·_𝑠 ‘𝐶)𝑖))
297	171	fveq1d 6916	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 𝑗 → ((𝑓‘𝑤)‘𝑖) = ((𝑓‘𝑗)‘𝑖))
298	297	oveq1d 7464	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 𝑗 → (((𝑓‘𝑤)‘𝑖)( ·_𝑠 ‘𝐶)𝑖) = (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖))
299	298	mpteq2dv 5203	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑗 → (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)) = (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))
300	296, 299	eqtrid 2810	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑗 → (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)) = (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))
301	300	oveq2d 7465	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑗 → (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))
302	221, 301	eqeq12d 2779	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑗 → ((𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) ↔ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
303	293, 302	anbi12d 644	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑗 → (((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) ↔ ((𝑓‘𝑗) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))))
304	303	cbvralvw 3244	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) ↔ ∀𝑗 ∈ 𝑦 ((𝑓‘𝑗) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
305	304	bilani 510	. . . . . . . . . . . . . . . . 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 (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
306	305	r19.21bi 3258	. . . . . . . . . . . . . . . 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 (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
307	306	simpld 500	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) ∧ 𝑗 ∈ 𝑦) → (𝑓‘𝑗) finSupp (0_g‘(Scalar‘𝐶)))
308	306	simprd 501	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) ∧ 𝑗 ∈ 𝑦) → (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))
309	69, 24, 16, 4, 12, 275, 276, 277, 278, 279, 81, 174, 280, 281, 283, 284, 285, 291, 292, 307, 308	fedgmullem1 34365	. . . . . . . . . . . . . 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‘𝐸)𝑤))))))
310	268, 274, 309	rspcedvd 3582	. . . . . . . . . . . . 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‘𝐸)𝑤))))))
311	310	anasss 472	. . . . . . . . . . . 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‘𝐸)𝑤))))))
312	244, 311	exlimddv 1970	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥))(𝑐 finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))))
313	312	anasss 472	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ (𝑎 finSupp (0_g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤))))) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥))(𝑐 finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))))
314		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (LSpan‘𝐵) = (LSpan‘𝐵)
315	58, 27, 314	islbs4 22182	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (LBasis‘𝐵) ↔ (𝑦 ∈ (LIndS‘𝐵) ∧ ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵)))
316	315	bilani 510	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑦 ∈ (LIndS‘𝐵) ∧ ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵)))
317	316	simprd 501	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵))
318	317	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵))
319	74, 62	eqtr3d 2800	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Base‘𝐴) = (Base‘𝐵))
320	319	ad3antrrr 743	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → (Base‘𝐴) = (Base‘𝐵))
321	318, 320	eqtr4d 2801	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((LSpan‘𝐵)‘𝑦) = (Base‘𝐴))
322	282, 321	eleqtrrd 2867	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ ((LSpan‘𝐵)‘𝑦))
323		eqid 2763	. . . . . . . . . . . . 13 ⊢ (Scalar‘𝐵) = (Scalar‘𝐵)
324	26	lveclmodd 21424	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ LMod)
325	324	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐵 ∈ LMod)
326	314, 58, 84, 323, 87, 85, 325, 60	ellspds 34021	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑧 ∈ ((LSpan‘𝐵)‘𝑦) ↔ ∃𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)(𝑎 finSupp (0_g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤))))))
327	326	biimpa 482	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ ((LSpan‘𝐵)‘𝑦)) → ∃𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)(𝑎 finSupp (0_g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))))
328	200, 322, 327	syl2anc 596	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ∃𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)(𝑎 finSupp (0_g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))))
329	313, 328	r19.29a 3174	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥))(𝑐 finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))))
330		eqid 2763	. . . . . . . . . . 11 ⊢ (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴))
331	197, 182, 330, 183, 186, 184, 83, 165, 153	ellspd 22152	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑧 ∈ ((LSpan‘𝐴)‘((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) “ (𝑦 × 𝑥))) ↔ ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥))(𝑐 finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))))))
332	331	adantr 486	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑧 ∈ ((LSpan‘𝐴)‘((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) “ (𝑦 × 𝑥))) ↔ ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥))(𝑐 finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))))))
333	329, 332	mpbird 260	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ ((LSpan‘𝐴)‘((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) “ (𝑦 × 𝑥))))
334	83	ffnd 6738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) Fn (𝑦 × 𝑥))
335	334	adantr 486	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) Fn (𝑦 × 𝑥))
336		fnima 6697	. . . . . . . . . 10 ⊢ ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) Fn (𝑦 × 𝑥) → ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) “ (𝑦 × 𝑥)) = ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))
337	335, 336	syl 18	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) “ (𝑦 × 𝑥)) = ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))
338	337	fveq2d 6918	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((LSpan‘𝐴)‘((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) “ (𝑦 × 𝑥))) = ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))
339	333, 338	eleqtrd 2866	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))
340	199, 339	eqelssd 3934	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = (Base‘𝐴))
341		eqid 2763	. . . . . . 7 ⊢ (Base‘(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = (Base‘(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))
342		drngnzr 21044	. . . . . . . . . 10 ⊢ (𝐾 ∈ DivRing → 𝐾 ∈ NzRing)
343	14, 342	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ NzRing)
344	255, 343	eqeltrrd 2865	. . . . . . . 8 ⊢ (𝜑 → (Scalar‘𝐴) ∈ NzRing)
345	344	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Scalar‘𝐴) ∈ NzRing)
346	182, 341, 183, 184, 185, 186, 197, 165, 345, 153, 152	lindflbs 34031	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ∈ (LBasis‘𝐴) ↔ ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) LIndF 𝐴 ∧ ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = (Base‘𝐴))))
347	190, 340, 346	mpbir2and 726	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ∈ (LBasis‘𝐴))
348		eqid 2763	. . . . . 6 ⊢ (LBasis‘𝐴) = (LBasis‘𝐴)
349	348	dimval 34337	. . . . 5 ⊢ ((𝐴 ∈ LVec ∧ ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ∈ (LBasis‘𝐴)) → (dim‘𝐴) = (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))
350	163, 347, 349	syl2anc 596	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐴) = (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))
351	27	dimval 34337	. . . . . 6 ⊢ ((𝐵 ∈ LVec ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐵) = (♯‘𝑦))
352	88, 57, 351	syl2anc 596	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐵) = (♯‘𝑦))
353	20	dimval 34337	. . . . . 6 ⊢ ((𝐶 ∈ LVec ∧ 𝑥 ∈ (LBasis‘𝐶)) → (dim‘𝐶) = (♯‘𝑥))
354	106, 37, 353	syl2anc 596	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐶) = (♯‘𝑥))
355	352, 354	oveq12d 7467	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((dim‘𝐵) ·_e (dim‘𝐶)) = ((♯‘𝑦) ·_e (♯‘𝑥)))
356	160, 350, 355	3eqtr4d 2808	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐴) = ((dim‘𝐵) ·_e (dim‘𝐶)))
357	32, 356	exlimddv 1970	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) → (dim‘𝐴) = ((dim‘𝐵) ·_e (dim‘𝐶)))
358	22, 357	n0limd 4304	1 ⊢ (𝜑 → (dim‘𝐴) = ((dim‘𝐵) ·_e (dim‘𝐶)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∃wex 1812 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 Vcvv 3454 ⊆ wss 3900 ∅c0 4281 {csn 4588 class class class wbr 5106 ↦ cmpt 5190 × cxp 5654 ran crn 5657 “ cima 5659 Fn wfn 6559 ⟶wf 6560 ⟶1-1wf1 6561 ‘cfv 6564 (class class class)co 7449 ∈ cmpo 7451 ∘_f cof 7721 ↑_m cmap 8883 ≈ cen 9006 finSupp cfsupp 9389 ·_e cxmu 13278 ♯chash 14513 Basecbs 17428 ↾_s cress 17449 +_gcplusg 17469 ._rcmulr 17470 Scalarcsca 17472 ·_𝑠 cvsca 17473 0_gc0g 17651 Σ_g cgsu 17652 Ringcrg 20501 NzRingcnzr 20804 SubRingcsubrg 20863 DivRingcdr 21022 LModclmod 21177 LSpanclspn 21288 LBasisclbs 21391 LVecclvec 21419 subringAlg csra 21488 freeLMod cfrlm 22096 LIndF clindf 22154 LIndSclinds 22155 dimcldim 34335

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7781 ax-inf2 9677 ax-ac2 10578 ax-cnex 11293 ax-resscn 11294 ax-1cn 11295 ax-icn 11296 ax-addcl 11297 ax-addrcl 11298 ax-mulcl 11299 ax-mulrcl 11300 ax-mulcom 11301 ax-addass 11302 ax-mulass 11303 ax-distr 11304 ax-i2m1 11305 ax-1ne0 11306 ax-1rid 11307 ax-rnegex 11308 ax-rrecex 11309 ax-cnre 11310 ax-pre-lttri 11311 ax-pre-lttrn 11312 ax-pre-ltadd 11313 ax-pre-mulgt0 11314

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-se 5610 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6328 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6518 df-fun 6566 df-fn 6567 df-f 6568 df-f1 6569 df-fo 6570 df-f1o 6571 df-fv 6572 df-isom 6573 df-riota 7406 df-ov 7452 df-oprab 7453 df-mpo 7454 df-of 7723 df-rpss 7769 df-om 7910 df-1st 8033 df-2nd 8034 df-supp 8213 df-tpos 8279 df-frecs 8335 df-wrecs 8366 df-recs 8415 df-rdg 8454 df-1o 8512 df-2o 8513 df-oadd 8516 df-er 8753 df-map 8885 df-ixp 8962 df-en 9010 df-dom 9011 df-sdom 9012 df-fin 9013 df-fsupp 9390 df-sup 9469 df-oi 9539 df-dju 10017 df-card 10055 df-acn 10058 df-ac 10232 df-pnf 11382 df-mnf 11383 df-xr 11384 df-ltxr 11385 df-le 11386 df-sub 11580 df-neg 11581 df-nn 12374 df-2 12443 df-3 12444 df-4 12445 df-5 12446 df-6 12447 df-7 12448 df-8 12449 df-9 12450 df-n0 12645 df-xnn0 12718 df-z 12732 df-dec 12853 df-uz 13004 df-xmul 13281 df-fz 13678 df-fzo 13827 df-seq 14183 df-hash 14514 df-struct 17366 df-sets 17383 df-slot 17401 df-ndx 17413 df-base 17429 df-ress 17450 df-plusg 17482 df-mulr 17483 df-sca 17485 df-vsca 17486 df-ip 17487 df-tset 17488 df-ple 17489 df-ocomp 17490 df-ds 17491 df-hom 17493 df-cco 17494 df-0g 17653 df-gsum 17654 df-prds 17659 df-pws 17661 df-mre 17797 df-mrc 17798 df-mri 17799 df-acs 17800 df-proset 18509 df-drs 18510 df-poset 18528 df-ipo 18743 df-mgm 18857 df-sgrp 18949 df-mnd 18965 df-mhm 19019 df-submnd 19020 df-grp 19188 df-minusg 19189 df-sbg 19190 df-mulg 19319 df-subg 19374 df-ghm 19469 df-cntz 19573 df-cmn 20038 df-abl 20039 df-mgp 20403 df-rng 20417 df-ur 20450 df-ring 20503 df-oppr 20609 df-dvdsr 20629 df-unit 20630 df-invr 20660 df-nzr 20805 df-subrng 20840 df-subrg 20864 df-drng 21024 df-lmod 21179 df-lss 21249 df-lsp 21289 df-lmhm 21339 df-lbs 21392 df-lvec 21420 df-sra 21490 df-rgmod 21491 df-dsmm 22082 df-frlm 22097 df-uvc 22133 df-lindf 22156 df-linds 22157 df-dim 34336

This theorem is used by: extdgmul 34399

W3C validator