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 31380

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 19780	. . . . . . . . . . 11 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (𝑉 ∈ (SubRing‘𝐹) ↔ (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈)))
6	5	biimpa 480	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ∈ (SubRing‘𝐹)) → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))
7	2, 3, 6	syl2anc 587	. . . . . . . . 9 ⊢ (𝜑 → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))
8	7	simprd 499	. . . . . . . 8 ⊢ (𝜑 → 𝑉 ⊆ 𝑈)
9		ressabs 16747	. . . . . . . 8 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈) → ((𝐸 ↾_s 𝑈) ↾_s 𝑉) = (𝐸 ↾_s 𝑉))
10	2, 8, 9	syl2anc 587	. . . . . . 7 ⊢ (𝜑 → ((𝐸 ↾_s 𝑈) ↾_s 𝑉) = (𝐸 ↾_s 𝑉))
11	4	oveq1i 7201	. . . . . . 7 ⊢ (𝐹 ↾_s 𝑉) = ((𝐸 ↾_s 𝑈) ↾_s 𝑉)
12		fedgmul.k	. . . . . . 7 ⊢ 𝐾 = (𝐸 ↾_s 𝑉)
13	10, 11, 12	3eqtr4g 2796	. . . . . 6 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) = 𝐾)
14		fedgmul.3	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ DivRing)
15	13, 14	eqeltrd 2831	. . . . 5 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) ∈ DivRing)
16		fedgmul.c	. . . . . 6 ⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
17		eqid 2736	. . . . . 6 ⊢ (𝐹 ↾_s 𝑉) = (𝐹 ↾_s 𝑉)
18	16, 17	sralvec 31343	. . . . 5 ⊢ ((𝐹 ∈ DivRing ∧ (𝐹 ↾_s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
19	1, 15, 3, 18	syl3anc 1373	. . . 4 ⊢ (𝜑 → 𝐶 ∈ LVec)
20		eqid 2736	. . . . 5 ⊢ (LBasis‘𝐶) = (LBasis‘𝐶)
21	20	lbsex 20156	. . . 4 ⊢ (𝐶 ∈ LVec → (LBasis‘𝐶) ≠ ∅)
22	19, 21	syl 17	. . 3 ⊢ (𝜑 → (LBasis‘𝐶) ≠ ∅)
23		n0 4247	. . 3 ⊢ ((LBasis‘𝐶) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (LBasis‘𝐶))
24	22, 23	sylib 221	. 2 ⊢ (𝜑 → ∃𝑥 𝑥 ∈ (LBasis‘𝐶))
25		fedgmul.1	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ DivRing)
26		fedgmul.b	. . . . . . . 8 ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
27	26, 4	sralvec 31343	. . . . . . 7 ⊢ ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐵 ∈ LVec)
28	25, 1, 2, 27	syl3anc 1373	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ LVec)
29		eqid 2736	. . . . . . 7 ⊢ (LBasis‘𝐵) = (LBasis‘𝐵)
30	29	lbsex 20156	. . . . . 6 ⊢ (𝐵 ∈ LVec → (LBasis‘𝐵) ≠ ∅)
31	28, 30	syl 17	. . . . 5 ⊢ (𝜑 → (LBasis‘𝐵) ≠ ∅)
32		n0 4247	. . . . 5 ⊢ ((LBasis‘𝐵) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (LBasis‘𝐵))
33	31, 32	sylib 221	. . . 4 ⊢ (𝜑 → ∃𝑦 𝑦 ∈ (LBasis‘𝐵))
34	33	adantr 484	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) → ∃𝑦 𝑦 ∈ (LBasis‘𝐵))
35		drngring 19728	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
36	25, 35	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ∈ Ring)
37	36	ad4antr 732	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝐸 ∈ Ring)
38		simplr 769	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ∈ (LBasis‘𝐶))
39		eqid 2736	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝐶) = (Base‘𝐶)
40	39, 20	lbsss 20068	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (LBasis‘𝐶) → 𝑥 ⊆ (Base‘𝐶))
41	38, 40	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ⊆ (Base‘𝐶))
42		eqid 2736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Base‘𝐸) = (Base‘𝐸)
43	42	subrgss 19755	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
44	2, 43	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐸))
45	4, 42	ressbas2 16739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
46	44, 45	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑈 = (Base‘𝐹))
47	16	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐶 = ((subringAlg ‘𝐹)‘𝑉))
48		eqid 2736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Base‘𝐹) = (Base‘𝐹)
49	48	subrgss 19755	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
50	3, 49	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐹))
51	47, 50	srabase 20169	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Base‘𝐹) = (Base‘𝐶))
52	46, 51	eqtrd 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 = (Base‘𝐶))
53	52, 44	eqsstrrd 3926	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
54	53	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘𝐶) ⊆ (Base‘𝐸))
55	41, 54	sstrd 3897	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ⊆ (Base‘𝐸))
56	55	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑥 ⊆ (Base‘𝐸))
57		simpr 488	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑖 ∈ 𝑥)
58	56, 57	sseldd 3888	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑖 ∈ (Base‘𝐸))
59		simpr 488	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ∈ (LBasis‘𝐵))
60		eqid 2736	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝐵) = (Base‘𝐵)
61	60, 29	lbsss 20068	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (LBasis‘𝐵) → 𝑦 ⊆ (Base‘𝐵))
62	59, 61	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ⊆ (Base‘𝐵))
63	26	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 = ((subringAlg ‘𝐸)‘𝑈))
64	63, 44	srabase 20169	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐵))
65	64	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘𝐸) = (Base‘𝐵))
66	62, 65	sseqtrrd 3928	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ⊆ (Base‘𝐸))
67	66	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑦 ⊆ (Base‘𝐸))
68		simplr 769	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑗 ∈ 𝑦)
69	67, 68	sseldd 3888	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑗 ∈ (Base‘𝐸))
70		eqid 2736	. . . . . . . . . . . . . 14 ⊢ (._r‘𝐸) = (._r‘𝐸)
71	42, 70	ringcl 19533	. . . . . . . . . . . . 13 ⊢ ((𝐸 ∈ Ring ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸)) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐸))
72	37, 58, 69, 71	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐸))
73		fedgmul.a	. . . . . . . . . . . . . . 15 ⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑉)
74	73	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝐸)‘𝑉))
75	7	simpld 498	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐸))
76	42	subrgss 19755	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
77	75, 76	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐸))
78	74, 77	srabase 20169	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐴))
79	78	ad4antr 732	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (Base‘𝐸) = (Base‘𝐴))
80	72, 79	eleqtrd 2833	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴))
81	80	anasss 470	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴))
82	81	ralrimivva 3102	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴))
83		oveq2 7199	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑗 → (𝑡(._r‘𝐸)𝑤) = (𝑡(._r‘𝐸)𝑗))
84		oveq1 7198	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑖 → (𝑡(._r‘𝐸)𝑗) = (𝑖(._r‘𝐸)𝑗))
85	83, 84	cbvmpov 7284	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) = (𝑗 ∈ 𝑦, 𝑖 ∈ 𝑥 ↦ (𝑖(._r‘𝐸)𝑗))
86	85	fmpo 7816	. . . . . . . . 9 ⊢ (∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴) ↔ (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴))
87	82, 86	sylib 221	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴))
88		eqid 2736	. . . . . . . . . . . . . 14 ⊢ (Base‘(Scalar‘𝐵)) = (Base‘(Scalar‘𝐵))
89		eqid 2736	. . . . . . . . . . . . . 14 ⊢ ( ·_𝑠 ‘𝐵) = ( ·_𝑠 ‘𝐵)
90		eqid 2736	. . . . . . . . . . . . . 14 ⊢ (+_g‘𝐵) = (+_g‘𝐵)
91		eqid 2736	. . . . . . . . . . . . . 14 ⊢ (0_g‘(Scalar‘𝐵)) = (0_g‘(Scalar‘𝐵))
92	28	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐵 ∈ LVec)
93	92	ad5antr 734	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝐵 ∈ LVec)
94	29	lbslinds 20749	. . . . . . . . . . . . . . . 16 ⊢ (LBasis‘𝐵) ⊆ (LIndS‘𝐵)
95	94, 59	sseldi 3885	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ∈ (LIndS‘𝐵))
96	95	ad5antr 734	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑦 ∈ (LIndS‘𝐵))
97	68	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑗 ∈ 𝑦)
98		simpllr 776	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑣 ∈ 𝑦)
99	63, 44	srasca 20172	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ↾_s 𝑈) = (Scalar‘𝐵))
100	4, 99	syl5eq 2783	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 = (Scalar‘𝐵))
101	100	fveq2d 6699	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Base‘𝐹) = (Base‘(Scalar‘𝐵)))
102	101, 51	eqtr3d 2773	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Base‘(Scalar‘𝐵)) = (Base‘𝐶))
103	102	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘(Scalar‘𝐵)) = (Base‘𝐶))
104	41, 103	sseqtrrd 3928	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ⊆ (Base‘(Scalar‘𝐵)))
105	104	ad5antr 734	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑥 ⊆ (Base‘(Scalar‘𝐵)))
106		simp-4r 784	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑖 ∈ 𝑥)
107	105, 106	sseldd 3888	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑖 ∈ (Base‘(Scalar‘𝐵)))
108		simplr 769	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑢 ∈ 𝑥)
109	105, 108	sseldd 3888	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑢 ∈ (Base‘(Scalar‘𝐵)))
110	19	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐶 ∈ LVec)
111		eqid 2736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (LSpan‘𝐶) = (LSpan‘𝐶)
112	39, 20, 111	islbs4 20748	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (LBasis‘𝐶) ↔ (𝑥 ∈ (LIndS‘𝐶) ∧ ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶)))
113	38, 112	sylib 221	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑥 ∈ (LIndS‘𝐶) ∧ ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶)))
114	113	simpld 498	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ∈ (LIndS‘𝐶))
115		eqid 2736	. . . . . . . . . . . . . . . . . . 19 ⊢ (0_g‘𝐶) = (0_g‘𝐶)
116	115	0nellinds 31234	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐶 ∈ LVec ∧ 𝑥 ∈ (LIndS‘𝐶)) → ¬ (0_g‘𝐶) ∈ 𝑥)
117	110, 114, 116	syl2anc 587	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ¬ (0_g‘𝐶) ∈ 𝑥)
118	117	ad5antr 734	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → ¬ (0_g‘𝐶) ∈ 𝑥)
119		nelne2 3029	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ 𝑥 ∧ ¬ (0_g‘𝐶) ∈ 𝑥) → 𝑖 ≠ (0_g‘𝐶))
120	106, 118, 119	syl2anc 587	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑖 ≠ (0_g‘𝐶))
121	100	fveq2d 6699	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0_g‘𝐹) = (0_g‘(Scalar‘𝐵)))
122	16, 1, 3	drgext0g 31345	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0_g‘𝐹) = (0_g‘𝐶))
123	121, 122	eqtr3d 2773	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0_g‘(Scalar‘𝐵)) = (0_g‘𝐶))
124	123	ad7antr 738	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (0_g‘(Scalar‘𝐵)) = (0_g‘𝐶))
125	120, 124	neeqtrrd 3006	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → 𝑖 ≠ (0_g‘(Scalar‘𝐵)))
126		simpr 488	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢))
127		ovexd 7226	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑖(._r‘𝐸)𝑗) ∈ V)
128	85	ovmpt4g 7334	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥 ∧ (𝑖(._r‘𝐸)𝑗) ∈ V) → (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑖(._r‘𝐸)𝑗))
129	97, 106, 127, 128	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑖(._r‘𝐸)𝑗))
130	26, 25, 2	drgextvsca 31346	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (._r‘𝐸) = ( ·_𝑠 ‘𝐵))
131	130	oveqd 7208	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑖(._r‘𝐸)𝑗) = (𝑖( ·_𝑠 ‘𝐵)𝑗))
132	131	ad7antr 738	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑖(._r‘𝐸)𝑗) = (𝑖( ·_𝑠 ‘𝐵)𝑗))
133	129, 132	eqtrd 2771	. . . . . . . . . . . . . . 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 7209	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)) → (𝑖(._r‘𝐸)𝑗) = (𝑢(._r‘𝐸)𝑣))
138		simplr 769	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → 𝑣 ∈ 𝑦)
139		simpr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → 𝑢 ∈ 𝑥)
140		ovexd 7226	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑢(._r‘𝐸)𝑣) ∈ V)
141	134, 137, 138, 139, 140	ovmpod 7339	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) = (𝑢(._r‘𝐸)𝑣))
142	141	adantllr 719	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) = (𝑢(._r‘𝐸)𝑣))
143	142	adantl3r 750	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) = (𝑢(._r‘𝐸)𝑣))
144	143	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) = (𝑢(._r‘𝐸)𝑣))
145	130	oveqd 7208	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑢(._r‘𝐸)𝑣) = (𝑢( ·_𝑠 ‘𝐵)𝑣))
146	145	ad7antr 738	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑢(._r‘𝐸)𝑣) = (𝑢( ·_𝑠 ‘𝐵)𝑣))
147	144, 146	eqtrd 2771	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) = (𝑢( ·_𝑠 ‘𝐵)𝑣))
148	126, 133, 147	3eqtr3d 2779	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑖( ·_𝑠 ‘𝐵)𝑗) = (𝑢( ·_𝑠 ‘𝐵)𝑣))
149	88, 89, 90, 91, 93, 96, 97, 98, 107, 109, 125, 148	linds2eq 31243	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢)) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢))
150	149	ex 416	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
151	150	anasss 470	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ (𝑣 ∈ 𝑦 ∧ 𝑢 ∈ 𝑥)) → ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
152	151	ralrimivva 3102	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → ∀𝑣 ∈ 𝑦 ∀𝑢 ∈ 𝑥 ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
153	152	anasss 470	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → ∀𝑣 ∈ 𝑦 ∀𝑢 ∈ 𝑥 ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
154	153	ralrimivva 3102	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 ∀𝑣 ∈ 𝑦 ∀𝑢 ∈ 𝑥 ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
155		f1opr 7245	. . . . . . . 8 ⊢ ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)–1-1→(Base‘𝐴) ↔ ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴) ∧ ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 ∀𝑣 ∈ 𝑦 ∀𝑢 ∈ 𝑥 ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢))))
156	87, 154, 155	sylanbrc 586	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)–1-1→(Base‘𝐴))
157	59, 38	xpexd 7514	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑦 × 𝑥) ∈ V)
158		f1rnen 30637	. . . . . . 7 ⊢ (((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)–1-1→(Base‘𝐴) ∧ (𝑦 × 𝑥) ∈ V) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ≈ (𝑦 × 𝑥))
159	156, 157, 158	syl2anc 587	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ≈ (𝑦 × 𝑥))
160		hasheni 13879	. . . . . 6 ⊢ (ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ≈ (𝑦 × 𝑥) → (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = (♯‘(𝑦 × 𝑥)))
161	159, 160	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = (♯‘(𝑦 × 𝑥)))
162		hashxpe 30801	. . . . . 6 ⊢ ((𝑦 ∈ (LBasis‘𝐵) ∧ 𝑥 ∈ (LBasis‘𝐶)) → (♯‘(𝑦 × 𝑥)) = ((♯‘𝑦) ·_e (♯‘𝑥)))
163	59, 38, 162	syl2anc 587	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (♯‘(𝑦 × 𝑥)) = ((♯‘𝑦) ·_e (♯‘𝑥)))
164	161, 163	eqtrd 2771	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = ((♯‘𝑦) ·_e (♯‘𝑥)))
165	73, 12	sralvec 31343	. . . . . . 7 ⊢ ((𝐸 ∈ DivRing ∧ 𝐾 ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec)
166	25, 14, 75, 165	syl3anc 1373	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ LVec)
167	166	ad2antrr 726	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐴 ∈ LVec)
168		lveclmod 20097	. . . . . . . . 9 ⊢ (𝐴 ∈ LVec → 𝐴 ∈ LMod)
169	166, 168	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ LMod)
170	169	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐴 ∈ LMod)
171	25	ad4antr 732	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝐸 ∈ DivRing)
172	1	ad4antr 732	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝐹 ∈ DivRing)
173	14	ad4antr 732	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝐾 ∈ DivRing)
174	2	ad4antr 732	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝑈 ∈ (SubRing‘𝐸))
175	3	ad4antr 732	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝑉 ∈ (SubRing‘𝐹))
176		fveq2 6695	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑗 → (𝑓‘𝑤) = (𝑓‘𝑗))
177	176	fveq1d 6697	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑗 → ((𝑓‘𝑤)‘𝑣) = ((𝑓‘𝑗)‘𝑣))
178		fveq2 6695	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑖 → ((𝑓‘𝑗)‘𝑣) = ((𝑓‘𝑗)‘𝑖))
179	177, 178	cbvmpov 7284	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) = (𝑗 ∈ 𝑦, 𝑖 ∈ 𝑥 ↦ ((𝑓‘𝑗)‘𝑖))
180		simp-4r 784	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝑥 ∈ (LBasis‘𝐶))
181		simpllr 776	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝑦 ∈ (LBasis‘𝐵))
182		simplr 769	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥))))
183		simpr 488	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴))
184	73, 26, 16, 4, 12, 171, 172, 173, 174, 175, 85, 179, 180, 181, 182, 183	fedgmullem2 31379	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴)) → 𝑐 = ((𝑦 × 𝑥) × {(0_g‘(Scalar‘𝐴))}))
185	184	ex 416	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) → ((𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0_g‘(Scalar‘𝐴))})))
186	185	ralrimiva 3095	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))((𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0_g‘(Scalar‘𝐴))})))
187		eqid 2736	. . . . . . . . 9 ⊢ (Base‘𝐴) = (Base‘𝐴)
188		eqid 2736	. . . . . . . . 9 ⊢ (Scalar‘𝐴) = (Scalar‘𝐴)
189		eqid 2736	. . . . . . . . 9 ⊢ ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘𝐴)
190		eqid 2736	. . . . . . . . 9 ⊢ (0_g‘𝐴) = (0_g‘𝐴)
191		eqid 2736	. . . . . . . . 9 ⊢ (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐴))
192		eqid 2736	. . . . . . . . 9 ⊢ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥))) = (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))
193	187, 188, 189, 190, 191, 192	islindf4 20754	. . . . . . . 8 ⊢ ((𝐴 ∈ LMod ∧ (𝑦 × 𝑥) ∈ V ∧ (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴)) → ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) LIndF 𝐴 ↔ ∀𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))((𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0_g‘(Scalar‘𝐴))}))))
194	193	biimpar 481	. . . . . . 7 ⊢ (((𝐴 ∈ LMod ∧ (𝑦 × 𝑥) ∈ V ∧ (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴)) ∧ ∀𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))((𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (0_g‘𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0_g‘(Scalar‘𝐴))}))) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) LIndF 𝐴)
195	170, 157, 87, 186, 194	syl31anc 1375	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) LIndF 𝐴)
196	72	anasss 470	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐸))
197	196	ralrimivva 3102	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐸))
198	85	rnmposs 30685	. . . . . . . . . 10 ⊢ (∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐸) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ⊆ (Base‘𝐸))
199	197, 198	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ⊆ (Base‘𝐸))
200	78	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘𝐸) = (Base‘𝐴))
201	199, 200	sseqtrd 3927	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ⊆ (Base‘𝐴))
202		eqid 2736	. . . . . . . . 9 ⊢ (LSpan‘𝐴) = (LSpan‘𝐴)
203	187, 202	lspssv 19974	. . . . . . . 8 ⊢ ((𝐴 ∈ LMod ∧ ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ⊆ (Base‘𝐴)) → ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) ⊆ (Base‘𝐴))
204	170, 201, 203	syl2anc 587	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) ⊆ (Base‘𝐴))
205		simpl 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)))
206	205	ad4antr 732	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → ((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)))
207		elmapi 8508	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦) → 𝑎:𝑦⟶(Base‘(Scalar‘𝐵)))
208	207	ad4antlr 733	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → 𝑎:𝑦⟶(Base‘(Scalar‘𝐵)))
209		simpr 488	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → 𝑗 ∈ 𝑦)
210	208, 209	ffvelrnd 6883	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → (𝑎‘𝑗) ∈ (Base‘(Scalar‘𝐵)))
211	113	simprd 499	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶))
212	206, 211	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶))
213	102	ad7antr 738	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → (Base‘(Scalar‘𝐵)) = (Base‘𝐶))
214	212, 213	eqtr4d 2774	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → ((LSpan‘𝐶)‘𝑥) = (Base‘(Scalar‘𝐵)))
215	210, 214	eleqtrrd 2834	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → (𝑎‘𝑗) ∈ ((LSpan‘𝐶)‘𝑥))
216		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
217		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (Scalar‘𝐶) = (Scalar‘𝐶)
218		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (0_g‘(Scalar‘𝐶)) = (0_g‘(Scalar‘𝐶))
219		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ ( ·_𝑠 ‘𝐶) = ( ·_𝑠 ‘𝐶)
220		lveclmod 20097	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 ∈ LVec → 𝐶 ∈ LMod)
221	19, 220	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐶 ∈ LMod)
222	221	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐶 ∈ LMod)
223	111, 39, 216, 217, 218, 219, 222, 41	ellspds 31232	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((𝑎‘𝑗) ∈ ((LSpan‘𝐶)‘𝑥) ↔ ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))))
224	223	biimpa 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑎‘𝑗) ∈ ((LSpan‘𝐶)‘𝑥)) → ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
225	206, 215, 224	syl2anc 587	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
226	225	ralrimiva 3095	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) → ∀𝑗 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
227		fveq2 6695	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑗 → (𝑎‘𝑤) = (𝑎‘𝑗))
228		fveq2 6695	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑖 → (𝑏‘𝑣) = (𝑏‘𝑖))
229		id 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑖 → 𝑣 = 𝑖)
230	228, 229	oveq12d 7209	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = 𝑖 → ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣) = ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖))
231	230	cbvmptv 5143	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)) = (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖))
232	231	oveq2i 7202	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))
233	232	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑗 → (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))
234	227, 233	eqeq12d 2752	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑗 → ((𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) ↔ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
235	234	anbi2d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑗 → ((𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) ↔ (𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))))
236	235	rexbidv 3206	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑗 → (∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) ↔ ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))))
237	236	cbvralvw 3348	. . . . . . . . . . . . . 14 ⊢ (∀𝑤 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) ↔ ∀𝑗 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
238		vex 3402	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
239		breq1 5042	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑓‘𝑤) → (𝑏 finSupp (0_g‘(Scalar‘𝐶)) ↔ (𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶))))
240		fveq1 6694	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (𝑓‘𝑤) → (𝑏‘𝑣) = ((𝑓‘𝑤)‘𝑣))
241	240	oveq1d 7206	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑓‘𝑤) → ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣) = (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))
242	241	mpteq2dv 5136	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑓‘𝑤) → (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)) = (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))
243	242	oveq2d 7207	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑓‘𝑤) → (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))
244	243	eqeq2d 2747	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑓‘𝑤) → ((𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) ↔ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))))
245	239, 244	anbi12d 634	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑓‘𝑤) → ((𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) ↔ ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))))
246	238, 245	ac6s 10063	. . . . . . . . . . . . . 14 ⊢ (∀𝑤 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) → ∃𝑓(𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))))
247	237, 246	sylbir 238	. . . . . . . . . . . . 13 ⊢ (∀𝑗 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥)(𝑏 finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))) → ∃𝑓(𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))))
248	226, 247	syl 17	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) → ∃𝑓(𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))))
249		simpllr 776	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥))
250		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑗 ∈ 𝑦)
251	249, 250	ffvelrnd 6883	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (𝑓‘𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥))
252		elmapi 8508	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓‘𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑_m 𝑥) → (𝑓‘𝑗):𝑥⟶(Base‘(Scalar‘𝐶)))
253	251, 252	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (𝑓‘𝑗):𝑥⟶(Base‘(Scalar‘𝐶)))
254	253	anasss 470	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → (𝑓‘𝑗):𝑥⟶(Base‘(Scalar‘𝐶)))
255		simprr 773	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → 𝑖 ∈ 𝑥)
256	254, 255	ffvelrnd 6883	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → ((𝑓‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐶)))
257	74, 77	srasca 20172	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐸 ↾_s 𝑉) = (Scalar‘𝐴))
258	12, 257	syl5eq 2783	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐴))
259	47, 50	srasca 20172	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) = (Scalar‘𝐶))
260	13, 259	eqtr3d 2773	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐶))
261	258, 260	eqtr3d 2773	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
262	261	fveq2d 6699	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
263	262	ad4antr 732	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
264	256, 263	eleqtrrd 2834	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → ((𝑓‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
265	264	ralrimivva 3102	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) → ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 ((𝑓‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
266	179	fmpo 7816	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 ((𝑓‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)) ↔ (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)):(𝑦 × 𝑥)⟶(Base‘(Scalar‘𝐴)))
267	265, 266	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) → (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)):(𝑦 × 𝑥)⟶(Base‘(Scalar‘𝐴)))
268		fvexd 6710	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) → (Base‘(Scalar‘𝐴)) ∈ V)
269	157	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) → (𝑦 × 𝑥) ∈ V)
270	268, 269	elmapd 8500	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) → ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥)) ↔ (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)):(𝑦 × 𝑥)⟶(Base‘(Scalar‘𝐴))))
271	267, 270	mpbird 260	. . . . . . . . . . . . . . . . 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 484	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥)))
274	273	adantl3r 750	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥)))
275		simpr 488	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) ∧ 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣))) → 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)))
276	275	breq1d 5049	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) ∧ 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣))) → (𝑐 finSupp (0_g‘(Scalar‘𝐴)) ↔ (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) finSupp (0_g‘(Scalar‘𝐴))))
277	275	oveq1d 7206	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) ∧ 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣))) → (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))
278	277	oveq2d 7207	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) ∧ 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣))) → (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) = (𝐴 Σ_g ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))))
279	278	eqeq2d 2747	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) ∧ 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣))) → (𝑧 = (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))) ↔ 𝑧 = (𝐴 Σ_g ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))))
280	276, 279	anbi12d 634	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) ∧ 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣))) → ((𝑐 finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))) ↔ ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))))))
281	25	ad8antr 740	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝐸 ∈ DivRing)
282	1	ad8antr 740	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝐹 ∈ DivRing)
283	14	ad8antr 740	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝐾 ∈ DivRing)
284	2	ad8antr 740	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑈 ∈ (SubRing‘𝐸))
285	3	ad8antr 740	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑉 ∈ (SubRing‘𝐹))
286	38	ad6antr 736	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑥 ∈ (LBasis‘𝐶))
287	59	ad6antr 736	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑦 ∈ (LBasis‘𝐵))
288		simpr 488	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ (Base‘𝐴))
289	288	ad5antr 734	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑧 ∈ (Base‘𝐴))
290	207	ad5antlr 735	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑎:𝑦⟶(Base‘(Scalar‘𝐵)))
291		simp-4r 784	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑎 finSupp (0_g‘(Scalar‘𝐵)))
292		simpllr 776	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤))))
293		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑗 → 𝑤 = 𝑗)
294	227, 293	oveq12d 7209	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑗 → ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤) = ((𝑎‘𝑗)( ·_𝑠 ‘𝐵)𝑗))
295	294	cbvmptv 5143	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)) = (𝑗 ∈ 𝑦 ↦ ((𝑎‘𝑗)( ·_𝑠 ‘𝐵)𝑗))
296	295	oveq2i 7202	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤))) = (𝐵 Σ_g (𝑗 ∈ 𝑦 ↦ ((𝑎‘𝑗)( ·_𝑠 ‘𝐵)𝑗)))
297	292, 296	eqtrdi 2787	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑧 = (𝐵 Σ_g (𝑗 ∈ 𝑦 ↦ ((𝑎‘𝑗)( ·_𝑠 ‘𝐵)𝑗))))
298		simplr 769	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥))
299		simpr 488	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))))
300	176	breq1d 5049	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑗 → ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ↔ (𝑓‘𝑗) finSupp (0_g‘(Scalar‘𝐶))))
301		fveq2 6695	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = 𝑖 → ((𝑓‘𝑤)‘𝑣) = ((𝑓‘𝑤)‘𝑖))
302	301, 229	oveq12d 7209	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 = 𝑖 → (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣) = (((𝑓‘𝑤)‘𝑖)( ·_𝑠 ‘𝐶)𝑖))
303	302	cbvmptv 5143	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)) = (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑖)( ·_𝑠 ‘𝐶)𝑖))
304	176	fveq1d 6697	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 𝑗 → ((𝑓‘𝑤)‘𝑖) = ((𝑓‘𝑗)‘𝑖))
305	304	oveq1d 7206	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 𝑗 → (((𝑓‘𝑤)‘𝑖)( ·_𝑠 ‘𝐶)𝑖) = (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖))
306	305	mpteq2dv 5136	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑗 → (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)) = (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))
307	303, 306	syl5eq 2783	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑗 → (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)) = (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))
308	307	oveq2d 7207	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑗 → (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))
309	227, 308	eqeq12d 2752	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑗 → ((𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))) ↔ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
310	300, 309	anbi12d 634	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑗 → (((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) ↔ ((𝑓‘𝑗) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))))
311	310	cbvralvw 3348	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))) ↔ ∀𝑗 ∈ 𝑦 ((𝑓‘𝑗) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
312	299, 311	sylib 221	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → ∀𝑗 ∈ 𝑦 ((𝑓‘𝑗) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
313	312	r19.21bi 3120	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) ∧ 𝑗 ∈ 𝑦) → ((𝑓‘𝑗) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖)))))
314	313	simpld 498	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) ∧ 𝑗 ∈ 𝑦) → (𝑓‘𝑗) finSupp (0_g‘(Scalar‘𝐶)))
315	313	simprd 499	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) ∧ 𝑗 ∈ 𝑦) → (𝑎‘𝑗) = (𝐶 Σ_g (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·_𝑠 ‘𝐶)𝑖))))
316	73, 26, 16, 4, 12, 281, 282, 283, 284, 285, 85, 179, 286, 287, 289, 290, 291, 297, 298, 314, 315	fedgmullem1 31378	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))))
317	274, 280, 316	rspcedvd 3530	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣))))) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥))(𝑐 finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))))
318	317	anasss 470	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) ∧ (𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑_m 𝑥) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0_g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σ_g (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·_𝑠 ‘𝐶)𝑣)))))) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥))(𝑐 finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))))
319	248, 318	exlimddv 1943	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥))(𝑐 finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))))
320	319	anasss 470	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)) ∧ (𝑎 finSupp (0_g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤))))) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥))(𝑐 finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))))
321		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (LSpan‘𝐵) = (LSpan‘𝐵)
322	60, 29, 321	islbs4 20748	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (LBasis‘𝐵) ↔ (𝑦 ∈ (LIndS‘𝐵) ∧ ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵)))
323	59, 322	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑦 ∈ (LIndS‘𝐵) ∧ ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵)))
324	323	simprd 499	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵))
325	324	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵))
326	78, 64	eqtr3d 2773	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Base‘𝐴) = (Base‘𝐵))
327	326	ad3antrrr 730	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → (Base‘𝐴) = (Base‘𝐵))
328	325, 327	eqtr4d 2774	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((LSpan‘𝐵)‘𝑦) = (Base‘𝐴))
329	288, 328	eleqtrrd 2834	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ ((LSpan‘𝐵)‘𝑦))
330		eqid 2736	. . . . . . . . . . . . 13 ⊢ (Scalar‘𝐵) = (Scalar‘𝐵)
331		lveclmod 20097	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ LVec → 𝐵 ∈ LMod)
332	28, 331	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ LMod)
333	332	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐵 ∈ LMod)
334	321, 60, 88, 330, 91, 89, 333, 62	ellspds 31232	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑧 ∈ ((LSpan‘𝐵)‘𝑦) ↔ ∃𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)(𝑎 finSupp (0_g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤))))))
335	334	biimpa 480	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ ((LSpan‘𝐵)‘𝑦)) → ∃𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)(𝑎 finSupp (0_g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))))
336	205, 329, 335	syl2anc 587	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ∃𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑦)(𝑎 finSupp (0_g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σ_g (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·_𝑠 ‘𝐵)𝑤)))))
337	320, 336	r19.29a 3198	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥))(𝑐 finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))))
338		eqid 2736	. . . . . . . . . . 11 ⊢ (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴))
339	202, 187, 338, 188, 191, 189, 87, 170, 157	ellspd 20718	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑧 ∈ ((LSpan‘𝐴)‘((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) “ (𝑦 × 𝑥))) ↔ ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥))(𝑐 finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))))))
340	339	adantr 484	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑧 ∈ ((LSpan‘𝐴)‘((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) “ (𝑦 × 𝑥))) ↔ ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑦 × 𝑥))(𝑐 finSupp (0_g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σ_g (𝑐 ∘_f ( ·_𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))))))
341	337, 340	mpbird 260	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ ((LSpan‘𝐴)‘((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) “ (𝑦 × 𝑥))))
342	87	ffnd 6524	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) Fn (𝑦 × 𝑥))
343	342	adantr 484	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) Fn (𝑦 × 𝑥))
344		fnima 6486	. . . . . . . . . 10 ⊢ ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) Fn (𝑦 × 𝑥) → ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) “ (𝑦 × 𝑥)) = ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))
345	343, 344	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) “ (𝑦 × 𝑥)) = ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))
346	345	fveq2d 6699	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((LSpan‘𝐴)‘((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) “ (𝑦 × 𝑥))) = ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))
347	341, 346	eleqtrd 2833	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))
348	204, 347	eqelssd 3908	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = (Base‘𝐴))
349		eqid 2736	. . . . . . 7 ⊢ (Base‘(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = (Base‘(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)))
350		drngnzr 20254	. . . . . . . . . 10 ⊢ (𝐾 ∈ DivRing → 𝐾 ∈ NzRing)
351	14, 350	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ NzRing)
352	258, 351	eqeltrrd 2832	. . . . . . . 8 ⊢ (𝜑 → (Scalar‘𝐴) ∈ NzRing)
353	352	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Scalar‘𝐴) ∈ NzRing)
354	187, 349, 188, 189, 190, 191, 202, 170, 353, 157, 156	lindflbs 31242	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ∈ (LBasis‘𝐴) ↔ ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) LIndF 𝐴 ∧ ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))) = (Base‘𝐴))))
355	195, 348, 354	mpbir2and 713	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ∈ (LBasis‘𝐴))
356		eqid 2736	. . . . . 6 ⊢ (LBasis‘𝐴) = (LBasis‘𝐴)
357	356	dimval 31354	. . . . 5 ⊢ ((𝐴 ∈ LVec ∧ ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤)) ∈ (LBasis‘𝐴)) → (dim‘𝐴) = (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))
358	167, 355, 357	syl2anc 587	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐴) = (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(._r‘𝐸)𝑤))))
359	29	dimval 31354	. . . . . 6 ⊢ ((𝐵 ∈ LVec ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐵) = (♯‘𝑦))
360	92, 59, 359	syl2anc 587	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐵) = (♯‘𝑦))
361	20	dimval 31354	. . . . . 6 ⊢ ((𝐶 ∈ LVec ∧ 𝑥 ∈ (LBasis‘𝐶)) → (dim‘𝐶) = (♯‘𝑥))
362	110, 38, 361	syl2anc 587	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐶) = (♯‘𝑥))
363	360, 362	oveq12d 7209	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((dim‘𝐵) ·_e (dim‘𝐶)) = ((♯‘𝑦) ·_e (♯‘𝑥)))
364	164, 358, 363	3eqtr4d 2781	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐴) = ((dim‘𝐵) ·_e (dim‘𝐶)))
365	34, 364	exlimddv 1943	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) → (dim‘𝐴) = ((dim‘𝐵) ·_e (dim‘𝐶)))
366	24, 365	exlimddv 1943	1 ⊢ (𝜑 → (dim‘𝐴) = ((dim‘𝐵) ·_e (dim‘𝐶)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1089 = wceq 1543 ∃wex 1787 ∈ wcel 2112 ≠ wne 2932 ∀wral 3051 ∃wrex 3052 Vcvv 3398 ⊆ wss 3853 ∅c0 4223 {csn 4527 class class class wbr 5039 ↦ cmpt 5120 × cxp 5534 ran crn 5537 “ cima 5539 Fn wfn 6353 ⟶wf 6354 –1-1→wf1 6355 ‘cfv 6358 (class class class)co 7191 ∈ cmpo 7193 ∘_f cof 7445 ↑_m cmap 8486 ≈ cen 8601 finSupp cfsupp 8963 ·_e cxmu 12668 ♯chash 13861 Basecbs 16666 ↾_s cress 16667 +_gcplusg 16749 ._rcmulr 16750 Scalarcsca 16752 ·_𝑠 cvsca 16753 0_gc0g 16898 Σ_g cgsu 16899 Ringcrg 19516 DivRingcdr 19721 SubRingcsubrg 19750 LModclmod 19853 LSpanclspn 19962 LBasisclbs 20065 LVecclvec 20093 subringAlg csra 20159 NzRingcnzr 20249 freeLMod cfrlm 20662 LIndF clindf 20720 LIndSclinds 20721 dimcldim 31352

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2708 ax-rep 5164 ax-sep 5177 ax-nul 5184 ax-pow 5243 ax-pr 5307 ax-un 7501 ax-reg 9186 ax-inf2 9234 ax-ac2 10042 ax-cnex 10750 ax-resscn 10751 ax-1cn 10752 ax-icn 10753 ax-addcl 10754 ax-addrcl 10755 ax-mulcl 10756 ax-mulrcl 10757 ax-mulcom 10758 ax-addass 10759 ax-mulass 10760 ax-distr 10761 ax-i2m1 10762 ax-1ne0 10763 ax-1rid 10764 ax-rnegex 10765 ax-rrecex 10766 ax-cnre 10767 ax-pre-lttri 10768 ax-pre-lttrn 10769 ax-pre-ltadd 10770 ax-pre-mulgt0 10771

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2728 df-clel 2809 df-nfc 2879 df-ne 2933 df-nel 3037 df-ral 3056 df-rex 3057 df-reu 3058 df-rmo 3059 df-rab 3060 df-v 3400 df-sbc 3684 df-csb 3799 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-pss 3872 df-nul 4224 df-if 4426 df-pw 4501 df-sn 4528 df-pr 4530 df-tp 4532 df-op 4534 df-uni 4806 df-int 4846 df-iun 4892 df-iin 4893 df-br 5040 df-opab 5102 df-mpt 5121 df-tr 5147 df-id 5440 df-eprel 5445 df-po 5453 df-so 5454 df-fr 5494 df-se 5495 df-we 5496 df-xp 5542 df-rel 5543 df-cnv 5544 df-co 5545 df-dm 5546 df-rn 5547 df-res 5548 df-ima 5549 df-pred 6140 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6316 df-fun 6360 df-fn 6361 df-f 6362 df-f1 6363 df-fo 6364 df-f1o 6365 df-fv 6366 df-isom 6367 df-riota 7148 df-ov 7194 df-oprab 7195 df-mpo 7196 df-of 7447 df-rpss 7489 df-om 7623 df-1st 7739 df-2nd 7740 df-supp 7882 df-tpos 7946 df-wrecs 8025 df-recs 8086 df-rdg 8124 df-1o 8180 df-oadd 8184 df-er 8369 df-map 8488 df-ixp 8557 df-en 8605 df-dom 8606 df-sdom 8607 df-fin 8608 df-fsupp 8964 df-sup 9036 df-oi 9104 df-r1 9345 df-rank 9346 df-dju 9482 df-card 9520 df-acn 9523 df-ac 9695 df-pnf 10834 df-mnf 10835 df-xr 10836 df-ltxr 10837 df-le 10838 df-sub 11029 df-neg 11030 df-nn 11796 df-2 11858 df-3 11859 df-4 11860 df-5 11861 df-6 11862 df-7 11863 df-8 11864 df-9 11865 df-n0 12056 df-xnn0 12128 df-z 12142 df-dec 12259 df-uz 12404 df-xmul 12671 df-fz 13061 df-fzo 13204 df-seq 13540 df-hash 13862 df-struct 16668 df-ndx 16669 df-slot 16670 df-base 16672 df-sets 16673 df-ress 16674 df-plusg 16762 df-mulr 16763 df-sca 16765 df-vsca 16766 df-ip 16767 df-tset 16768 df-ple 16769 df-ocomp 16770 df-ds 16771 df-hom 16773 df-cco 16774 df-0g 16900 df-gsum 16901 df-prds 16906 df-pws 16908 df-mre 17043 df-mrc 17044 df-mri 17045 df-acs 17046 df-proset 17756 df-drs 17757 df-poset 17774 df-ipo 17988 df-mgm 18068 df-sgrp 18117 df-mnd 18128 df-mhm 18172 df-submnd 18173 df-grp 18322 df-minusg 18323 df-sbg 18324 df-mulg 18443 df-subg 18494 df-ghm 18574 df-cntz 18665 df-cmn 19126 df-abl 19127 df-mgp 19459 df-ur 19471 df-ring 19518 df-oppr 19595 df-dvdsr 19613 df-unit 19614 df-invr 19644 df-drng 19723 df-subrg 19752 df-lmod 19855 df-lss 19923 df-lsp 19963 df-lmhm 20013 df-lbs 20066 df-lvec 20094 df-sra 20163 df-rgmod 20164 df-nzr 20250 df-dsmm 20648 df-frlm 20663 df-uvc 20699 df-lindf 20722 df-linds 20723 df-dim 31353

This theorem is referenced by: extdgmul 31404

W3C validator