Theorem fedgmul 33808

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

Hypotheses

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

Assertion

Ref	Expression
fedgmul	⊢ (𝜑 → (dim‘𝐴) = ((dim‘𝐵) ·e (dim‘𝐶)))

Proof of Theorem fedgmul

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

Step	Hyp	Ref	Expression
1		fedgmul.2	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ DivRing)
2		fedgmul.4	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸))
3		fedgmul.5	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐹))
4		fedgmul.f	. . . . . . . . . . . 12 ⊢ 𝐹 = (𝐸 ↾s 𝑈)
5	4	subsubrg 20543	. . . . . . . . . . 11 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (𝑉 ∈ (SubRing‘𝐹) ↔ (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈)))
6	5	biimpa 476	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ∈ (SubRing‘𝐹)) → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))
7	2, 3, 6	syl2anc 585	. . . . . . . . 9 ⊢ (𝜑 → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))
8	7	simprd 495	. . . . . . . 8 ⊢ (𝜑 → 𝑉 ⊆ 𝑈)
9		ressabs 17187	. . . . . . . 8 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈) → ((𝐸 ↾s 𝑈) ↾s 𝑉) = (𝐸 ↾s 𝑉))
10	2, 8, 9	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → ((𝐸 ↾s 𝑈) ↾s 𝑉) = (𝐸 ↾s 𝑉))
11	4	oveq1i 7378	. . . . . . 7 ⊢ (𝐹 ↾s 𝑉) = ((𝐸 ↾s 𝑈) ↾s 𝑉)
12		fedgmul.k	. . . . . . 7 ⊢ 𝐾 = (𝐸 ↾s 𝑉)
13	10, 11, 12	3eqtr4g 2797	. . . . . 6 ⊢ (𝜑 → (𝐹 ↾s 𝑉) = 𝐾)
14		fedgmul.3	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ DivRing)
15	13, 14	eqeltrd 2837	. . . . 5 ⊢ (𝜑 → (𝐹 ↾s 𝑉) ∈ DivRing)
16		fedgmul.c	. . . . . 6 ⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
17		eqid 2737	. . . . . 6 ⊢ (𝐹 ↾s 𝑉) = (𝐹 ↾s 𝑉)
18	16, 17	sralvec 33761	. . . . 5 ⊢ ((𝐹 ∈ DivRing ∧ (𝐹 ↾s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
19	1, 15, 3, 18	syl3anc 1374	. . . 4 ⊢ (𝜑 → 𝐶 ∈ LVec)
20		eqid 2737	. . . . 5 ⊢ (LBasis‘𝐶) = (LBasis‘𝐶)
21	20	lbsex 21132	. . . 4 ⊢ (𝐶 ∈ LVec → (LBasis‘𝐶) ≠ ∅)
22	19, 21	syl 17	. . 3 ⊢ (𝜑 → (LBasis‘𝐶) ≠ ∅)
23		n0 4307	. . 3 ⊢ ((LBasis‘𝐶) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (LBasis‘𝐶))
24	22, 23	sylib 218	. 2 ⊢ (𝜑 → ∃𝑥 𝑥 ∈ (LBasis‘𝐶))
25		fedgmul.1	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ DivRing)
26		fedgmul.b	. . . . . . . 8 ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
27	26, 4	sralvec 33761	. . . . . . 7 ⊢ ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐵 ∈ LVec)
28	25, 1, 2, 27	syl3anc 1374	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ LVec)
29		eqid 2737	. . . . . . 7 ⊢ (LBasis‘𝐵) = (LBasis‘𝐵)
30	29	lbsex 21132	. . . . . 6 ⊢ (𝐵 ∈ LVec → (LBasis‘𝐵) ≠ ∅)
31	28, 30	syl 17	. . . . 5 ⊢ (𝜑 → (LBasis‘𝐵) ≠ ∅)
32		n0 4307	. . . . 5 ⊢ ((LBasis‘𝐵) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (LBasis‘𝐵))
33	31, 32	sylib 218	. . . 4 ⊢ (𝜑 → ∃𝑦 𝑦 ∈ (LBasis‘𝐵))
34	33	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) → ∃𝑦 𝑦 ∈ (LBasis‘𝐵))
35		drngring 20681	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
36	25, 35	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ∈ Ring)
37	36	ad4antr 733	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝐸 ∈ Ring)
38		simplr 769	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ∈ (LBasis‘𝐶))
39		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝐶) = (Base‘𝐶)
40	39, 20	lbsss 21041	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (LBasis‘𝐶) → 𝑥 ⊆ (Base‘𝐶))
41	38, 40	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ⊆ (Base‘𝐶))
42		eqid 2737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Base‘𝐸) = (Base‘𝐸)
43	42	subrgss 20517	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
44	2, 43	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐸))
45	4, 42	ressbas2 17177	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
46	44, 45	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑈 = (Base‘𝐹))
47	16	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐶 = ((subringAlg ‘𝐹)‘𝑉))
48		eqid 2737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Base‘𝐹) = (Base‘𝐹)
49	48	subrgss 20517	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
50	3, 49	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐹))
51	47, 50	srabase 21141	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Base‘𝐹) = (Base‘𝐶))
52	46, 51	eqtrd 2772	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 = (Base‘𝐶))
53	52, 44	eqsstrrd 3971	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
54	53	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘𝐶) ⊆ (Base‘𝐸))
55	41, 54	sstrd 3946	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ⊆ (Base‘𝐸))
56	55	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑥 ⊆ (Base‘𝐸))
57		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑖 ∈ 𝑥)
58	56, 57	sseldd 3936	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑖 ∈ (Base‘𝐸))
59		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ∈ (LBasis‘𝐵))
60		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝐵) = (Base‘𝐵)
61	60, 29	lbsss 21041	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (LBasis‘𝐵) → 𝑦 ⊆ (Base‘𝐵))
62	59, 61	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ⊆ (Base‘𝐵))
63	26	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 = ((subringAlg ‘𝐸)‘𝑈))
64	63, 44	srabase 21141	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐵))
65	64	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘𝐸) = (Base‘𝐵))
66	62, 65	sseqtrrd 3973	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ⊆ (Base‘𝐸))
67	66	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑦 ⊆ (Base‘𝐸))
68		simplr 769	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑗 ∈ 𝑦)
69	67, 68	sseldd 3936	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑗 ∈ (Base‘𝐸))
70		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (.r‘𝐸) = (.r‘𝐸)
71	42, 70	ringcl 20197	. . . . . . . . . . . . 13 ⊢ ((𝐸 ∈ Ring ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸)) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐸))
72	37, 58, 69, 71	syl3anc 1374	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐸))
73		fedgmul.a	. . . . . . . . . . . . . . 15 ⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑉)
74	73	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝐸)‘𝑉))
75	7	simpld 494	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐸))
76	42	subrgss 20517	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
77	75, 76	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐸))
78	74, 77	srabase 21141	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐴))
79	78	ad4antr 733	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (Base‘𝐸) = (Base‘𝐴))
80	72, 79	eleqtrd 2839	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴))
81	80	anasss 466	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴))
82	81	ralrimivva 3181	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴))
83		oveq2 7376	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑗 → (𝑡(.r‘𝐸)𝑤) = (𝑡(.r‘𝐸)𝑗))
84		oveq1 7375	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑖 → (𝑡(.r‘𝐸)𝑗) = (𝑖(.r‘𝐸)𝑗))
85	83, 84	cbvmpov 7463	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) = (𝑗 ∈ 𝑦, 𝑖 ∈ 𝑥 ↦ (𝑖(.r‘𝐸)𝑗))
86	85	fmpo 8022	. . . . . . . . 9 ⊢ (∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴) ↔ (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴))
87	82, 86	sylib 218	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴))
88		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (Base‘(Scalar‘𝐵)) = (Base‘(Scalar‘𝐵))
89		eqid 2737	. . . . . . . . . . . . . 14 ⊢ ( ·𝑠 ‘𝐵) = ( ·𝑠 ‘𝐵)
90		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (+g‘𝐵) = (+g‘𝐵)
91		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (0g‘(Scalar‘𝐵)) = (0g‘(Scalar‘𝐵))
92	28	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐵 ∈ LVec)
93	92	ad5antr 735	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → 𝐵 ∈ LVec)
94	29	lbslinds 21800	. . . . . . . . . . . . . . . 16 ⊢ (LBasis‘𝐵) ⊆ (LIndS‘𝐵)
95	94, 59	sselid 3933	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ∈ (LIndS‘𝐵))
96	95	ad5antr 735	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → 𝑦 ∈ (LIndS‘𝐵))
97	68	ad3antrrr 731	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → 𝑗 ∈ 𝑦)
98		simpllr 776	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → 𝑣 ∈ 𝑦)
99	63, 44	srasca 21144	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ↾s 𝑈) = (Scalar‘𝐵))
100	4, 99	eqtrid 2784	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 = (Scalar‘𝐵))
101	100	fveq2d 6846	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Base‘𝐹) = (Base‘(Scalar‘𝐵)))
102	101, 51	eqtr3d 2774	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Base‘(Scalar‘𝐵)) = (Base‘𝐶))
103	102	ad2antrr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘(Scalar‘𝐵)) = (Base‘𝐶))
104	41, 103	sseqtrrd 3973	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ⊆ (Base‘(Scalar‘𝐵)))
105	104	ad5antr 735	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → 𝑥 ⊆ (Base‘(Scalar‘𝐵)))
106		simp-4r 784	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → 𝑖 ∈ 𝑥)
107	105, 106	sseldd 3936	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → 𝑖 ∈ (Base‘(Scalar‘𝐵)))
108		simplr 769	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → 𝑢 ∈ 𝑥)
109	105, 108	sseldd 3936	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → 𝑢 ∈ (Base‘(Scalar‘𝐵)))
110	19	ad2antrr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐶 ∈ LVec)
111		eqid 2737	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (LSpan‘𝐶) = (LSpan‘𝐶)
112	39, 20, 111	islbs4 21799	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (LBasis‘𝐶) ↔ (𝑥 ∈ (LIndS‘𝐶) ∧ ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶)))
113	38, 112	sylib 218	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑥 ∈ (LIndS‘𝐶) ∧ ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶)))
114	113	simpld 494	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ∈ (LIndS‘𝐶))
115		eqid 2737	. . . . . . . . . . . . . . . . . . 19 ⊢ (0g‘𝐶) = (0g‘𝐶)
116	115	0nellinds 33462	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐶 ∈ LVec ∧ 𝑥 ∈ (LIndS‘𝐶)) → ¬ (0g‘𝐶) ∈ 𝑥)
117	110, 114, 116	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ¬ (0g‘𝐶) ∈ 𝑥)
118	117	ad5antr 735	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → ¬ (0g‘𝐶) ∈ 𝑥)
119		nelne2 3031	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ 𝑥 ∧ ¬ (0g‘𝐶) ∈ 𝑥) → 𝑖 ≠ (0g‘𝐶))
120	106, 118, 119	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → 𝑖 ≠ (0g‘𝐶))
121	100	fveq2d 6846	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0g‘𝐹) = (0g‘(Scalar‘𝐵)))
122	16, 1, 3	drgext0g 33766	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0g‘𝐹) = (0g‘𝐶))
123	121, 122	eqtr3d 2774	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0g‘(Scalar‘𝐵)) = (0g‘𝐶))
124	123	ad7antr 739	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → (0g‘(Scalar‘𝐵)) = (0g‘𝐶))
125	120, 124	neeqtrrd 3007	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → 𝑖 ≠ (0g‘(Scalar‘𝐵)))
126		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢))
127		ovexd 7403	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → (𝑖(.r‘𝐸)𝑗) ∈ V)
128	85	ovmpt4g 7515	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥 ∧ (𝑖(.r‘𝐸)𝑗) ∈ V) → (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑖(.r‘𝐸)𝑗))
129	97, 106, 127, 128	syl3anc 1374	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑖(.r‘𝐸)𝑗))
130	26, 25, 2	drgextvsca 33767	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (.r‘𝐸) = ( ·𝑠 ‘𝐵))
131	130	oveqd 7385	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑖(.r‘𝐸)𝑗) = (𝑖( ·𝑠 ‘𝐵)𝑗))
132	131	ad7antr 739	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → (𝑖(.r‘𝐸)𝑗) = (𝑖( ·𝑠 ‘𝐵)𝑗))
133	129, 132	eqtrd 2772	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑖( ·𝑠 ‘𝐵)𝑗))
134	85	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) = (𝑗 ∈ 𝑦, 𝑖 ∈ 𝑥 ↦ (𝑖(.r‘𝐸)𝑗)))
135		simprr 773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)) → 𝑖 = 𝑢)
136		simprl 771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)) → 𝑗 = 𝑣)
137	135, 136	oveq12d 7386	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)) → (𝑖(.r‘𝐸)𝑗) = (𝑢(.r‘𝐸)𝑣))
138		simplr 769	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → 𝑣 ∈ 𝑦)
139		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → 𝑢 ∈ 𝑥)
140		ovexd 7403	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑢(.r‘𝐸)𝑣) ∈ V)
141	134, 137, 138, 139, 140	ovmpod 7520	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢) = (𝑢(.r‘𝐸)𝑣))
142	141	adantllr 720	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢) = (𝑢(.r‘𝐸)𝑣))
143	142	adantl3r 751	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢) = (𝑢(.r‘𝐸)𝑣))
144	143	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢) = (𝑢(.r‘𝐸)𝑣))
145	130	oveqd 7385	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑢(.r‘𝐸)𝑣) = (𝑢( ·𝑠 ‘𝐵)𝑣))
146	145	ad7antr 739	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → (𝑢(.r‘𝐸)𝑣) = (𝑢( ·𝑠 ‘𝐵)𝑣))
147	144, 146	eqtrd 2772	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢) = (𝑢( ·𝑠 ‘𝐵)𝑣))
148	126, 133, 147	3eqtr3d 2780	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → (𝑖( ·𝑠 ‘𝐵)𝑗) = (𝑢( ·𝑠 ‘𝐵)𝑣))
149	88, 89, 90, 91, 93, 96, 97, 98, 107, 109, 125, 148	linds2eq 33473	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢))
150	149	ex 412	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
151	150	anasss 466	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ (𝑣 ∈ 𝑦 ∧ 𝑢 ∈ 𝑥)) → ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
152	151	ralrimivva 3181	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → ∀𝑣 ∈ 𝑦 ∀𝑢 ∈ 𝑥 ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
153	152	anasss 466	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → ∀𝑣 ∈ 𝑦 ∀𝑢 ∈ 𝑥 ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
154	153	ralrimivva 3181	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 ∀𝑣 ∈ 𝑦 ∀𝑢 ∈ 𝑥 ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
155		f1opr 7424	. . . . . . . 8 ⊢ ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)):(𝑦 × 𝑥)–1-1→(Base‘𝐴) ↔ ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴) ∧ ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 ∀𝑣 ∈ 𝑦 ∀𝑢 ∈ 𝑥 ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢))))
156	87, 154, 155	sylanbrc 584	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)):(𝑦 × 𝑥)–1-1→(Base‘𝐴))
157	59, 38	xpexd 7706	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑦 × 𝑥) ∈ V)
158		f1rnen 32717	. . . . . . 7 ⊢ (((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)):(𝑦 × 𝑥)–1-1→(Base‘𝐴) ∧ (𝑦 × 𝑥) ∈ V) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) ≈ (𝑦 × 𝑥))
159	156, 157, 158	syl2anc 585	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) ≈ (𝑦 × 𝑥))
160		hasheni 14283	. . . . . 6 ⊢ (ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) ≈ (𝑦 × 𝑥) → (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))) = (♯‘(𝑦 × 𝑥)))
161	159, 160	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))) = (♯‘(𝑦 × 𝑥)))
162		hashxpe 32897	. . . . . 6 ⊢ ((𝑦 ∈ (LBasis‘𝐵) ∧ 𝑥 ∈ (LBasis‘𝐶)) → (♯‘(𝑦 × 𝑥)) = ((♯‘𝑦) ·e (♯‘𝑥)))
163	59, 38, 162	syl2anc 585	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (♯‘(𝑦 × 𝑥)) = ((♯‘𝑦) ·e (♯‘𝑥)))
164	161, 163	eqtrd 2772	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))) = ((♯‘𝑦) ·e (♯‘𝑥)))
165	73, 12	sralvec 33761	. . . . . . 7 ⊢ ((𝐸 ∈ DivRing ∧ 𝐾 ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec)
166	25, 14, 75, 165	syl3anc 1374	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ LVec)
167	166	ad2antrr 727	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐴 ∈ LVec)
168		lveclmod 21070	. . . . . . . . 9 ⊢ (𝐴 ∈ LVec → 𝐴 ∈ LMod)
169	166, 168	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ LMod)
170	169	ad2antrr 727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐴 ∈ LMod)
171	25	ad4antr 733	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴)) → 𝐸 ∈ DivRing)
172	1	ad4antr 733	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴)) → 𝐹 ∈ DivRing)
173	14	ad4antr 733	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴)) → 𝐾 ∈ DivRing)
174	2	ad4antr 733	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴)) → 𝑈 ∈ (SubRing‘𝐸))
175	3	ad4antr 733	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴)) → 𝑉 ∈ (SubRing‘𝐹))
176		fveq2 6842	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑗 → (𝑓‘𝑤) = (𝑓‘𝑗))
177	176	fveq1d 6844	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑗 → ((𝑓‘𝑤)‘𝑣) = ((𝑓‘𝑗)‘𝑣))
178		fveq2 6842	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑖 → ((𝑓‘𝑗)‘𝑣) = ((𝑓‘𝑗)‘𝑖))
179	177, 178	cbvmpov 7463	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) = (𝑗 ∈ 𝑦, 𝑖 ∈ 𝑥 ↦ ((𝑓‘𝑗)‘𝑖))
180		simp-4r 784	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴)) → 𝑥 ∈ (LBasis‘𝐶))
181		simpllr 776	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴)) → 𝑦 ∈ (LBasis‘𝐵))
182		simplr 769	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴)) → 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥))))
183		simpr 484	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴)) → (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴))
184	73, 26, 16, 4, 12, 171, 172, 173, 174, 175, 85, 179, 180, 181, 182, 183	fedgmullem2 33807	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴)) → 𝑐 = ((𝑦 × 𝑥) × {(0g‘(Scalar‘𝐴))}))
185	184	ex 412	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) → ((𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0g‘(Scalar‘𝐴))})))
186	185	ralrimiva 3130	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))((𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0g‘(Scalar‘𝐴))})))
187		eqid 2737	. . . . . . . . 9 ⊢ (Base‘𝐴) = (Base‘𝐴)
188		eqid 2737	. . . . . . . . 9 ⊢ (Scalar‘𝐴) = (Scalar‘𝐴)
189		eqid 2737	. . . . . . . . 9 ⊢ ( ·𝑠 ‘𝐴) = ( ·𝑠 ‘𝐴)
190		eqid 2737	. . . . . . . . 9 ⊢ (0g‘𝐴) = (0g‘𝐴)
191		eqid 2737	. . . . . . . . 9 ⊢ (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐴))
192		eqid 2737	. . . . . . . . 9 ⊢ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥))) = (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))
193	187, 188, 189, 190, 191, 192	islindf4 21805	. . . . . . . 8 ⊢ ((𝐴 ∈ LMod ∧ (𝑦 × 𝑥) ∈ V ∧ (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴)) → ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) LIndF 𝐴 ↔ ∀𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))((𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0g‘(Scalar‘𝐴))}))))
194	193	biimpar 477	. . . . . . 7 ⊢ (((𝐴 ∈ LMod ∧ (𝑦 × 𝑥) ∈ V ∧ (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴)) ∧ ∀𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))((𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0g‘(Scalar‘𝐴))}))) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) LIndF 𝐴)
195	170, 157, 87, 186, 194	syl31anc 1376	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) LIndF 𝐴)
196	72	anasss 466	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐸))
197	196	ralrimivva 3181	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐸))
198	85	rnmposs 32762	. . . . . . . . . 10 ⊢ (∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐸) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) ⊆ (Base‘𝐸))
199	197, 198	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) ⊆ (Base‘𝐸))
200	78	ad2antrr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘𝐸) = (Base‘𝐴))
201	199, 200	sseqtrd 3972	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) ⊆ (Base‘𝐴))
202		eqid 2737	. . . . . . . . 9 ⊢ (LSpan‘𝐴) = (LSpan‘𝐴)
203	187, 202	lspssv 20946	. . . . . . . 8 ⊢ ((𝐴 ∈ LMod ∧ ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) ⊆ (Base‘𝐴)) → ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))) ⊆ (Base‘𝐴))
204	170, 201, 203	syl2anc 585	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))) ⊆ (Base‘𝐴))
205		simpl 482	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)))
206	205	ad4antr 733	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → ((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)))
207		elmapi 8798	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦) → 𝑎:𝑦⟶(Base‘(Scalar‘𝐵)))
208	207	ad4antlr 734	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → 𝑎:𝑦⟶(Base‘(Scalar‘𝐵)))
209		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → 𝑗 ∈ 𝑦)
210	208, 209	ffvelcdmd 7039	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → (𝑎‘𝑗) ∈ (Base‘(Scalar‘𝐵)))
211	113	simprd 495	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶))
212	206, 211	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶))
213	102	ad7antr 739	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → (Base‘(Scalar‘𝐵)) = (Base‘𝐶))
214	212, 213	eqtr4d 2775	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → ((LSpan‘𝐶)‘𝑥) = (Base‘(Scalar‘𝐵)))
215	210, 214	eleqtrrd 2840	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → (𝑎‘𝑗) ∈ ((LSpan‘𝐶)‘𝑥))
216		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
217		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (Scalar‘𝐶) = (Scalar‘𝐶)
218		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (0g‘(Scalar‘𝐶)) = (0g‘(Scalar‘𝐶))
219		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ ( ·𝑠 ‘𝐶) = ( ·𝑠 ‘𝐶)
220		lveclmod 21070	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 ∈ LVec → 𝐶 ∈ LMod)
221	19, 220	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐶 ∈ LMod)
222	221	ad2antrr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐶 ∈ LMod)
223	111, 39, 216, 217, 218, 219, 222, 41	ellspds 33460	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((𝑎‘𝑗) ∈ ((LSpan‘𝐶)‘𝑥) ↔ ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖))))))
224	223	biimpa 476	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑎‘𝑗) ∈ ((LSpan‘𝐶)‘𝑥)) → ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖)))))
225	206, 215, 224	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖)))))
226	225	ralrimiva 3130	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) → ∀𝑗 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖)))))
227		fveq2 6842	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑗 → (𝑎‘𝑤) = (𝑎‘𝑗))
228		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑖 → (𝑏‘𝑣) = (𝑏‘𝑖))
229		id 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑖 → 𝑣 = 𝑖)
230	228, 229	oveq12d 7386	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = 𝑖 → ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣) = ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖))
231	230	cbvmptv 5204	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣)) = (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖))
232	231	oveq2i 7379	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 Σg (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣))) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖)))
233	232	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑗 → (𝐶 Σg (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣))) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖))))
234	227, 233	eqeq12d 2753	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑗 → ((𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣))) ↔ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖)))))
235	234	anbi2d 631	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑗 → ((𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣)))) ↔ (𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖))))))
236	235	rexbidv 3162	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑗 → (∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣)))) ↔ ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖))))))
237	236	cbvralvw 3216	. . . . . . . . . . . . . 14 ⊢ (∀𝑤 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣)))) ↔ ∀𝑗 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖)))))
238		vex 3446	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
239		breq1 5103	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑓‘𝑤) → (𝑏 finSupp (0g‘(Scalar‘𝐶)) ↔ (𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶))))
240		fveq1 6841	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (𝑓‘𝑤) → (𝑏‘𝑣) = ((𝑓‘𝑤)‘𝑣))
241	240	oveq1d 7383	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑓‘𝑤) → ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣) = (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))
242	241	mpteq2dv 5194	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑓‘𝑤) → (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣)) = (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣)))
243	242	oveq2d 7384	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑓‘𝑤) → (𝐶 Σg (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣))) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))
244	243	eqeq2d 2748	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑓‘𝑤) → ((𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣))) ↔ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣)))))
245	239, 244	anbi12d 633	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑓‘𝑤) → ((𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣)))) ↔ ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))))
246	238, 245	ac6s 10406	. . . . . . . . . . . . . 14 ⊢ (∀𝑤 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣)))) → ∃𝑓(𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))))
247	237, 246	sylbir 235	. . . . . . . . . . . . 13 ⊢ (∀𝑗 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖)))) → ∃𝑓(𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))))
248	226, 247	syl 17	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) → ∃𝑓(𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))))
249		simpllr 776	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥))
250		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑗 ∈ 𝑦)
251	249, 250	ffvelcdmd 7039	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (𝑓‘𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥))
252		elmapi 8798	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓‘𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥) → (𝑓‘𝑗):𝑥⟶(Base‘(Scalar‘𝐶)))
253	251, 252	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (𝑓‘𝑗):𝑥⟶(Base‘(Scalar‘𝐶)))
254	253	anasss 466	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → (𝑓‘𝑗):𝑥⟶(Base‘(Scalar‘𝐶)))
255		simprr 773	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → 𝑖 ∈ 𝑥)
256	254, 255	ffvelcdmd 7039	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → ((𝑓‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐶)))
257	74, 77	srasca 21144	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐸 ↾s 𝑉) = (Scalar‘𝐴))
258	12, 257	eqtrid 2784	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐴))
259	47, 50	srasca 21144	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐹 ↾s 𝑉) = (Scalar‘𝐶))
260	13, 259	eqtr3d 2774	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐶))
261	258, 260	eqtr3d 2774	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
262	261	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
263	262	ad4antr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
264	256, 263	eleqtrrd 2840	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → ((𝑓‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
265	264	ralrimivva 3181	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 ((𝑓‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
266	179	fmpo 8022	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 ((𝑓‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)) ↔ (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)):(𝑦 × 𝑥)⟶(Base‘(Scalar‘𝐴)))
267	265, 266	sylib 218	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)):(𝑦 × 𝑥)⟶(Base‘(Scalar‘𝐴)))
268		fvexd 6857	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → (Base‘(Scalar‘𝐴)) ∈ V)
269	157	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → (𝑦 × 𝑥) ∈ V)
270	268, 269	elmapd 8789	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥)) ↔ (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)):(𝑦 × 𝑥)⟶(Base‘(Scalar‘𝐴))))
271	267, 270	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥)))
272	271	ad5ant15 759	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥)))
273	272	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥)))
274	273	adantl3r 751	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥)))
275		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) ∧ 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣))) → 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)))
276	275	breq1d 5110	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) ∧ 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣))) → (𝑐 finSupp (0g‘(Scalar‘𝐴)) ↔ (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) finSupp (0g‘(Scalar‘𝐴))))
277	275	oveq1d 7383	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) ∧ 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣))) → (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))) = ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))))
278	277	oveq2d 7384	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) ∧ 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣))) → (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (𝐴 Σg ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))))
279	278	eqeq2d 2748	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) ∧ 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣))) → (𝑧 = (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) ↔ 𝑧 = (𝐴 Σg ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))))))
280	276, 279	anbi12d 633	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) ∧ 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣))) → ((𝑐 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))))) ↔ ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))))))
281	25	ad8antr 741	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝐸 ∈ DivRing)
282	1	ad8antr 741	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝐹 ∈ DivRing)
283	14	ad8antr 741	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝐾 ∈ DivRing)
284	2	ad8antr 741	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝑈 ∈ (SubRing‘𝐸))
285	3	ad8antr 741	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝑉 ∈ (SubRing‘𝐹))
286	38	ad6antr 737	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝑥 ∈ (LBasis‘𝐶))
287	59	ad6antr 737	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝑦 ∈ (LBasis‘𝐵))
288		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ (Base‘𝐴))
289	288	ad5antr 735	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝑧 ∈ (Base‘𝐴))
290	207	ad5antlr 736	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝑎:𝑦⟶(Base‘(Scalar‘𝐵)))
291		simp-4r 784	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝑎 finSupp (0g‘(Scalar‘𝐵)))
292		simpllr 776	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤))))
293		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑗 → 𝑤 = 𝑗)
294	227, 293	oveq12d 7386	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑗 → ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤) = ((𝑎‘𝑗)( ·𝑠 ‘𝐵)𝑗))
295	294	cbvmptv 5204	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)) = (𝑗 ∈ 𝑦 ↦ ((𝑎‘𝑗)( ·𝑠 ‘𝐵)𝑗))
296	295	oveq2i 7379	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤))) = (𝐵 Σg (𝑗 ∈ 𝑦 ↦ ((𝑎‘𝑗)( ·𝑠 ‘𝐵)𝑗)))
297	292, 296	eqtrdi 2788	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝑧 = (𝐵 Σg (𝑗 ∈ 𝑦 ↦ ((𝑎‘𝑗)( ·𝑠 ‘𝐵)𝑗))))
298		simplr 769	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥))
299		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣)))))
300	176	breq1d 5110	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑗 → ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ↔ (𝑓‘𝑗) finSupp (0g‘(Scalar‘𝐶))))
301		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = 𝑖 → ((𝑓‘𝑤)‘𝑣) = ((𝑓‘𝑤)‘𝑖))
302	301, 229	oveq12d 7386	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 = 𝑖 → (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣) = (((𝑓‘𝑤)‘𝑖)( ·𝑠 ‘𝐶)𝑖))
303	302	cbvmptv 5204	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣)) = (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑖)( ·𝑠 ‘𝐶)𝑖))
304	176	fveq1d 6844	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 𝑗 → ((𝑓‘𝑤)‘𝑖) = ((𝑓‘𝑗)‘𝑖))
305	304	oveq1d 7383	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 𝑗 → (((𝑓‘𝑤)‘𝑖)( ·𝑠 ‘𝐶)𝑖) = (((𝑓‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))
306	305	mpteq2dv 5194	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑗 → (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑖)( ·𝑠 ‘𝐶)𝑖)) = (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)))
307	303, 306	eqtrid 2784	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑗 → (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣)) = (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)))
308	307	oveq2d 7384	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑗 → (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))
309	227, 308	eqeq12d 2753	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑗 → ((𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))) ↔ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)))))
310	300, 309	anbi12d 633	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑗 → (((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣)))) ↔ ((𝑓‘𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))))
311	310	cbvralvw 3216	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣)))) ↔ ∀𝑗 ∈ 𝑦 ((𝑓‘𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)))))
312	299, 311	sylib 218	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → ∀𝑗 ∈ 𝑦 ((𝑓‘𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)))))
313	312	r19.21bi 3230	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) ∧ 𝑗 ∈ 𝑦) → ((𝑓‘𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)))))
314	313	simpld 494	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) ∧ 𝑗 ∈ 𝑦) → (𝑓‘𝑗) finSupp (0g‘(Scalar‘𝐶)))
315	313	simprd 495	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) ∧ 𝑗 ∈ 𝑦) → (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))
316	73, 26, 16, 4, 12, 281, 282, 283, 284, 285, 85, 179, 286, 287, 289, 290, 291, 297, 298, 314, 315	fedgmullem1 33806	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))))))
317	274, 280, 316	rspcedvd 3580	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥))(𝑐 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))))))
318	317	anasss 466	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ (𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣)))))) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥))(𝑐 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))))))
319	248, 318	exlimddv 1937	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥))(𝑐 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))))))
320	319	anasss 466	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ (𝑎 finSupp (0g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤))))) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥))(𝑐 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))))))
321		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (LSpan‘𝐵) = (LSpan‘𝐵)
322	60, 29, 321	islbs4 21799	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (LBasis‘𝐵) ↔ (𝑦 ∈ (LIndS‘𝐵) ∧ ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵)))
323	59, 322	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑦 ∈ (LIndS‘𝐵) ∧ ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵)))
324	323	simprd 495	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵))
325	324	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵))
326	78, 64	eqtr3d 2774	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Base‘𝐴) = (Base‘𝐵))
327	326	ad3antrrr 731	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → (Base‘𝐴) = (Base‘𝐵))
328	325, 327	eqtr4d 2775	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((LSpan‘𝐵)‘𝑦) = (Base‘𝐴))
329	288, 328	eleqtrrd 2840	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ ((LSpan‘𝐵)‘𝑦))
330		eqid 2737	. . . . . . . . . . . . 13 ⊢ (Scalar‘𝐵) = (Scalar‘𝐵)
331		lveclmod 21070	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ LVec → 𝐵 ∈ LMod)
332	28, 331	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ LMod)
333	332	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐵 ∈ LMod)
334	321, 60, 88, 330, 91, 89, 333, 62	ellspds 33460	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑧 ∈ ((LSpan‘𝐵)‘𝑦) ↔ ∃𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)(𝑎 finSupp (0g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤))))))
335	334	biimpa 476	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ ((LSpan‘𝐵)‘𝑦)) → ∃𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)(𝑎 finSupp (0g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))))
336	205, 329, 335	syl2anc 585	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ∃𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)(𝑎 finSupp (0g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))))
337	320, 336	r19.29a 3146	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥))(𝑐 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))))))
338		eqid 2737	. . . . . . . . . . 11 ⊢ (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴))
339	202, 187, 338, 188, 191, 189, 87, 170, 157	ellspd 21769	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑧 ∈ ((LSpan‘𝐴)‘((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) “ (𝑦 × 𝑥))) ↔ ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥))(𝑐 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))))))
340	339	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑧 ∈ ((LSpan‘𝐴)‘((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) “ (𝑦 × 𝑥))) ↔ ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥))(𝑐 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))))))
341	337, 340	mpbird 257	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ ((LSpan‘𝐴)‘((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) “ (𝑦 × 𝑥))))
342	87	ffnd 6671	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) Fn (𝑦 × 𝑥))
343	342	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) Fn (𝑦 × 𝑥))
344		fnima 6630	. . . . . . . . . 10 ⊢ ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) Fn (𝑦 × 𝑥) → ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) “ (𝑦 × 𝑥)) = ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))
345	343, 344	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) “ (𝑦 × 𝑥)) = ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))
346	345	fveq2d 6846	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((LSpan‘𝐴)‘((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) “ (𝑦 × 𝑥))) = ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))))
347	341, 346	eleqtrd 2839	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))))
348	204, 347	eqelssd 3957	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))) = (Base‘𝐴))
349		eqid 2737	. . . . . . 7 ⊢ (Base‘(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))) = (Base‘(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))
350		drngnzr 20693	. . . . . . . . . 10 ⊢ (𝐾 ∈ DivRing → 𝐾 ∈ NzRing)
351	14, 350	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ NzRing)
352	258, 351	eqeltrrd 2838	. . . . . . . 8 ⊢ (𝜑 → (Scalar‘𝐴) ∈ NzRing)
353	352	ad2antrr 727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Scalar‘𝐴) ∈ NzRing)
354	187, 349, 188, 189, 190, 191, 202, 170, 353, 157, 156	lindflbs 33471	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) ∈ (LBasis‘𝐴) ↔ ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) LIndF 𝐴 ∧ ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))) = (Base‘𝐴))))
355	195, 348, 354	mpbir2and 714	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) ∈ (LBasis‘𝐴))
356		eqid 2737	. . . . . 6 ⊢ (LBasis‘𝐴) = (LBasis‘𝐴)
357	356	dimval 33777	. . . . 5 ⊢ ((𝐴 ∈ LVec ∧ ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) ∈ (LBasis‘𝐴)) → (dim‘𝐴) = (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))))
358	167, 355, 357	syl2anc 585	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐴) = (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))))
359	29	dimval 33777	. . . . . 6 ⊢ ((𝐵 ∈ LVec ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐵) = (♯‘𝑦))
360	92, 59, 359	syl2anc 585	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐵) = (♯‘𝑦))
361	20	dimval 33777	. . . . . 6 ⊢ ((𝐶 ∈ LVec ∧ 𝑥 ∈ (LBasis‘𝐶)) → (dim‘𝐶) = (♯‘𝑥))
362	110, 38, 361	syl2anc 585	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐶) = (♯‘𝑥))
363	360, 362	oveq12d 7386	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((dim‘𝐵) ·e (dim‘𝐶)) = ((♯‘𝑦) ·e (♯‘𝑥)))
364	164, 358, 363	3eqtr4d 2782	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐴) = ((dim‘𝐵) ·e (dim‘𝐶)))
365	34, 364	exlimddv 1937	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) → (dim‘𝐴) = ((dim‘𝐵) ·e (dim‘𝐶)))
366	24, 365	exlimddv 1937	1 ⊢ (𝜑 → (dim‘𝐴) = ((dim‘𝐵) ·e (dim‘𝐶)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  ∃wrex 3062  Vcvv 3442   ⊆ wss 3903  ∅c0 4287  {csn 4582   class class class wbr 5100   ↦ cmpt 5181   × cxp 5630  ran crn 5633   “ cima 5635   Fn wfn 6495  ⟶wf 6496  –1-1→wf1 6497  ‘cfv 6500  (class class class)co 7368   ∈ cmpo 7370   ∘_f cof 7630   ↑_m cmap 8775   ≈ cen 8892   finSupp cfsupp 9276   ·_e cxmu 13037  ♯chash 14265  Basecbs 17148   ↾_s cress 17169  +_gcplusg 17189  ._rcmulr 17190  Scalarcsca 17192   ·_𝑠 cvsca 17193  0_gc0g 17371   Σ_g cgsu 17372  Ringcrg 20180  NzRingcnzr 20457  SubRingcsubrg 20514  DivRingcdr 20674  LModclmod 20823  LSpanclspn 20934  LBasisclbs 21038  LVecclvec 21066  subringAlg csra 21135   freeLMod cfrlm 21713   LIndF clindf 21771  LIndSclinds 21772  dimcldim 33775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-reg 9509  ax-inf2 9562  ax-ac2 10385  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-tp 4587  df-op 4589  df-uni 4866  df-int 4905  df-iun 4950  df-iin 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-se 5586  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-of 7632  df-rpss 7678  df-om 7819  df-1st 7943  df-2nd 7944  df-supp 8113  df-tpos 8178  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-1o 8407  df-2o 8408  df-oadd 8411  df-er 8645  df-map 8777  df-ixp 8848  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-fsupp 9277  df-sup 9357  df-oi 9427  df-r1 9688  df-rank 9689  df-dju 9825  df-card 9863  df-acn 9866  df-ac 10038  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-nn 12158  df-2 12220  df-3 12221  df-4 12222  df-5 12223  df-6 12224  df-7 12225  df-8 12226  df-9 12227  df-n0 12414  df-xnn0 12487  df-z 12501  df-dec 12620  df-uz 12764  df-xmul 13040  df-fz 13436  df-fzo 13583  df-seq 13937  df-hash 14266  df-struct 17086  df-sets 17103  df-slot 17121  df-ndx 17133  df-base 17149  df-ress 17170  df-plusg 17202  df-mulr 17203  df-sca 17205  df-vsca 17206  df-ip 17207  df-tset 17208  df-ple 17209  df-ocomp 17210  df-ds 17211  df-hom 17213  df-cco 17214  df-0g 17373  df-gsum 17374  df-prds 17379  df-pws 17381  df-mre 17517  df-mrc 17518  df-mri 17519  df-acs 17520  df-proset 18229  df-drs 18230  df-poset 18248  df-ipo 18463  df-mgm 18577  df-sgrp 18656  df-mnd 18672  df-mhm 18720  df-submnd 18721  df-grp 18878  df-minusg 18879  df-sbg 18880  df-mulg 19010  df-subg 19065  df-ghm 19154  df-cntz 19258  df-cmn 19723  df-abl 19724  df-mgp 20088  df-rng 20100  df-ur 20129  df-ring 20182  df-oppr 20285  df-dvdsr 20305  df-unit 20306  df-invr 20336  df-nzr 20458  df-subrng 20491  df-subrg 20515  df-drng 20676  df-lmod 20825  df-lss 20895  df-lsp 20935  df-lmhm 20986  df-lbs 21039  df-lvec 21067  df-sra 21137  df-rgmod 21138  df-dsmm 21699  df-frlm 21714  df-uvc 21750  df-lindf 21773  df-linds 21774  df-dim 33776

This theorem is referenced by:  extdgmul  33840