Theorem fedgmul 33822

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 20577	. . . . . . . . . . 11 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (𝑉 ∈ (SubRing‘𝐹) ↔ (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈)))
6	5	biimpa 477	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ∈ (SubRing‘𝐹)) → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))
7	2, 3, 6	syl2anc 590	. . . . . . . . 9 ⊢ (𝜑 → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))
8	7	simprd 496	. . . . . . . 8 ⊢ (𝜑 → 𝑉 ⊆ 𝑈)
9		ressabs 17216	. . . . . . . 8 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈) → ((𝐸 ↾s 𝑈) ↾s 𝑉) = (𝐸 ↾s 𝑉))
10	2, 8, 9	syl2anc 590	. . . . . . 7 ⊢ (𝜑 → ((𝐸 ↾s 𝑈) ↾s 𝑉) = (𝐸 ↾s 𝑉))
11	4	oveq1i 7373	. . . . . . 7 ⊢ (𝐹 ↾s 𝑉) = ((𝐸 ↾s 𝑈) ↾s 𝑉)
12		fedgmul.k	. . . . . . 7 ⊢ 𝐾 = (𝐸 ↾s 𝑉)
13	10, 11, 12	3eqtr4g 2800	. . . . . 6 ⊢ (𝜑 → (𝐹 ↾s 𝑉) = 𝐾)
14		fedgmul.3	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ DivRing)
15	13, 14	eqeltrd 2840	. . . . 5 ⊢ (𝜑 → (𝐹 ↾s 𝑉) ∈ DivRing)
16		fedgmul.c	. . . . . 6 ⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
17		eqid 2740	. . . . . 6 ⊢ (𝐹 ↾s 𝑉) = (𝐹 ↾s 𝑉)
18	16, 17	sralvec 33776	. . . . 5 ⊢ ((𝐹 ∈ DivRing ∧ (𝐹 ↾s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
19	1, 15, 3, 18	syl3anc 1379	. . . 4 ⊢ (𝜑 → 𝐶 ∈ LVec)
20		eqid 2740	. . . . 5 ⊢ (LBasis‘𝐶) = (LBasis‘𝐶)
21	20	lbsex 21165	. . . 4 ⊢ (𝐶 ∈ LVec → (LBasis‘𝐶) ≠ ∅)
22	19, 21	syl 17	. . 3 ⊢ (𝜑 → (LBasis‘𝐶) ≠ ∅)
23		n0 4288	. . 3 ⊢ ((LBasis‘𝐶) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (LBasis‘𝐶))
24	22, 23	sylib 219	. 2 ⊢ (𝜑 → ∃𝑥 𝑥 ∈ (LBasis‘𝐶))
25		fedgmul.1	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ DivRing)
26		fedgmul.b	. . . . . . . 8 ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
27	26, 4	sralvec 33776	. . . . . . 7 ⊢ ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐵 ∈ LVec)
28	25, 1, 2, 27	syl3anc 1379	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ LVec)
29		eqid 2740	. . . . . . 7 ⊢ (LBasis‘𝐵) = (LBasis‘𝐵)
30	29	lbsex 21165	. . . . . 6 ⊢ (𝐵 ∈ LVec → (LBasis‘𝐵) ≠ ∅)
31	28, 30	syl 17	. . . . 5 ⊢ (𝜑 → (LBasis‘𝐵) ≠ ∅)
32		n0 4288	. . . . 5 ⊢ ((LBasis‘𝐵) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (LBasis‘𝐵))
33	31, 32	sylib 219	. . . 4 ⊢ (𝜑 → ∃𝑦 𝑦 ∈ (LBasis‘𝐵))
34	33	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) → ∃𝑦 𝑦 ∈ (LBasis‘𝐵))
35		drngring 20715	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
36	25, 35	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ∈ Ring)
37	36	ad4antr 738	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝐸 ∈ Ring)
38		simplr 774	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ∈ (LBasis‘𝐶))
39		eqid 2740	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝐶) = (Base‘𝐶)
40	39, 20	lbsss 21074	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (LBasis‘𝐶) → 𝑥 ⊆ (Base‘𝐶))
41	38, 40	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ⊆ (Base‘𝐶))
42		eqid 2740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Base‘𝐸) = (Base‘𝐸)
43	42	subrgss 20551	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
44	2, 43	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐸))
45	4, 42	ressbas2 17206	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
46	44, 45	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑈 = (Base‘𝐹))
47	16	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐶 = ((subringAlg ‘𝐹)‘𝑉))
48		eqid 2740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Base‘𝐹) = (Base‘𝐹)
49	48	subrgss 20551	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
50	3, 49	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐹))
51	47, 50	srabase 21174	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Base‘𝐹) = (Base‘𝐶))
52	46, 51	eqtrd 2775	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 = (Base‘𝐶))
53	52, 44	eqsstrrd 3957	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
54	53	ad2antrr 732	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘𝐶) ⊆ (Base‘𝐸))
55	41, 54	sstrd 3932	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ⊆ (Base‘𝐸))
56	55	ad2antrr 732	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑥 ⊆ (Base‘𝐸))
57		simpr 485	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑖 ∈ 𝑥)
58	56, 57	sseldd 3923	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑖 ∈ (Base‘𝐸))
59		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ∈ (LBasis‘𝐵))
60		eqid 2740	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝐵) = (Base‘𝐵)
61	60, 29	lbsss 21074	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (LBasis‘𝐵) → 𝑦 ⊆ (Base‘𝐵))
62	59, 61	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ⊆ (Base‘𝐵))
63	26	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 = ((subringAlg ‘𝐸)‘𝑈))
64	63, 44	srabase 21174	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐵))
65	64	ad2antrr 732	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘𝐸) = (Base‘𝐵))
66	62, 65	sseqtrrd 3959	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ⊆ (Base‘𝐸))
67	66	ad2antrr 732	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑦 ⊆ (Base‘𝐸))
68		simplr 774	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑗 ∈ 𝑦)
69	67, 68	sseldd 3923	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑗 ∈ (Base‘𝐸))
70		eqid 2740	. . . . . . . . . . . . . 14 ⊢ (.r‘𝐸) = (.r‘𝐸)
71	42, 70	ringcl 20229	. . . . . . . . . . . . 13 ⊢ ((𝐸 ∈ Ring ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸)) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐸))
72	37, 58, 69, 71	syl3anc 1379	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐸))
73		fedgmul.a	. . . . . . . . . . . . . . 15 ⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑉)
74	73	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝐸)‘𝑉))
75	7	simpld 495	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐸))
76	42	subrgss 20551	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
77	75, 76	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐸))
78	74, 77	srabase 21174	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐴))
79	78	ad4antr 738	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (Base‘𝐸) = (Base‘𝐴))
80	72, 79	eleqtrd 2842	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴))
81	80	anasss 467	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴))
82	81	ralrimivva 3183	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴))
83		oveq2 7371	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑗 → (𝑡(.r‘𝐸)𝑤) = (𝑡(.r‘𝐸)𝑗))
84		oveq1 7370	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑖 → (𝑡(.r‘𝐸)𝑗) = (𝑖(.r‘𝐸)𝑗))
85	83, 84	cbvmpov 7458	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) = (𝑗 ∈ 𝑦, 𝑖 ∈ 𝑥 ↦ (𝑖(.r‘𝐸)𝑗))
86	85	fmpo 8017	. . . . . . . . 9 ⊢ (∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴) ↔ (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴))
87	82, 86	sylib 219	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴))
88		eqid 2740	. . . . . . . . . . . . . 14 ⊢ (Base‘(Scalar‘𝐵)) = (Base‘(Scalar‘𝐵))
89		eqid 2740	. . . . . . . . . . . . . 14 ⊢ ( ·𝑠 ‘𝐵) = ( ·𝑠 ‘𝐵)
90		eqid 2740	. . . . . . . . . . . . . 14 ⊢ (+g‘𝐵) = (+g‘𝐵)
91		eqid 2740	. . . . . . . . . . . . . 14 ⊢ (0g‘(Scalar‘𝐵)) = (0g‘(Scalar‘𝐵))
92	28	ad2antrr 732	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐵 ∈ LVec)
93	92	ad5antr 740	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → 𝐵 ∈ LVec)
94	29	lbslinds 21815	. . . . . . . . . . . . . . . 16 ⊢ (LBasis‘𝐵) ⊆ (LIndS‘𝐵)
95	94, 59	sselid 3920	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑦 ∈ (LIndS‘𝐵))
96	95	ad5antr 740	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → 𝑦 ∈ (LIndS‘𝐵))
97	68	ad3antrrr 736	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → 𝑗 ∈ 𝑦)
98		simpllr 781	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → 𝑣 ∈ 𝑦)
99	63, 44	srasca 21177	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ↾s 𝑈) = (Scalar‘𝐵))
100	4, 99	eqtrid 2787	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 = (Scalar‘𝐵))
101	100	fveq2d 6838	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Base‘𝐹) = (Base‘(Scalar‘𝐵)))
102	101, 51	eqtr3d 2777	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Base‘(Scalar‘𝐵)) = (Base‘𝐶))
103	102	ad2antrr 732	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘(Scalar‘𝐵)) = (Base‘𝐶))
104	41, 103	sseqtrrd 3959	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ⊆ (Base‘(Scalar‘𝐵)))
105	104	ad5antr 740	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → 𝑥 ⊆ (Base‘(Scalar‘𝐵)))
106		simp-4r 789	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → 𝑖 ∈ 𝑥)
107	105, 106	sseldd 3923	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → 𝑖 ∈ (Base‘(Scalar‘𝐵)))
108		simplr 774	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → 𝑢 ∈ 𝑥)
109	105, 108	sseldd 3923	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → 𝑢 ∈ (Base‘(Scalar‘𝐵)))
110	19	ad2antrr 732	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐶 ∈ LVec)
111		eqid 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (LSpan‘𝐶) = (LSpan‘𝐶)
112	39, 20, 111	islbs4 21814	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (LBasis‘𝐶) ↔ (𝑥 ∈ (LIndS‘𝐶) ∧ ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶)))
113	38, 112	sylib 219	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑥 ∈ (LIndS‘𝐶) ∧ ((LSpan‘𝐶)‘𝑥) = (Base‘𝐶)))
114	113	simpld 495	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝑥 ∈ (LIndS‘𝐶))
115		eqid 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ (0g‘𝐶) = (0g‘𝐶)
116	115	0nellinds 33460	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐶 ∈ LVec ∧ 𝑥 ∈ (LIndS‘𝐶)) → ¬ (0g‘𝐶) ∈ 𝑥)
117	110, 114, 116	syl2anc 590	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ¬ (0g‘𝐶) ∈ 𝑥)
118	117	ad5antr 740	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → ¬ (0g‘𝐶) ∈ 𝑥)
119		nelne2 3033	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ 𝑥 ∧ ¬ (0g‘𝐶) ∈ 𝑥) → 𝑖 ≠ (0g‘𝐶))
120	106, 118, 119	syl2anc 590	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → 𝑖 ≠ (0g‘𝐶))
121	100	fveq2d 6838	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0g‘𝐹) = (0g‘(Scalar‘𝐵)))
122	16, 1, 3	drgext0g 33781	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0g‘𝐹) = (0g‘𝐶))
123	121, 122	eqtr3d 2777	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0g‘(Scalar‘𝐵)) = (0g‘𝐶))
124	123	ad7antr 744	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → (0g‘(Scalar‘𝐵)) = (0g‘𝐶))
125	120, 124	neeqtrrd 3009	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → 𝑖 ≠ (0g‘(Scalar‘𝐵)))
126		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢))
127		ovexd 7398	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → (𝑖(.r‘𝐸)𝑗) ∈ V)
128	85	ovmpt4g 7510	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥 ∧ (𝑖(.r‘𝐸)𝑗) ∈ V) → (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑖(.r‘𝐸)𝑗))
129	97, 106, 127, 128	syl3anc 1379	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑖(.r‘𝐸)𝑗))
130	26, 25, 2	drgextvsca 33782	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (.r‘𝐸) = ( ·𝑠 ‘𝐵))
131	130	oveqd 7380	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑖(.r‘𝐸)𝑗) = (𝑖( ·𝑠 ‘𝐵)𝑗))
132	131	ad7antr 744	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → (𝑖(.r‘𝐸)𝑗) = (𝑖( ·𝑠 ‘𝐵)𝑗))
133	129, 132	eqtrd 2775	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑖( ·𝑠 ‘𝐵)𝑗))
134	85	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) = (𝑗 ∈ 𝑦, 𝑖 ∈ 𝑥 ↦ (𝑖(.r‘𝐸)𝑗)))
135		simprr 778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)) → 𝑖 = 𝑢)
136		simprl 776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)) → 𝑗 = 𝑣)
137	135, 136	oveq12d 7381	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)) → (𝑖(.r‘𝐸)𝑗) = (𝑢(.r‘𝐸)𝑣))
138		simplr 774	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → 𝑣 ∈ 𝑦)
139		simpr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → 𝑢 ∈ 𝑥)
140		ovexd 7398	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑢(.r‘𝐸)𝑣) ∈ V)
141	134, 137, 138, 139, 140	ovmpod 7515	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢) = (𝑢(.r‘𝐸)𝑣))
142	141	adantllr 725	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢) = (𝑢(.r‘𝐸)𝑣))
143	142	adantl3r 756	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢) = (𝑢(.r‘𝐸)𝑣))
144	143	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢) = (𝑢(.r‘𝐸)𝑣))
145	130	oveqd 7380	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑢(.r‘𝐸)𝑣) = (𝑢( ·𝑠 ‘𝐵)𝑣))
146	145	ad7antr 744	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → (𝑢(.r‘𝐸)𝑣) = (𝑢( ·𝑠 ‘𝐵)𝑣))
147	144, 146	eqtrd 2775	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢) = (𝑢( ·𝑠 ‘𝐵)𝑣))
148	126, 133, 147	3eqtr3d 2783	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → (𝑖( ·𝑠 ‘𝐵)𝑗) = (𝑢( ·𝑠 ‘𝐵)𝑣))
149	88, 89, 90, 91, 93, 96, 97, 98, 107, 109, 125, 148	linds2eq 33471	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) ∧ (𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢)) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢))
150	149	ex 413	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ 𝑣 ∈ 𝑦) ∧ 𝑢 ∈ 𝑥) → ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
151	150	anasss 467	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) ∧ (𝑣 ∈ 𝑦 ∧ 𝑢 ∈ 𝑥)) → ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
152	151	ralrimivva 3183	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → ∀𝑣 ∈ 𝑦 ∀𝑢 ∈ 𝑥 ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
153	152	anasss 467	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → ∀𝑣 ∈ 𝑦 ∀𝑢 ∈ 𝑥 ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
154	153	ralrimivva 3183	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 ∀𝑣 ∈ 𝑦 ∀𝑢 ∈ 𝑥 ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢)))
155		f1opr 7419	. . . . . . . 8 ⊢ ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)):(𝑦 × 𝑥)–1-1→(Base‘𝐴) ↔ ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴) ∧ ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 ∀𝑣 ∈ 𝑦 ∀𝑢 ∈ 𝑥 ((𝑗(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑖) = (𝑣(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))𝑢) → (𝑗 = 𝑣 ∧ 𝑖 = 𝑢))))
156	87, 154, 155	sylanbrc 589	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)):(𝑦 × 𝑥)–1-1→(Base‘𝐴))
157	59, 38	xpexd 7701	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑦 × 𝑥) ∈ V)
158		f1rnen 32727	. . . . . . 7 ⊢ (((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)):(𝑦 × 𝑥)–1-1→(Base‘𝐴) ∧ (𝑦 × 𝑥) ∈ V) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) ≈ (𝑦 × 𝑥))
159	156, 157, 158	syl2anc 590	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) ≈ (𝑦 × 𝑥))
160		hasheni 14308	. . . . . 6 ⊢ (ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) ≈ (𝑦 × 𝑥) → (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))) = (♯‘(𝑦 × 𝑥)))
161	159, 160	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))) = (♯‘(𝑦 × 𝑥)))
162		hashxpe 32906	. . . . . 6 ⊢ ((𝑦 ∈ (LBasis‘𝐵) ∧ 𝑥 ∈ (LBasis‘𝐶)) → (♯‘(𝑦 × 𝑥)) = ((♯‘𝑦) ·e (♯‘𝑥)))
163	59, 38, 162	syl2anc 590	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (♯‘(𝑦 × 𝑥)) = ((♯‘𝑦) ·e (♯‘𝑥)))
164	161, 163	eqtrd 2775	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))) = ((♯‘𝑦) ·e (♯‘𝑥)))
165	73, 12	sralvec 33776	. . . . . . 7 ⊢ ((𝐸 ∈ DivRing ∧ 𝐾 ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec)
166	25, 14, 75, 165	syl3anc 1379	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ LVec)
167	166	ad2antrr 732	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐴 ∈ LVec)
168		lveclmod 21103	. . . . . . . . 9 ⊢ (𝐴 ∈ LVec → 𝐴 ∈ LMod)
169	166, 168	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ LMod)
170	169	ad2antrr 732	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐴 ∈ LMod)
171	25	ad4antr 738	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴)) → 𝐸 ∈ DivRing)
172	1	ad4antr 738	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴)) → 𝐹 ∈ DivRing)
173	14	ad4antr 738	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴)) → 𝐾 ∈ DivRing)
174	2	ad4antr 738	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴)) → 𝑈 ∈ (SubRing‘𝐸))
175	3	ad4antr 738	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴)) → 𝑉 ∈ (SubRing‘𝐹))
176		fveq2 6834	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑗 → (𝑓‘𝑤) = (𝑓‘𝑗))
177	176	fveq1d 6836	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑗 → ((𝑓‘𝑤)‘𝑣) = ((𝑓‘𝑗)‘𝑣))
178		fveq2 6834	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑖 → ((𝑓‘𝑗)‘𝑣) = ((𝑓‘𝑗)‘𝑖))
179	177, 178	cbvmpov 7458	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) = (𝑗 ∈ 𝑦, 𝑖 ∈ 𝑥 ↦ ((𝑓‘𝑗)‘𝑖))
180		simp-4r 789	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴)) → 𝑥 ∈ (LBasis‘𝐶))
181		simpllr 781	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴)) → 𝑦 ∈ (LBasis‘𝐵))
182		simplr 774	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴)) → 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥))))
183		simpr 485	. . . . . . . . . 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 33821	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) ∧ (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴)) → 𝑐 = ((𝑦 × 𝑥) × {(0g‘(Scalar‘𝐴))}))
185	184	ex 413	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))) → ((𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0g‘(Scalar‘𝐴))})))
186	185	ralrimiva 3132	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))((𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0g‘(Scalar‘𝐴))})))
187		eqid 2740	. . . . . . . . 9 ⊢ (Base‘𝐴) = (Base‘𝐴)
188		eqid 2740	. . . . . . . . 9 ⊢ (Scalar‘𝐴) = (Scalar‘𝐴)
189		eqid 2740	. . . . . . . . 9 ⊢ ( ·𝑠 ‘𝐴) = ( ·𝑠 ‘𝐴)
190		eqid 2740	. . . . . . . . 9 ⊢ (0g‘𝐴) = (0g‘𝐴)
191		eqid 2740	. . . . . . . . 9 ⊢ (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐴))
192		eqid 2740	. . . . . . . . 9 ⊢ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥))) = (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))
193	187, 188, 189, 190, 191, 192	islindf4 21820	. . . . . . . 8 ⊢ ((𝐴 ∈ LMod ∧ (𝑦 × 𝑥) ∈ V ∧ (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴)) → ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) LIndF 𝐴 ↔ ∀𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))((𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0g‘(Scalar‘𝐴))}))))
194	193	biimpar 478	. . . . . . 7 ⊢ (((𝐴 ∈ LMod ∧ (𝑦 × 𝑥) ∈ V ∧ (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)):(𝑦 × 𝑥)⟶(Base‘𝐴)) ∧ ∀𝑐 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑦 × 𝑥)))((𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))) = (0g‘𝐴) → 𝑐 = ((𝑦 × 𝑥) × {(0g‘(Scalar‘𝐴))}))) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) LIndF 𝐴)
195	170, 157, 87, 186, 194	syl31anc 1381	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) LIndF 𝐴)
196	72	anasss 467	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐸))
197	196	ralrimivva 3183	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐸))
198	85	rnmposs 32772	. . . . . . . . . 10 ⊢ (∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐸) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) ⊆ (Base‘𝐸))
199	197, 198	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) ⊆ (Base‘𝐸))
200	78	ad2antrr 732	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Base‘𝐸) = (Base‘𝐴))
201	199, 200	sseqtrd 3958	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) ⊆ (Base‘𝐴))
202		eqid 2740	. . . . . . . . 9 ⊢ (LSpan‘𝐴) = (LSpan‘𝐴)
203	187, 202	lspssv 20980	. . . . . . . 8 ⊢ ((𝐴 ∈ LMod ∧ ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) ⊆ (Base‘𝐴)) → ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))) ⊆ (Base‘𝐴))
204	170, 201, 203	syl2anc 590	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))) ⊆ (Base‘𝐴))
205		simpl 483	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)))
206	205	ad4antr 738	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → ((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)))
207		elmapi 8793	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦) → 𝑎:𝑦⟶(Base‘(Scalar‘𝐵)))
208	207	ad4antlr 739	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → 𝑎:𝑦⟶(Base‘(Scalar‘𝐵)))
209		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → 𝑗 ∈ 𝑦)
210	208, 209	ffvelcdmd 7033	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → (𝑎‘𝑗) ∈ (Base‘(Scalar‘𝐵)))
211	113	simprd 496	. . . . . . . . . . . . . . . . . 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 744	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → (Base‘(Scalar‘𝐵)) = (Base‘𝐶))
214	212, 213	eqtr4d 2778	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → ((LSpan‘𝐶)‘𝑥) = (Base‘(Scalar‘𝐵)))
215	210, 214	eleqtrrd 2843	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → (𝑎‘𝑗) ∈ ((LSpan‘𝐶)‘𝑥))
216		eqid 2740	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
217		eqid 2740	. . . . . . . . . . . . . . . . 17 ⊢ (Scalar‘𝐶) = (Scalar‘𝐶)
218		eqid 2740	. . . . . . . . . . . . . . . . 17 ⊢ (0g‘(Scalar‘𝐶)) = (0g‘(Scalar‘𝐶))
219		eqid 2740	. . . . . . . . . . . . . . . . 17 ⊢ ( ·𝑠 ‘𝐶) = ( ·𝑠 ‘𝐶)
220		lveclmod 21103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 ∈ LVec → 𝐶 ∈ LMod)
221	19, 220	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐶 ∈ LMod)
222	221	ad2antrr 732	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐶 ∈ LMod)
223	111, 39, 216, 217, 218, 219, 222, 41	ellspds 33458	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((𝑎‘𝑗) ∈ ((LSpan‘𝐶)‘𝑥) ↔ ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖))))))
224	223	biimpa 477	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ (𝑎‘𝑗) ∈ ((LSpan‘𝐶)‘𝑥)) → ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖)))))
225	206, 215, 224	syl2anc 590	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑗 ∈ 𝑦) → ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖)))))
226	225	ralrimiva 3132	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) → ∀𝑗 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖)))))
227		fveq2 6834	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑗 → (𝑎‘𝑤) = (𝑎‘𝑗))
228		fveq2 6834	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑖 → (𝑏‘𝑣) = (𝑏‘𝑖))
229		id 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑖 → 𝑣 = 𝑖)
230	228, 229	oveq12d 7381	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = 𝑖 → ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣) = ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖))
231	230	cbvmptv 5183	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣)) = (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖))
232	231	oveq2i 7374	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 Σg (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣))) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖)))
233	232	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑗 → (𝐶 Σg (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣))) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖))))
234	227, 233	eqeq12d 2756	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑗 → ((𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣))) ↔ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖)))))
235	234	anbi2d 636	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑗 → ((𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣)))) ↔ (𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖))))))
236	235	rexbidv 3164	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑗 → (∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣)))) ↔ ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖))))))
237	236	cbvralvw 3218	. . . . . . . . . . . . . 14 ⊢ (∀𝑤 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣)))) ↔ ∀𝑗 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ ((𝑏‘𝑖)( ·𝑠 ‘𝐶)𝑖)))))
238		vex 3436	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
239		breq1 5082	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑓‘𝑤) → (𝑏 finSupp (0g‘(Scalar‘𝐶)) ↔ (𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶))))
240		fveq1 6833	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (𝑓‘𝑤) → (𝑏‘𝑣) = ((𝑓‘𝑤)‘𝑣))
241	240	oveq1d 7378	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑓‘𝑤) → ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣) = (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))
242	241	mpteq2dv 5173	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑓‘𝑤) → (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣)) = (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣)))
243	242	oveq2d 7379	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑓‘𝑤) → (𝐶 Σg (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣))) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))
244	243	eqeq2d 2751	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑓‘𝑤) → ((𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣))) ↔ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣)))))
245	239, 244	anbi12d 638	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑓‘𝑤) → ((𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣)))) ↔ ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))))
246	238, 245	ac6s 10404	. . . . . . . . . . . . . 14 ⊢ (∀𝑤 ∈ 𝑦 ∃𝑏 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥)(𝑏 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ ((𝑏‘𝑣)( ·𝑠 ‘𝐶)𝑣)))) → ∃𝑓(𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))))
247	237, 246	sylbir 236	. . . . . . . . . . . . 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 781	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥))
250		simplr 774	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → 𝑗 ∈ 𝑦)
251	249, 250	ffvelcdmd 7033	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (𝑓‘𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥))
252		elmapi 8793	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓‘𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑥) → (𝑓‘𝑗):𝑥⟶(Base‘(Scalar‘𝐶)))
253	251, 252	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ 𝑗 ∈ 𝑦) ∧ 𝑖 ∈ 𝑥) → (𝑓‘𝑗):𝑥⟶(Base‘(Scalar‘𝐶)))
254	253	anasss 467	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → (𝑓‘𝑗):𝑥⟶(Base‘(Scalar‘𝐶)))
255		simprr 778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → 𝑖 ∈ 𝑥)
256	254, 255	ffvelcdmd 7033	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → ((𝑓‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐶)))
257	74, 77	srasca 21177	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐸 ↾s 𝑉) = (Scalar‘𝐴))
258	12, 257	eqtrid 2787	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐴))
259	47, 50	srasca 21177	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐹 ↾s 𝑉) = (Scalar‘𝐶))
260	13, 259	eqtr3d 2777	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐶))
261	258, 260	eqtr3d 2777	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
262	261	fveq2d 6838	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
263	262	ad4antr 738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
264	256, 263	eleqtrrd 2843	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ (𝑗 ∈ 𝑦 ∧ 𝑖 ∈ 𝑥)) → ((𝑓‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
265	264	ralrimivva 3183	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → ∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 ((𝑓‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
266	179	fmpo 8017	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑗 ∈ 𝑦 ∀𝑖 ∈ 𝑥 ((𝑓‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)) ↔ (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)):(𝑦 × 𝑥)⟶(Base‘(Scalar‘𝐴)))
267	265, 266	sylib 219	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)):(𝑦 × 𝑥)⟶(Base‘(Scalar‘𝐴)))
268		fvexd 6849	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → (Base‘(Scalar‘𝐴)) ∈ V)
269	157	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → (𝑦 × 𝑥) ∈ V)
270	268, 269	elmapd 8784	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥)) ↔ (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)):(𝑦 × 𝑥)⟶(Base‘(Scalar‘𝐴))))
271	267, 270	mpbird 258	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥)))
272	271	ad5ant15 764	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) → (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥)))
273	272	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥)))
274	273	adantl3r 756	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥)))
275		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) ∧ 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣))) → 𝑐 = (𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)))
276	275	breq1d 5089	. . . . . . . . . . . . . . 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 7378	. . . . . . . . . . . . . . . . 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 7379	. . . . . . . . . . . . . . . 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 2751	. . . . . . . . . . . . . . 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 638	. . . . . . . . . . . . . 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 746	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝐸 ∈ DivRing)
282	1	ad8antr 746	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝐹 ∈ DivRing)
283	14	ad8antr 746	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝐾 ∈ DivRing)
284	2	ad8antr 746	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝑈 ∈ (SubRing‘𝐸))
285	3	ad8antr 746	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝑉 ∈ (SubRing‘𝐹))
286	38	ad6antr 742	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝑥 ∈ (LBasis‘𝐶))
287	59	ad6antr 742	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝑦 ∈ (LBasis‘𝐵))
288		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ (Base‘𝐴))
289	288	ad5antr 740	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝑧 ∈ (Base‘𝐴))
290	207	ad5antlr 741	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝑎:𝑦⟶(Base‘(Scalar‘𝐵)))
291		simp-4r 789	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝑎 finSupp (0g‘(Scalar‘𝐵)))
292		simpllr 781	. . . . . . . . . . . . . . . 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 7381	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑗 → ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤) = ((𝑎‘𝑗)( ·𝑠 ‘𝐵)𝑗))
295	294	cbvmptv 5183	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)) = (𝑗 ∈ 𝑦 ↦ ((𝑎‘𝑗)( ·𝑠 ‘𝐵)𝑗))
296	295	oveq2i 7374	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤))) = (𝐵 Σg (𝑗 ∈ 𝑦 ↦ ((𝑎‘𝑗)( ·𝑠 ‘𝐵)𝑗)))
297	292, 296	eqtrdi 2791	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝑧 = (𝐵 Σg (𝑗 ∈ 𝑦 ↦ ((𝑎‘𝑗)( ·𝑠 ‘𝐵)𝑗))))
298		simplr 774	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥))
299	176	breq1d 5089	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑗 → ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ↔ (𝑓‘𝑗) finSupp (0g‘(Scalar‘𝐶))))
300		fveq2 6834	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = 𝑖 → ((𝑓‘𝑤)‘𝑣) = ((𝑓‘𝑤)‘𝑖))
301	300, 229	oveq12d 7381	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 = 𝑖 → (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣) = (((𝑓‘𝑤)‘𝑖)( ·𝑠 ‘𝐶)𝑖))
302	301	cbvmptv 5183	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣)) = (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑖)( ·𝑠 ‘𝐶)𝑖))
303	176	fveq1d 6836	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 𝑗 → ((𝑓‘𝑤)‘𝑖) = ((𝑓‘𝑗)‘𝑖))
304	303	oveq1d 7378	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 𝑗 → (((𝑓‘𝑤)‘𝑖)( ·𝑠 ‘𝐶)𝑖) = (((𝑓‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))
305	304	mpteq2dv 5173	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑗 → (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑖)( ·𝑠 ‘𝐶)𝑖)) = (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)))
306	302, 305	eqtrid 2787	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑗 → (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣)) = (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)))
307	306	oveq2d 7379	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑗 → (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))
308	227, 307	eqeq12d 2756	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑗 → ((𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))) ↔ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)))))
309	299, 308	anbi12d 638	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑗 → (((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣)))) ↔ ((𝑓‘𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))))
310	309	cbvralvw 3218	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣)))) ↔ ∀𝑗 ∈ 𝑦 ((𝑓‘𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)))))
311	310	bilani 505	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → ∀𝑗 ∈ 𝑦 ((𝑓‘𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)))))
312	311	r19.21bi 3232	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) ∧ 𝑗 ∈ 𝑦) → ((𝑓‘𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)))))
313	312	simpld 495	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) ∧ 𝑗 ∈ 𝑦) → (𝑓‘𝑗) finSupp (0g‘(Scalar‘𝐶)))
314	312	simprd 496	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) ∧ 𝑗 ∈ 𝑦) → (𝑎‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑥 ↦ (((𝑓‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))
315	73, 26, 16, 4, 12, 281, 282, 283, 284, 285, 85, 179, 286, 287, 289, 290, 291, 297, 298, 313, 314	fedgmullem1 33820	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) ∧ 𝑓:𝑦⟶((Base‘(Scalar‘𝐶)) ↑m 𝑥)) ∧ ∀𝑤 ∈ 𝑦 ((𝑓‘𝑤) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝑎‘𝑤) = (𝐶 Σg (𝑣 ∈ 𝑥 ↦ (((𝑓‘𝑤)‘𝑣)( ·𝑠 ‘𝐶)𝑣))))) → ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg ((𝑤 ∈ 𝑦, 𝑣 ∈ 𝑥 ↦ ((𝑓‘𝑤)‘𝑣)) ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))))))
316	274, 280, 315	rspcedvd 3569	. . . . . . . . . . . . 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‘𝐸)𝑤))))))
317	316	anasss 467	. . . . . . . . . . . 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‘𝐸)𝑤))))))
318	248, 317	exlimddv 1942	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝐵))) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥))(𝑐 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))))))
319	318	anasss 467	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)) ∧ (𝑎 finSupp (0g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤))))) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥))(𝑐 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))))))
320		eqid 2740	. . . . . . . . . . . . . . . . 17 ⊢ (LSpan‘𝐵) = (LSpan‘𝐵)
321	60, 29, 320	islbs4 21814	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (LBasis‘𝐵) ↔ (𝑦 ∈ (LIndS‘𝐵) ∧ ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵)))
322	321	bilani 505	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑦 ∈ (LIndS‘𝐵) ∧ ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵)))
323	322	simprd 496	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵))
324	323	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((LSpan‘𝐵)‘𝑦) = (Base‘𝐵))
325	78, 64	eqtr3d 2777	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Base‘𝐴) = (Base‘𝐵))
326	325	ad3antrrr 736	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → (Base‘𝐴) = (Base‘𝐵))
327	324, 326	eqtr4d 2778	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((LSpan‘𝐵)‘𝑦) = (Base‘𝐴))
328	288, 327	eleqtrrd 2843	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ ((LSpan‘𝐵)‘𝑦))
329		eqid 2740	. . . . . . . . . . . . 13 ⊢ (Scalar‘𝐵) = (Scalar‘𝐵)
330		lveclmod 21103	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ LVec → 𝐵 ∈ LMod)
331	28, 330	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ LMod)
332	331	ad2antrr 732	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → 𝐵 ∈ LMod)
333	320, 60, 88, 329, 91, 89, 332, 62	ellspds 33458	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑧 ∈ ((LSpan‘𝐵)‘𝑦) ↔ ∃𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)(𝑎 finSupp (0g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤))))))
334	333	biimpa 477	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ ((LSpan‘𝐵)‘𝑦)) → ∃𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)(𝑎 finSupp (0g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))))
335	205, 328, 334	syl2anc 590	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ∃𝑎 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑦)(𝑎 finSupp (0g‘(Scalar‘𝐵)) ∧ 𝑧 = (𝐵 Σg (𝑤 ∈ 𝑦 ↦ ((𝑎‘𝑤)( ·𝑠 ‘𝐵)𝑤)))))
336	319, 335	r19.29a 3148	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥))(𝑐 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))))))
337		eqid 2740	. . . . . . . . . . 11 ⊢ (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴))
338	202, 187, 337, 188, 191, 189, 87, 170, 157	ellspd 21784	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑧 ∈ ((LSpan‘𝐴)‘((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) “ (𝑦 × 𝑥))) ↔ ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥))(𝑐 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))))))
339	338	adantr 481	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑧 ∈ ((LSpan‘𝐴)‘((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) “ (𝑦 × 𝑥))) ↔ ∃𝑐 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑦 × 𝑥))(𝑐 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑧 = (𝐴 Σg (𝑐 ∘f ( ·𝑠 ‘𝐴)(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))))))
340	336, 339	mpbird 258	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ ((LSpan‘𝐴)‘((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) “ (𝑦 × 𝑥))))
341	87	ffnd 6663	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) Fn (𝑦 × 𝑥))
342	341	adantr 481	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) Fn (𝑦 × 𝑥))
343		fnima 6622	. . . . . . . . . 10 ⊢ ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) Fn (𝑦 × 𝑥) → ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) “ (𝑦 × 𝑥)) = ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))
344	342, 343	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) “ (𝑦 × 𝑥)) = ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))
345	344	fveq2d 6838	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → ((LSpan‘𝐴)‘((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) “ (𝑦 × 𝑥))) = ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))))
346	340, 345	eleqtrd 2842	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))))
347	204, 346	eqelssd 3943	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))) = (Base‘𝐴))
348		eqid 2740	. . . . . . 7 ⊢ (Base‘(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))) = (Base‘(𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)))
349		drngnzr 20727	. . . . . . . . . 10 ⊢ (𝐾 ∈ DivRing → 𝐾 ∈ NzRing)
350	14, 349	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ NzRing)
351	258, 350	eqeltrrd 2841	. . . . . . . 8 ⊢ (𝜑 → (Scalar‘𝐴) ∈ NzRing)
352	351	ad2antrr 732	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (Scalar‘𝐴) ∈ NzRing)
353	187, 348, 188, 189, 190, 191, 202, 170, 352, 157, 156	lindflbs 33469	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) ∈ (LBasis‘𝐴) ↔ ((𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) LIndF 𝐴 ∧ ((LSpan‘𝐴)‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))) = (Base‘𝐴))))
354	195, 347, 353	mpbir2and 719	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) ∈ (LBasis‘𝐴))
355		eqid 2740	. . . . . 6 ⊢ (LBasis‘𝐴) = (LBasis‘𝐴)
356	355	dimval 33792	. . . . 5 ⊢ ((𝐴 ∈ LVec ∧ ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤)) ∈ (LBasis‘𝐴)) → (dim‘𝐴) = (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))))
357	167, 354, 356	syl2anc 590	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐴) = (♯‘ran (𝑤 ∈ 𝑦, 𝑡 ∈ 𝑥 ↦ (𝑡(.r‘𝐸)𝑤))))
358	29	dimval 33792	. . . . . 6 ⊢ ((𝐵 ∈ LVec ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐵) = (♯‘𝑦))
359	92, 59, 358	syl2anc 590	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐵) = (♯‘𝑦))
360	20	dimval 33792	. . . . . 6 ⊢ ((𝐶 ∈ LVec ∧ 𝑥 ∈ (LBasis‘𝐶)) → (dim‘𝐶) = (♯‘𝑥))
361	110, 38, 360	syl2anc 590	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐶) = (♯‘𝑥))
362	359, 361	oveq12d 7381	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → ((dim‘𝐵) ·e (dim‘𝐶)) = ((♯‘𝑦) ·e (♯‘𝑥)))
363	164, 357, 362	3eqtr4d 2785	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) ∧ 𝑦 ∈ (LBasis‘𝐵)) → (dim‘𝐴) = ((dim‘𝐵) ·e (dim‘𝐶)))
364	34, 363	exlimddv 1942	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ (LBasis‘𝐶)) → (dim‘𝐴) = ((dim‘𝐵) ·e (dim‘𝐶)))
365	24, 364	exlimddv 1942	1 ⊢ (𝜑 → (dim‘𝐴) = ((dim‘𝐵) ·e (dim‘𝐶)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1092   = wceq 1547  ∃wex 1786   ∈ wcel 2119   ≠ wne 2935  ∀wral 3054  ∃wrex 3064  Vcvv 3432   ⊆ wss 3890  ∅c0 4268  {csn 4562   class class class wbr 5079   ↦ cmpt 5160   × cxp 5623  ran crn 5626   “ cima 5628   Fn wfn 6487  ⟶wf 6488  –1-1→wf1 6489  ‘cfv 6492  (class class class)co 7363   ∈ cmpo 7365   ∘_f cof 7625   ↑_m cmap 8770   ≈ cen 8887   finSupp cfsupp 9271   ·_e cxmu 13060  ♯chash 14290  Basecbs 17177   ↾_s cress 17198  +_gcplusg 17218  ._rcmulr 17219  Scalarcsca 17221   ·_𝑠 cvsca 17222  0_gc0g 17400   Σ_g cgsu 17401  Ringcrg 20212  NzRingcnzr 20491  SubRingcsubrg 20548  DivRingcdr 20708  LModclmod 20857  LSpanclspn 20968  LBasisclbs 21071  LVecclvec 21099  subringAlg csra 21168   freeLMod cfrlm 21728   LIndF clindf 21786  LIndSclinds 21787  dimcldim 33790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-rep 5206  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-reg 9504  ax-inf2 9560  ax-ac2 10383  ax-cnex 11092  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-mulcom 11100  ax-addass 11101  ax-mulass 11102  ax-distr 11103  ax-i2m1 11104  ax-1ne0 11105  ax-1rid 11106  ax-rnegex 11107  ax-rrecex 11108  ax-cnre 11109  ax-pre-lttri 11110  ax-pre-lttrn 11111  ax-pre-ltadd 11112  ax-pre-mulgt0 11113

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-rmo 3345  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-tp 4567  df-op 4569  df-uni 4846  df-int 4885  df-iun 4930  df-iin 4931  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-se 5579  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7320  df-ov 7366  df-oprab 7367  df-mpo 7368  df-of 7627  df-rpss 7673  df-om 7814  df-1st 7938  df-2nd 7939  df-supp 8108  df-tpos 8173  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-1o 8402  df-2o 8403  df-oadd 8406  df-er 8640  df-map 8772  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9272  df-sup 9352  df-oi 9422  df-r1 9686  df-rank 9687  df-dju 9823  df-card 9861  df-acn 9864  df-ac 10036  df-pnf 11179  df-mnf 11180  df-xr 11181  df-ltxr 11182  df-le 11183  df-sub 11377  df-neg 11378  df-nn 12173  df-2 12242  df-3 12243  df-4 12244  df-5 12245  df-6 12246  df-7 12247  df-8 12248  df-9 12249  df-n0 12436  df-xnn0 12509  df-z 12523  df-dec 12643  df-uz 12787  df-xmul 13063  df-fz 13460  df-fzo 13607  df-seq 13962  df-hash 14291  df-struct 17115  df-sets 17132  df-slot 17150  df-ndx 17162  df-base 17178  df-ress 17199  df-plusg 17231  df-mulr 17232  df-sca 17234  df-vsca 17235  df-ip 17236  df-tset 17237  df-ple 17238  df-ocomp 17239  df-ds 17240  df-hom 17242  df-cco 17243  df-0g 17402  df-gsum 17403  df-prds 17408  df-pws 17410  df-mre 17546  df-mrc 17547  df-mri 17548  df-acs 17549  df-proset 18258  df-drs 18259  df-poset 18277  df-ipo 18492  df-mgm 18606  df-sgrp 18685  df-mnd 18701  df-mhm 18749  df-submnd 18750  df-grp 18910  df-minusg 18911  df-sbg 18912  df-mulg 19042  df-subg 19097  df-ghm 19186  df-cntz 19290  df-cmn 19755  df-abl 19756  df-mgp 20120  df-rng 20132  df-ur 20161  df-ring 20214  df-oppr 20315  df-dvdsr 20335  df-unit 20336  df-invr 20366  df-nzr 20492  df-subrng 20525  df-subrg 20549  df-drng 20710  df-lmod 20859  df-lss 20929  df-lsp 20969  df-lmhm 21019  df-lbs 21072  df-lvec 21100  df-sra 21170  df-rgmod 21171  df-dsmm 21714  df-frlm 21729  df-uvc 21765  df-lindf 21788  df-linds 21789  df-dim 33791

This theorem is referenced by:  extdgmul  33854