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 34310

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 9590. (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 20856	. . . . . . . . . 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 17432	. . . . . . 7 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈) → ((𝐸 ↾_s 𝑈) ↾_s 𝑉) = (𝐸 ↾_s 𝑉))
10	2, 8, 9	syl2anc 596	. . . . . 6 ⊢ (𝜑 → ((𝐸 ↾_s 𝑈) ↾_s 𝑉) = (𝐸 ↾_s 𝑉))
11	4	oveq1i 7431	. . . . . 6 ⊢ (𝐹 ↾_s 𝑉) = ((𝐸 ↾_s 𝑈) ↾_s 𝑉)
12		fedgmul.k	. . . . . 6 ⊢ 𝐾 = (𝐸 ↾_s 𝑉)
13	10, 11, 12	3eqtr4g 2820	. . . . 5 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) = 𝐾)
14		fedgmul.3	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ DivRing)
15	13, 14	eqeltrd 2860	. . . 4 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) ∈ DivRing)
16		fedgmul.c	. . . . 5 ⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
17		eqid 2760	. . . . 5 ⊢ (𝐹 ↾_s 𝑉) = (𝐹 ↾_s 𝑉)
18	16, 17	sralvec 34264	. . . 4 ⊢ ((𝐹 ∈ DivRing ∧ (𝐹 ↾_s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
19	1, 15, 3, 18	syl3anc 1398	. . 3 ⊢ (𝜑 → 𝐶 ∈ LVec)
20		eqid 2760	. . . 4 ⊢ (LBasis‘𝐶) = (LBasis‘𝐶)
21	20	lbsex 21449	. . 3 ⊢ (𝐶 ∈ LVec → (LBasis‘𝐶) ≠ ∅)
22	19, 21	syl 18	. 2 ⊢ (𝜑 → (LBasis‘𝐶) ≠ ∅)
23		fedgmul.1	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ DivRing)
24		fedgmul.b	. . . . . . . 8 ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
25	24, 4	sralvec 34264	. . . . . . 7 ⊢ ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐵 ∈ LVec)
26	23, 1, 2, 25	syl3anc 1398	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ LVec)
27		eqid 2760	. . . . . . 7 ⊢ (LBasis‘𝐵) = (LBasis‘𝐵)
28	27	lbsex 21449	. . . . . 6 ⊢ (𝐵 ∈ LVec → (LBasis‘𝐵) ≠ ∅)
29	26, 28	syl 18	. . . . 5 ⊢ (𝜑 → (LBasis‘𝐵) ≠ ∅)
30		n0 4299	. . . . 5 ⊢ ((LBasis‘𝐵) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (LBasis‘𝐵))
31	29, 30	sylib 221	. . . 4 ⊢ (𝜑 → ∃𝑦 𝑦 ∈ (LBasis‘𝐵))
32	31	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) → ∃𝑦 𝑦 ∈ (LBasis‘𝐵))
33		eqid 2760	. . . . . . . . . . . . 13 ⊢ (Base‘𝐸) = (Base‘𝐸)
34		eqid 2760	. . . . . . . . . . . . 13 ⊢ (._r‘𝐸) = (._r‘𝐸)
35	23	drngringd 20994	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ∈ Ring)
36	35	ad4antr 745	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝐸 ∈ Ring)
37		simplr 781	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ∈ (LBasis‘𝐶))
38		eqid 2760	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝐶) = (Base‘𝐶)
39	38, 20	lbsss 21358	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (LBasis‘𝐶) → 𝑥 ⊆ (Base‘𝐶))
40	37, 39	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ⊆ (Base‘𝐶))
41	33	subrgss 20830	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
42	2, 41	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐸))
43	4, 33	ressbas2 17422	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
44	42, 43	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑈 = (Base‘𝐹))
45	16	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐶 = ((subringAlg ‘𝐹)‘𝑉))
46		eqid 2760	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Base‘𝐹) = (Base‘𝐹)
47	46	subrgss 20830	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
48	3, 47	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐹))
49	45, 48	srabase 21458	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Base‘𝐹) = (Base‘𝐶))
50	44, 49	eqtrd 2795	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 = (Base‘𝐶))
51	50, 42	eqsstrrd 3943	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
52	51	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘𝐶) ⊆ (Base‘𝐸))
53	40, 52	sstrd 3918	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ⊆ (Base‘𝐸))
54	53	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑥 ⊆ (Base‘𝐸))
55		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑖 ∈ 𝑥)
56	54, 55	sseldd 3909	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑖 ∈ (Base‘𝐸))
57		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ∈ (LBasis‘𝐵))
58		eqid 2760	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝐵) = (Base‘𝐵)
59	58, 27	lbsss 21358	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (LBasis‘𝐵) → 𝑦 ⊆ (Base‘𝐵))
60	57, 59	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ⊆ (Base‘𝐵))
61	24	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 = ((subringAlg ‘𝐸)‘𝑈))
62	61, 42	srabase 21458	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐵))
63	62	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘𝐸) = (Base‘𝐵))
64	60, 63	sseqtrrd 3945	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ⊆ (Base‘𝐸))
65	64	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑦 ⊆ (Base‘𝐸))
66		simplr 781	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑗 ∈ 𝑦)
67	65, 66	sseldd 3909	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑗 ∈ (Base‘𝐸))
68	33, 34, 36, 56, 67	ringcld 20490	. . . . . . . . . . . 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 20830	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
73	71, 72	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐸))
74	70, 73	srabase 21458	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐴))
75	74	ad4antr 745	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (Base‘𝐸) = (Base‘𝐴))
76	68, 75	eleqtrd 2862	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴))
77	76	anasss 472	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴))
78	77	ralrimivva 3205	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴))
79		oveq2 7429	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑗 → (𝑡(._r‘𝐸)𝑤) = (𝑡(._r‘𝐸)𝑗))
80		oveq1 7428	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑖 → (𝑡(._r‘𝐸)𝑗) = (𝑖(._r‘𝐸)𝑗))
81	79, 80	cbvmpov 7516	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) = (𝑗 ∈ 𝑦, 𝑖 ∈ 𝑥 ↦ (𝑖(._r‘𝐸)𝑗))
82	81	fmpo 8080	. . . . . . . . 9 ⊢ (∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴) ↔ (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴))
83	78, 82	sylib 221	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴))
84		eqid 2760	. . . . . . . . . . . . . 14 ⊢ (Base‘(Scalar‘𝐵)) = (Base‘(Scalar‘𝐵))
85		eqid 2760	. . . . . . . . . . . . . 14 ⊢ ( ·_𝑠 ‘𝐵) = ( ·_𝑠 ‘𝐵)
86		eqid 2760	. . . . . . . . . . . . . 14 ⊢ (+_g‘𝐵) = (+_g‘𝐵)
87		eqid 2760	. . . . . . . . . . . . . 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 22145	. . . . . . . . . . . . . . . 16 ⊢ (LBasis‘𝐵) ⊆ (LIndS‘𝐵)
91	90, 57	sselid 3906	. . . . . . . . . . . . . . 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 21461	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ↾_s 𝑈) = (Scalar‘𝐵))
96	4, 95	eqtrid 2807	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 = (Scalar‘𝐵))
97	96	fveq2d 6890	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Base‘𝐹) = (Base‘(Scalar‘𝐵)))
98	97, 49	eqtr3d 2797	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Base‘(Scalar‘𝐵)) = (Base‘𝐶))
99	98	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘(Scalar‘𝐵)) = (Base‘𝐶))
100	40, 99	sseqtrrd 3945	. . . . . . . . . . . . . . . 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 3909	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑖 ∈ (Base‘(Scalar‘𝐵)))
104		simplr 781	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑢 ∈ 𝑥)
105	101, 104	sseldd 3909	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑢 ∈ (Base‘(Scalar‘𝐵)))
106	19	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐶 ∈ LVec)
107		eqid 2760	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (LSpan‘𝐶) = (LSpan‘𝐶)
108	38, 20, 107	islbs4 22144	. . . . . . . . . . . . . . . . . . . 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 2760	. . . . . . . . . . . . . . . . . . 19 ⊢ (0_g‘𝐶) = (0_g‘𝐶)
112	111	0nellinds 33973	. . . . . . . . . . . . . . . . . 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 3053	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ 𝑥 ∧ ¬ (0_g‘𝐶) ∈ 𝑥) → 𝑖 ≠ (0_g‘𝐶))
116	102, 114, 115	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑖 ≠ (0_g‘𝐶))
117	96	fveq2d 6890	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0_g‘𝐹) = (0_g‘(Scalar‘𝐵)))
118	16, 1, 3	drgext0g 34269	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0_g‘𝐹) = (0_g‘𝐶))
119	117, 118	eqtr3d 2797	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0_g‘(Scalar‘𝐵)) = (0_g‘𝐶))
120	119	ad7antr 751	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (0_g‘(Scalar‘𝐵)) = (0_g‘𝐶))
121	116, 120	neeqtrrd 3029	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑖 ≠ (0_g‘(Scalar‘𝐵)))
122		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢))
123		ovexd 7456	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑖(._r‘𝐸)𝑗) ∈ V)
124	81	ovmpt4g 7568	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥 ∧ (𝑖(._r‘𝐸)𝑗) ∈ V) → (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑖(._r‘𝐸)𝑗))
125	93, 102, 123, 124	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑖(._r‘𝐸)𝑗))
126	24, 23, 2	drgextvsca 34270	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (._r‘𝐸) = ( ·_𝑠 ‘𝐵))
127	126	oveqd 7438	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑖(._r‘𝐸)𝑗) = (𝑖( ·_𝑠 ‘𝐵)𝑗))
128	127	ad7antr 751	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑖(._r‘𝐸)𝑗) = (𝑖( ·_𝑠 ‘𝐵)𝑗))
129	125, 128	eqtrd 2795	. . . . . . . . . . . . . . 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 7439	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)) → (𝑖(._r‘𝐸)𝑗) = (𝑢(._r‘𝐸)𝑣))
134		simplr 781	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → 𝑣 ∈ 𝑦)
135		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → 𝑢 ∈ 𝑥)
136		ovexd 7456	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑢(._r‘𝐸)𝑣) ∈ V)
137	130, 133, 134, 135, 136	ovmpod 7573	. . . . . . . . . . . . . . . . . . 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 7438	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑢(._r‘𝐸)𝑣) = (𝑢( ·_𝑠 ‘𝐵)𝑣))
142	141	ad7antr 751	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑢(._r‘𝐸)𝑣) = (𝑢( ·_𝑠 ‘𝐵)𝑣))
143	140, 142	eqtrd 2795	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) = (𝑢( ·_𝑠 ‘𝐵)𝑣))
144	122, 129, 143	3eqtr3d 2803	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑖( ·_𝑠 ‘𝐵)𝑗) = (𝑢( ·_𝑠 ‘𝐵)𝑣))
145	84, 85, 86, 87, 89, 92, 93, 94, 103, 105, 121, 144	linds2eq 33983	. . . . . . . . . . . . 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 3205	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → ∀𝑣 ∈ 𝑦 ∀𝑢 ∈ 𝑥 ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
149	148	anasss 472	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → ∀𝑣 ∈ 𝑦 ∀𝑢 ∈ 𝑥 ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
150	149	ralrimivva 3205	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 ∀𝑣 ∈ 𝑦 ∀𝑢 ∈ 𝑥 ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
151		f1opr 7477	. . . . . . . 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 7766	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑦 × 𝑥) ∈ V)
154		f1rnen 33270	. . . . . . 7 ⊢ (((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)–1-1→(Base‘𝐴) ∧ (𝑦 × 𝑥) ∈ V) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ≈ (𝑦 × 𝑥))
155	152, 153, 154	syl2anc 596	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ≈ (𝑦 × 𝑥))
156		hasheni 14496	. . . . . 6 ⊢ (ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ≈ (𝑦 × 𝑥) → (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = (♯‘(𝑦 × 𝑥)))
157	155, 156	syl 18	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = (♯‘(𝑦 × 𝑥)))
158		hashxpe 33446	. . . . . 6 ⊢ ((𝑦 ∈ (LBasis‘𝐵) ∧ 𝑥 ∈ (LBasis‘𝐶)) → (♯‘(𝑦 × 𝑥)) = ((♯‘𝑦) ·_e (♯‘𝑥)))
159	57, 37, 158	syl2anc 596	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (♯‘(𝑦 × 𝑥)) = ((♯‘𝑦) ·_e (♯‘𝑥)))
160	157, 159	eqtrd 2795	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = ((♯‘𝑦) ·_e (♯‘𝑥)))
161	69, 12	sralvec 34264	. . . . . . 7 ⊢ ((𝐸 ∈ DivRing ∧ 𝐾 ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec)
162	23, 14, 71, 161	syl3anc 1398	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ LVec)
163	162	ad2antrr 739	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐴 ∈ LVec)
164	162	lveclmodd 21388	. . . . . . . 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 6886	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑗 → (𝑓‘𝑤) = (𝑓‘𝑗))
172	171	fveq1d 6888	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑗 → ((𝑓‘𝑤)‘𝑣) = ((𝑓‘𝑗)‘𝑣))
173		fveq2 6886	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑖 → ((𝑓‘𝑗)‘𝑣) = ((𝑓‘𝑗)‘𝑖))
174	172, 173	cbvmpov 7516	. . . . . . . . . 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 34309	. . . . . . . . 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 3154	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))((𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0_g‘(Scalar‘𝐴))})))
182		eqid 2760	. . . . . . . . 9 ⊢ (Base‘𝐴) = (Base‘𝐴)
183		eqid 2760	. . . . . . . . 9 ⊢ (Scalar‘𝐴) = (Scalar‘𝐴)
184		eqid 2760	. . . . . . . . 9 ⊢ ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘𝐴)
185		eqid 2760	. . . . . . . . 9 ⊢ (0_g‘𝐴) = (0_g‘𝐴)
186		eqid 2760	. . . . . . . . 9 ⊢ (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐴))
187		eqid 2760	. . . . . . . . 9 ⊢ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥))) = (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))
188	182, 183, 184, 185, 186, 187	islindf4 22150	. . . . . . . 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 1400	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) LIndF 𝐴)
191	68	anasss 472	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐸))
192	191	ralrimivva 3205	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐸))
193	81	rnmposs 33315	. . . . . . . . . 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 3944	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ⊆ (Base‘𝐴))
197		eqid 2760	. . . . . . . . 9 ⊢ (LSpan‘𝐴) = (LSpan‘𝐴)
198	182, 197	lspssv 21264	. . . . . . . 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 8873	. . . . . . . . . . . . . . . . . 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 7086	. . . . . . . . . . . . . . . 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 2798	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → ((LSpan‘𝐶)‘𝑥) = (Base‘(Scalar‘𝐵)))
210	205, 209	eleqtrrd 2863	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → (𝑎‘𝑗) ∈ ((LSpan‘𝐶)‘𝑥))
211		eqid 2760	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
212		eqid 2760	. . . . . . . . . . . . . . . . 17 ⊢ (Scalar‘𝐶) = (Scalar‘𝐶)
213		eqid 2760	. . . . . . . . . . . . . . . . 17 ⊢ (0_g‘(Scalar‘𝐶)) = (0_g‘(Scalar‘𝐶))
214		eqid 2760	. . . . . . . . . . . . . . . . 17 ⊢ ( ·_𝑠 ‘𝐶) = ( ·_𝑠 ‘𝐶)
215	19	lveclmodd 21388	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐶 ∈ LMod)
216	215	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐶 ∈ LMod)
217	107, 38, 211, 212, 213, 214, 216, 40	ellspds 33971	. . . . . . . . . . . . . . . 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 3154	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) → ∀𝑗 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
221		fveq2 6886	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑗 → (𝑎‘𝑤) = (𝑎‘𝑗))
222		fveq2 6886	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑖 → (𝑏‘𝑣) = (𝑏‘𝑖))
223		id 23	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑖 → 𝑣 = 𝑖)
224	222, 223	oveq12d 7439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = 𝑖 → ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣) = ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖))
225	224	cbvmptv 5208	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)) = (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖))
226	225	oveq2i 7432	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))
227	226	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑗 → (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))
228	221, 227	eqeq12d 2776	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑗 → ((𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) ↔ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
229	228	anbi2d 642	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑗 → ((𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) ↔ (𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))))
230	229	rexbidv 3186	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑗 → (∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) ↔ ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))))
231	230	cbvralvw 3240	. . . . . . . . . . . . . 14 ⊢ (∀𝑤 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) ↔ ∀𝑗 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
232		vex 3454	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
233		ovex 7454	. . . . . . . . . . . . . . 15 ⊢ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥) ∈ V
234		breq1 5105	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑓‘𝑤) → (𝑏 finSupp (0_g‘(Scalar‘𝐶)) ↔ (𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶))))
235		fveq1 6885	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (𝑓‘𝑤) → (𝑏‘𝑣) = ((𝑓‘𝑤)‘𝑣))
236	235	oveq1d 7436	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (𝑓‘𝑤) → ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣) = (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))
237	236	mpteq2dv 5198	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑓‘𝑤) → (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)) = (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))
238	237	oveq2d 7437	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑓‘𝑤) → (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))
239	238	eqeq2d 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑓‘𝑤) → ((𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) ↔ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))))
240	234, 239	anbi12d 644	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑓‘𝑤) → ((𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) ↔ ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))))
241	240	ac6 10562	. . . . . . . . . . . . . . 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 1480	. . . . . . . . . . . . . 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 6901	. . . . . . . . . . . . . . . . . 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 7086	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (𝑓‘𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥))
250	249	elmaprd 8874	. . . . . . . . . . . . . . . . . . . . . . 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 7086	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → ((𝑓‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐶)))
254	70, 73	srasca 21461	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐸 ↾_s 𝑉) = (Scalar‘𝐴))
255	12, 254	eqtrid 2807	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐴))
256	45, 48	srasca 21461	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) = (Scalar‘𝐶))
257	13, 256	eqtr3d 2797	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐶))
258	255, 257	eqtr3d 2797	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
259	258	fveq2d 6890	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
260	259	ad4antr 745	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
261	253, 260	eleqtrrd 2863	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → ((𝑓‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
262	261	ralrimivva 3205	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) → ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 ((𝑓‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
263	174	fmpo 8080	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 ((𝑓‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)) ↔ (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)):(𝑦 × 𝑥)⟶(Base‘(Scalar‘𝐴)))
264	262, 263	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) → (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)):(𝑦 × 𝑥)⟶(Base‘(Scalar‘𝐴)))
265	245, 246, 264	elmapdd 8865	. . . . . . . . . . . . . . . . 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 5112	. . . . . . . . . . . . . . 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 7436	. . . . . . . . . . . . . . . . 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 7437	. . . . . . . . . . . . . . . 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 2771	. . . . . . . . . . . . . . 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 7439	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑗 → ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤) = ((𝑎‘𝑗)( ·_𝑠 ‘𝐵)𝑗))
289	288	cbvmptv 5208	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)) = (𝑗 ∈ 𝑦 ↦ ((𝑎‘𝑗)( ·_𝑠 ‘𝐵)𝑗))
290	289	oveq2i 7432	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤))) = (𝐵 Σ_g (𝑗 ∈ 𝑦 ↦ ((𝑎‘𝑗)( ·_𝑠 ‘𝐵)𝑗)))
291	286, 290	eqtrdi 2811	. . . . . . . . . . . . . . 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 5112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑗 → ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ↔ (𝑓‘𝑗) finSupp (0_g‘(Scalar‘𝐶))))
294		fveq2 6886	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = 𝑖 → ((𝑓‘𝑤)‘𝑣) = ((𝑓‘𝑤)‘𝑖))
295	294, 223	oveq12d 7439	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 = 𝑖 → (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣) = (((𝑓‘𝑤)‘𝑖)( ·_𝑠 ‘𝐶)𝑖))
296	295	cbvmptv 5208	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)) = (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑖)( ·_𝑠 ‘𝐶)𝑖))
297	171	fveq1d 6888	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 𝑗 → ((𝑓‘𝑤)‘𝑖) = ((𝑓‘𝑗)‘𝑖))
298	297	oveq1d 7436	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 𝑗 → (((𝑓‘𝑤)‘𝑖)( ·_𝑠 ‘𝐶)𝑖) = (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖))
299	298	mpteq2dv 5198	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑗 → (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)) = (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))
300	296, 299	eqtrid 2807	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑗 → (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)) = (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))
301	300	oveq2d 7437	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑗 → (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))
302	221, 301	eqeq12d 2776	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑗 → ((𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) ↔ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
303	293, 302	anbi12d 644	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑗 → (((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) ↔ ((𝑓‘𝑗) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))))
304	303	cbvralvw 3240	. . . . . . . . . . . . . . . . . 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 3254	. . . . . . . . . . . . . . . 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 34308	. . . . . . . . . . . . . 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 3578	. . . . . . . . . . . . 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 1967	. . . . . . . . . . 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 2760	. . . . . . . . . . . . . . . . 17 ⊢ (LSpan‘𝐵) = (LSpan‘𝐵)
315	58, 27, 314	islbs4 22144	. . . . . . . . . . . . . . . 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 2797	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Base‘𝐴) = (Base‘𝐵))
320	319	ad3antrrr 743	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → (Base‘𝐴) = (Base‘𝐵))
321	318, 320	eqtr4d 2798	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((LSpan‘𝐵)‘𝑦) = (Base‘𝐴))
322	282, 321	eleqtrrd 2863	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ ((LSpan‘𝐵)‘𝑦))
323		eqid 2760	. . . . . . . . . . . . 13 ⊢ (Scalar‘𝐵) = (Scalar‘𝐵)
324	26	lveclmodd 21388	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ LMod)
325	324	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐵 ∈ LMod)
326	314, 58, 84, 323, 87, 85, 325, 60	ellspds 33971	. . . . . . . . . . . 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 3170	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥))(𝑐 finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))))
330		eqid 2760	. . . . . . . . . . 11 ⊢ (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴))
331	197, 182, 330, 183, 186, 184, 83, 165, 153	ellspd 22114	. . . . . . . . . 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 6711	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) Fn (𝑦 × 𝑥))
335	334	adantr 486	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) Fn (𝑦 × 𝑥))
336		fnima 6670	. . . . . . . . . 10 ⊢ ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) Fn (𝑦 × 𝑥) → ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) “ (𝑦 × 𝑥)) = ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))
337	335, 336	syl 18	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) “ (𝑦 × 𝑥)) = ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))
338	337	fveq2d 6890	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((LSpan‘𝐴)‘((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) “ (𝑦 × 𝑥))) = ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))
339	333, 338	eleqtrd 2862	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))
340	199, 339	eqelssd 3929	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = (Base‘𝐴))
341		eqid 2760	. . . . . . 7 ⊢ (Base‘(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = (Base‘(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))
342		drngnzr 21008	. . . . . . . . . 10 ⊢ (𝐾 ∈ DivRing → 𝐾 ∈ NzRing)
343	14, 342	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ NzRing)
344	255, 343	eqeltrrd 2861	. . . . . . . 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 33981	. . . . . 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 2760	. . . . . 6 ⊢ (LBasis‘𝐴) = (LBasis‘𝐴)
349	348	dimval 34280	. . . . 5 ⊢ ((𝐴 ∈ LVec ∧ ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ∈ (LBasis‘𝐴)) → (dim‘𝐴) = (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))
350	163, 347, 349	syl2anc 596	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐴) = (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))
351	27	dimval 34280	. . . . . 6 ⊢ ((𝐵 ∈ LVec ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐵) = (♯‘𝑦))
352	88, 57, 351	syl2anc 596	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐵) = (♯‘𝑦))
353	20	dimval 34280	. . . . . 6 ⊢ ((𝐶 ∈ LVec ∧ 𝑥 ∈ (LBasis‘𝐶)) → (dim‘𝐶) = (♯‘𝑥))
354	106, 37, 353	syl2anc 596	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐶) = (♯‘𝑥))
355	352, 354	oveq12d 7439	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((dim‘𝐵) ·_e (dim‘𝐶)) = ((♯‘𝑦) ·_e (♯‘𝑥)))
356	160, 350, 355	3eqtr4d 2805	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐴) = ((dim‘𝐵) ·_e (dim‘𝐶)))
357	32, 356	exlimddv 1967	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) → (dim‘𝐴) = ((dim‘𝐵) ·_e (dim‘𝐶)))
358	22, 357	n0limd 4300	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 1569 ∃wex 1811 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 Vcvv 3450 ⊆ wss 3895 ∅c0 4278 {csn 4584 class class class wbr 5102 ↦ cmpt 5185 × cxp 5648 ran crn 5651 “ cima 5653 Fn wfn 6534 ⟶wf 6535 –1-1→wf1 6536 ‘cfv 6539 (class class class)co 7421 ∈ cmpo 7423 ∘_f cof 7692 ↑_m cmap 8851 ≈ cen 8974 finSupp cfsupp 9357 ·_e cxmu 13244 ♯chash 14478 Basecbs 17393 ↾_s cress 17414 +_gcplusg 17434 ._rcmulr 17435 Scalarcsca 17437 ·_𝑠 cvsca 17438 0_gc0g 17616 Σ_g cgsu 17617 Ringcrg 20465 NzRingcnzr 20768 SubRingcsubrg 20827 DivRingcdr 20986 LModclmod 21141 LSpanclspn 21252 LBasisclbs 21355 LVecclvec 21383 subringAlg csra 21452 freeLMod cfrlm 22058 LIndF clindf 22116 LIndSclinds 22117 dimcldim 34278

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752 ax-inf2 9646 ax-ac2 10545 ax-cnex 11260 ax-resscn 11261 ax-1cn 11262 ax-icn 11263 ax-addcl 11264 ax-addrcl 11265 ax-mulcl 11266 ax-mulrcl 11267 ax-mulcom 11268 ax-addass 11269 ax-mulass 11270 ax-distr 11271 ax-i2m1 11272 ax-1ne0 11273 ax-1rid 11274 ax-rnegex 11275 ax-rrecex 11276 ax-cnre 11277 ax-pre-lttri 11278 ax-pre-lttrn 11279 ax-pre-ltadd 11280 ax-pre-mulgt0 11281

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-isom 6548 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-of 7694 df-rpss 7740 df-om 7879 df-1st 8002 df-2nd 8003 df-supp 8181 df-tpos 8247 df-frecs 8303 df-wrecs 8334 df-recs 8383 df-rdg 8422 df-1o 8480 df-2o 8481 df-oadd 8484 df-er 8721 df-map 8853 df-ixp 8930 df-en 8978 df-dom 8979 df-sdom 8980 df-fin 8981 df-fsupp 9358 df-sup 9438 df-oi 9508 df-dju 9986 df-card 10024 df-acn 10027 df-ac 10199 df-pnf 11349 df-mnf 11350 df-xr 11351 df-ltxr 11352 df-le 11353 df-sub 11547 df-neg 11548 df-nn 12340 df-2 12409 df-3 12410 df-4 12411 df-5 12412 df-6 12413 df-7 12414 df-8 12415 df-9 12416 df-n0 12611 df-xnn0 12684 df-z 12698 df-dec 12819 df-uz 12970 df-xmul 13247 df-fz 13644 df-fzo 13793 df-seq 14149 df-hash 14479 df-struct 17331 df-sets 17348 df-slot 17366 df-ndx 17378 df-base 17394 df-ress 17415 df-plusg 17447 df-mulr 17448 df-sca 17450 df-vsca 17451 df-ip 17452 df-tset 17453 df-ple 17454 df-ocomp 17455 df-ds 17456 df-hom 17458 df-cco 17459 df-0g 17618 df-gsum 17619 df-prds 17624 df-pws 17626 df-mre 17762 df-mrc 17763 df-mri 17764 df-acs 17765 df-proset 18474 df-drs 18475 df-poset 18493 df-ipo 18708 df-mgm 18822 df-sgrp 18914 df-mnd 18930 df-mhm 18984 df-submnd 18985 df-grp 19153 df-minusg 19154 df-sbg 19155 df-mulg 19284 df-subg 19339 df-ghm 19434 df-cntz 19537 df-cmn 20002 df-abl 20003 df-mgp 20367 df-rng 20381 df-ur 20414 df-ring 20467 df-oppr 20573 df-dvdsr 20593 df-unit 20594 df-invr 20624 df-nzr 20769 df-subrng 20804 df-subrg 20828 df-drng 20988 df-lmod 21143 df-lss 21213 df-lsp 21253 df-lmhm 21303 df-lbs 21356 df-lvec 21384 df-sra 21454 df-rgmod 21455 df-dsmm 22044 df-frlm 22059 df-uvc 22095 df-lindf 22118 df-linds 22119 df-dim 34279

This theorem is used by: extdgmul 34342

W3C validator