fedgmul

Description: The multiplicativity formula for degrees of field extensions. Given E a field extension of F , itself a field extension of K , we have [ E : K ] = [ E : F ] [ F : K ] . Proposition 1.2 of Lang, p. 224. Here ( dimA ) is the degree of the extension E of K , ( dimB ) is the degree of the extension E of F , and ( dimC ) is the degree of the extension F of K . This proof is valid for infinite dimensions, and is actually valid for division ring extensions, not just field extensions. (Contributed by Thierry Arnoux, 25-Jul-2023) Remove dependency on ax-reg . (Revised by Timothy J. O'Malley, 15-Oct-2026)

	Ref	Expression
Hypotheses	fedgmul.a	$⊢ A = subringAlg (E) (V)$
	fedgmul.b	$⊢ B = subringAlg (E) (U)$
	fedgmul.c	$⊢ C = subringAlg (F) (V)$
	fedgmul.f	$⊢ F = E ↾_{𝑠} U$
	fedgmul.k	$⊢ K = E ↾_{𝑠} V$
	fedgmul.1	$⊢ φ \to E \in DivRing$
	fedgmul.2	$⊢ φ \to F \in DivRing$
	fedgmul.3	$⊢ φ \to K \in DivRing$
	fedgmul.4	$⊢ φ \to U \in SubRing (E)$
	fedgmul.5	$⊢ φ \to V \in SubRing (F)$
Assertion	fedgmul	$⊢ φ \to \dim (A) = \dim (B) \cdot_{𝑒} \dim (C)$

Proof

Step	Hyp	Ref	Expression
1		fedgmul.a	$⊢ A = subringAlg (E) (V)$
2		fedgmul.b	$⊢ B = subringAlg (E) (U)$
3		fedgmul.c	$⊢ C = subringAlg (F) (V)$
4		fedgmul.f	$⊢ F = E ↾_{𝑠} U$
5		fedgmul.k	$⊢ K = E ↾_{𝑠} V$
6		fedgmul.1	$⊢ φ \to E \in DivRing$
7		fedgmul.2	$⊢ φ \to F \in DivRing$
8		fedgmul.3	$⊢ φ \to K \in DivRing$
9		fedgmul.4	$⊢ φ \to U \in SubRing (E)$
10		fedgmul.5	$⊢ φ \to V \in SubRing (F)$
11	4	subsubrg	$⊢ U \in SubRing (E) \to (V \in SubRing (F) \leftrightarrow (V \in SubRing (E) \land V \subseteq U))$
12	11	biimpa	$⊢ (U \in SubRing (E) \land V \in SubRing (F)) \to (V \in SubRing (E) \land V \subseteq U)$
13	9 10 12	syl2anc	$⊢ φ \to (V \in SubRing (E) \land V \subseteq U)$
14	13	simprd	$⊢ φ \to V \subseteq U$
15		ressabs	$⊢ (U \in SubRing (E) \land V \subseteq U) \to (E ↾_{𝑠} U) ↾_{𝑠} V = E ↾_{𝑠} V$
16	9 14 15	syl2anc	$⊢ φ \to (E ↾_{𝑠} U) ↾_{𝑠} V = E ↾_{𝑠} V$
17	4	oveq1i	$⊢ F ↾_{𝑠} V = (E ↾_{𝑠} U) ↾_{𝑠} V$
18	16 17 5	3eqtr4g	$⊢ φ \to F ↾_{𝑠} V = K$
19	18 8	eqeltrd	$⊢ φ \to F ↾_{𝑠} V \in DivRing$
20		eqid	$⊢ F ↾_{𝑠} V = F ↾_{𝑠} V$
21	3 20	sralvec	$⊢ (F \in DivRing \land F ↾_{𝑠} V \in DivRing \land V \in SubRing (F)) \to C \in LVec$
22	7 19 10 21	syl3anc	$⊢ φ \to C \in LVec$
23		eqid	$⊢ LBasis (C) = LBasis (C)$
24	23	lbsex	$⊢ C \in LVec \to LBasis (C) \neq \emptyset$
25	22 24	syl	$⊢ φ \to LBasis (C) \neq \emptyset$
26	2 4	sralvec	$⊢ (E \in DivRing \land F \in DivRing \land U \in SubRing (E)) \to B \in LVec$
27	6 7 9 26	syl3anc	$⊢ φ \to B \in LVec$
28		eqid	$⊢ LBasis (B) = LBasis (B)$
29	28	lbsex	$⊢ B \in LVec \to LBasis (B) \neq \emptyset$
30	27 29	syl	$⊢ φ \to LBasis (B) \neq \emptyset$
31		n0	$⊢ LBasis (B) \neq \emptyset \leftrightarrow \exists y y \in LBasis (B)$
32	30 31	sylib	$⊢ φ \to \exists y y \in LBasis (B)$
33	32	adantr	$⊢ (φ \land x \in LBasis (C)) \to \exists y y \in LBasis (B)$
34		eqid	$⊢ {Base}_{E} = {Base}_{E}$
35		eqid	$⊢ \cdot_{E} = \cdot_{E}$
36	6	drngringd	$⊢ φ \to E \in Ring$
37	36	ad4antr	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \to E \in Ring$
38		simplr	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to x \in LBasis (C)$
39		eqid	$⊢ {Base}_{C} = {Base}_{C}$
40	39 23	lbsss	$⊢ x \in LBasis (C) \to x \subseteq {Base}_{C}$
41	38 40	syl	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to x \subseteq {Base}_{C}$
42	34	subrgss	$⊢ U \in SubRing (E) \to U \subseteq {Base}_{E}$
43	9 42	syl	$⊢ φ \to U \subseteq {Base}_{E}$
44	4 34	ressbas2	$⊢ U \subseteq {Base}_{E} \to U = {Base}_{F}$
45	43 44	syl	$⊢ φ \to U = {Base}_{F}$
46	3	a1i	$⊢ φ \to C = subringAlg (F) (V)$
47		eqid	$⊢ {Base}_{F} = {Base}_{F}$
48	47	subrgss	$⊢ V \in SubRing (F) \to V \subseteq {Base}_{F}$
49	10 48	syl	$⊢ φ \to V \subseteq {Base}_{F}$
50	46 49	srabase	$⊢ φ \to {Base}_{F} = {Base}_{C}$
51	45 50	eqtrd	$⊢ φ \to U = {Base}_{C}$
52	51 43	eqsstrrd	$⊢ φ \to {Base}_{C} \subseteq {Base}_{E}$
53	52	ad2antrr	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to {Base}_{C} \subseteq {Base}_{E}$
54	41 53	sstrd	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to x \subseteq {Base}_{E}$
55	54	ad2antrr	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \to x \subseteq {Base}_{E}$
56		simpr	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \to i \in x$
57	55 56	sseldd	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \to i \in {Base}_{E}$
58		simpr	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to y \in LBasis (B)$
59		eqid	$⊢ {Base}_{B} = {Base}_{B}$
60	59 28	lbsss	$⊢ y \in LBasis (B) \to y \subseteq {Base}_{B}$
61	58 60	syl	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to y \subseteq {Base}_{B}$
62	2	a1i	$⊢ φ \to B = subringAlg (E) (U)$
63	62 43	srabase	$⊢ φ \to {Base}_{E} = {Base}_{B}$
64	63	ad2antrr	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to {Base}_{E} = {Base}_{B}$
65	61 64	sseqtrrd	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to y \subseteq {Base}_{E}$
66	65	ad2antrr	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \to y \subseteq {Base}_{E}$
67		simplr	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \to j \in y$
68	66 67	sseldd	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \to j \in {Base}_{E}$
69	34 35 37 57 68	ringcld	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \to i \cdot_{E} j \in {Base}_{E}$
70	1	a1i	$⊢ φ \to A = subringAlg (E) (V)$
71	13	simpld	$⊢ φ \to V \in SubRing (E)$
72	34	subrgss	$⊢ V \in SubRing (E) \to V \subseteq {Base}_{E}$
73	71 72	syl	$⊢ φ \to V \subseteq {Base}_{E}$
74	70 73	srabase	$⊢ φ \to {Base}_{E} = {Base}_{A}$
75	74	ad4antr	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \to {Base}_{E} = {Base}_{A}$
76	69 75	eleqtrd	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \to i \cdot_{E} j \in {Base}_{A}$
77	76	anasss	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land (j \in y \land i \in x)) \to i \cdot_{E} j \in {Base}_{A}$
78	77	ralrimivva	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to \forall j \in y \forall i \in x i \cdot_{E} j \in {Base}_{A}$
79		oveq2	$⊢ w = j \to t \cdot_{E} w = t \cdot_{E} j$
80		oveq1	$⊢ t = i \to t \cdot_{E} j = i \cdot_{E} j$
81	79 80	cbvmpov	$⊢ (w \in y, t \in x ⟼ t \cdot_{E} w) = (j \in y, i \in x ⟼ i \cdot_{E} j)$
82	81	fmpo	$⊢ \forall j \in y \forall i \in x i \cdot_{E} j \in {Base}_{A} \leftrightarrow (w \in y, t \in x ⟼ t \cdot_{E} w) : y \times x ⟶ {Base}_{A}$
83	78 82	sylib	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to (w \in y, t \in x ⟼ t \cdot_{E} w) : y \times x ⟶ {Base}_{A}$
84		eqid	$⊢ {Base}_{Scalar (B)} = {Base}_{Scalar (B)}$
85		eqid	$⊢ \cdot_{B} = \cdot_{B}$
86		eqid	$⊢ +_{B} = +_{B}$
87		eqid	$⊢ 0_{Scalar (B)} = 0_{Scalar (B)}$
88	27	ad2antrr	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to B \in LVec$
89	88	ad5antr	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \land j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u) \to B \in LVec$
90	28	lbslinds	$⊢ LBasis (B) \subseteq LIndS (B)$
91	90 58	sselid	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to y \in LIndS (B)$
92	91	ad5antr	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \land j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u) \to y \in LIndS (B)$
93	67	ad3antrrr	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \land j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u) \to j \in y$
94		simpllr	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \land j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u) \to v \in y$
95	62 43	srasca	$⊢ φ \to E ↾_{𝑠} U = Scalar (B)$
96	4 95	eqtrid	$⊢ φ \to F = Scalar (B)$
97	96	fveq2d	$⊢ φ \to {Base}_{F} = {Base}_{Scalar (B)}$
98	97 50	eqtr3d	$⊢ φ \to {Base}_{Scalar (B)} = {Base}_{C}$
99	98	ad2antrr	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to {Base}_{Scalar (B)} = {Base}_{C}$
100	41 99	sseqtrrd	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to x \subseteq {Base}_{Scalar (B)}$
101	100	ad5antr	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \land j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u) \to x \subseteq {Base}_{Scalar (B)}$
102		simp-4r	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \land j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u) \to i \in x$
103	101 102	sseldd	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \land j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u) \to i \in {Base}_{Scalar (B)}$
104		simplr	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \land j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u) \to u \in x$
105	101 104	sseldd	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \land j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u) \to u \in {Base}_{Scalar (B)}$
106	22	ad2antrr	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to C \in LVec$
107		eqid	$⊢ LSpan (C) = LSpan (C)$
108	39 23 107	islbs4	$⊢ x \in LBasis (C) \leftrightarrow (x \in LIndS (C) \land LSpan (C) (x) = {Base}_{C})$
109	38 108	sylib	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to (x \in LIndS (C) \land LSpan (C) (x) = {Base}_{C})$
110	109	simpld	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to x \in LIndS (C)$
111		eqid	$⊢ 0_{C} = 0_{C}$
112	111	0nellinds	$⊢ (C \in LVec \land x \in LIndS (C)) \to \neg 0_{C} \in x$
113	106 110 112	syl2anc	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to \neg 0_{C} \in x$
114	113	ad5antr	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \land j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u) \to \neg 0_{C} \in x$
115		nelne2	$⊢ (i \in x \land \neg 0_{C} \in x) \to i \neq 0_{C}$
116	102 114 115	syl2anc	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \land j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u) \to i \neq 0_{C}$
117	96	fveq2d	$⊢ φ \to 0_{F} = 0_{Scalar (B)}$
118	3 7 10	drgext0g	$⊢ φ \to 0_{F} = 0_{C}$
119	117 118	eqtr3d	$⊢ φ \to 0_{Scalar (B)} = 0_{C}$
120	119	ad7antr	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \land j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u) \to 0_{Scalar (B)} = 0_{C}$
121	116 120	neeqtrrd	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \land j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u) \to i \neq 0_{Scalar (B)}$
122		simpr	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \land j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u) \to j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u$
123		ovexd	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \land j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u) \to i \cdot_{E} j \in V$
124	81	ovmpt4g	$⊢ (j \in y \land i \in x \land i \cdot_{E} j \in V) \to j (w \in y, t \in x ⟼ t \cdot_{E} w) i = i \cdot_{E} j$
125	93 102 123 124	syl3anc	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \land j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u) \to j (w \in y, t \in x ⟼ t \cdot_{E} w) i = i \cdot_{E} j$
126	2 6 9	drgextvsca	$⊢ φ \to \cdot_{E} = \cdot_{B}$
127	126	oveqd	$⊢ φ \to i \cdot_{E} j = i \cdot_{B} j$
128	127	ad7antr	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \land j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u) \to i \cdot_{E} j = i \cdot_{B} j$
129	125 128	eqtrd	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \land j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u) \to j (w \in y, t \in x ⟼ t \cdot_{E} w) i = i \cdot_{B} j$
130	81	a1i	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land v \in y) \land u \in x) \to (w \in y, t \in x ⟼ t \cdot_{E} w) = (j \in y, i \in x ⟼ i \cdot_{E} j)$
131		simprr	$⊢ (((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land v \in y) \land u \in x) \land (j = v \land i = u)) \to i = u$
132		simprl	$⊢ (((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land v \in y) \land u \in x) \land (j = v \land i = u)) \to j = v$
133	131 132	oveq12d	$⊢ (((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land v \in y) \land u \in x) \land (j = v \land i = u)) \to i \cdot_{E} j = u \cdot_{E} v$
134		simplr	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land v \in y) \land u \in x) \to v \in y$
135		simpr	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land v \in y) \land u \in x) \to u \in x$
136		ovexd	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land v \in y) \land u \in x) \to u \cdot_{E} v \in V$
137	130 133 134 135 136	ovmpod	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land v \in y) \land u \in x) \to v (w \in y, t \in x ⟼ t \cdot_{E} w) u = u \cdot_{E} v$
138	137	adantllr	$⊢ (((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land i \in x) \land v \in y) \land u \in x) \to v (w \in y, t \in x ⟼ t \cdot_{E} w) u = u \cdot_{E} v$
139	138	adantl3r	$⊢ ((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \to v (w \in y, t \in x ⟼ t \cdot_{E} w) u = u \cdot_{E} v$
140	139	adantr	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \land j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u) \to v (w \in y, t \in x ⟼ t \cdot_{E} w) u = u \cdot_{E} v$
141	126	oveqd	$⊢ φ \to u \cdot_{E} v = u \cdot_{B} v$
142	141	ad7antr	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \land j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u) \to u \cdot_{E} v = u \cdot_{B} v$
143	140 142	eqtrd	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \land j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u) \to v (w \in y, t \in x ⟼ t \cdot_{E} w) u = u \cdot_{B} v$
144	122 129 143	3eqtr3d	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \land j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u) \to i \cdot_{B} j = u \cdot_{B} v$
145	84 85 86 87 89 92 93 94 103 105 121 144	linds2eq	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \land j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u) \to (j = v \land i = u)$
146	145	ex	$⊢ ((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land v \in y) \land u \in x) \to (j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u \to (j = v \land i = u))$
147	146	anasss	$⊢ (((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \land (v \in y \land u \in x)) \to (j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u \to (j = v \land i = u))$
148	147	ralrimivva	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land j \in y) \land i \in x) \to \forall v \in y \forall u \in x (j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u \to (j = v \land i = u))$
149	148	anasss	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land (j \in y \land i \in x)) \to \forall v \in y \forall u \in x (j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u \to (j = v \land i = u))$
150	149	ralrimivva	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to \forall j \in y \forall i \in x \forall v \in y \forall u \in x (j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u \to (j = v \land i = u))$
151		f1opr	$⊢ (w \in y, t \in x ⟼ t \cdot_{E} w) : y \times x \underset{1-1}{⟶} {Base}_{A} \leftrightarrow ((w \in y, t \in x ⟼ t \cdot_{E} w) : y \times x ⟶ {Base}_{A} \land \forall j \in y \forall i \in x \forall v \in y \forall u \in x (j (w \in y, t \in x ⟼ t \cdot_{E} w) i = v (w \in y, t \in x ⟼ t \cdot_{E} w) u \to (j = v \land i = u)))$
152	83 150 151	sylanbrc	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to (w \in y, t \in x ⟼ t \cdot_{E} w) : y \times x \underset{1-1}{⟶} {Base}_{A}$
153	58 38	xpexd	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to y \times x \in V$
154		f1rnen	$⊢ ((w \in y, t \in x ⟼ t \cdot_{E} w) : y \times x \underset{1-1}{⟶} {Base}_{A} \land y \times x \in V) \to ran (w \in y, t \in x ⟼ t \cdot_{E} w) \approx (y \times x)$
155	152 153 154	syl2anc	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to ran (w \in y, t \in x ⟼ t \cdot_{E} w) \approx (y \times x)$
156		hasheni	$⊢ ran (w \in y, t \in x ⟼ t \cdot_{E} w) \approx (y \times x) \to \|ran (w \in y, t \in x ⟼ t \cdot_{E} w)\| = \|y \times x\|$
157	155 156	syl	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to \|ran (w \in y, t \in x ⟼ t \cdot_{E} w)\| = \|y \times x\|$
158		hashxpe	$⊢ (y \in LBasis (B) \land x \in LBasis (C)) \to \|y \times x\| = \|y\| \cdot_{𝑒} \|x\|$
159	58 38 158	syl2anc	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to \|y \times x\| = \|y\| \cdot_{𝑒} \|x\|$
160	157 159	eqtrd	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to \|ran (w \in y, t \in x ⟼ t \cdot_{E} w)\| = \|y\| \cdot_{𝑒} \|x\|$
161	1 5	sralvec	$⊢ (E \in DivRing \land K \in DivRing \land V \in SubRing (E)) \to A \in LVec$
162	6 8 71 161	syl3anc	$⊢ φ \to A \in LVec$
163	162	ad2antrr	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to A \in LVec$
164	162	lveclmodd	$⊢ φ \to A \in LMod$
165	164	ad2antrr	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to A \in LMod$
166	6	ad4antr	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land c \in {Base}_{(Scalar (A) freeLMod (y \times x))}) \land \sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)) = 0_{A}) \to E \in DivRing$
167	7	ad4antr	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land c \in {Base}_{(Scalar (A) freeLMod (y \times x))}) \land \sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)) = 0_{A}) \to F \in DivRing$
168	8	ad4antr	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land c \in {Base}_{(Scalar (A) freeLMod (y \times x))}) \land \sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)) = 0_{A}) \to K \in DivRing$
169	9	ad4antr	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land c \in {Base}_{(Scalar (A) freeLMod (y \times x))}) \land \sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)) = 0_{A}) \to U \in SubRing (E)$
170	10	ad4antr	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land c \in {Base}_{(Scalar (A) freeLMod (y \times x))}) \land \sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)) = 0_{A}) \to V \in SubRing (F)$
171		fveq2	$⊢ w = j \to f (w) = f (j)$
172	171	fveq1d	$⊢ w = j \to f (w) (v) = f (j) (v)$
173		fveq2	$⊢ v = i \to f (j) (v) = f (j) (i)$
174	172 173	cbvmpov	$⊢ (w \in y, v \in x ⟼ f (w) (v)) = (j \in y, i \in x ⟼ f (j) (i))$
175		simp-4r	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land c \in {Base}_{(Scalar (A) freeLMod (y \times x))}) \land \sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)) = 0_{A}) \to x \in LBasis (C)$
176		simpllr	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land c \in {Base}_{(Scalar (A) freeLMod (y \times x))}) \land \sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)) = 0_{A}) \to y \in LBasis (B)$
177		simplr	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land c \in {Base}_{(Scalar (A) freeLMod (y \times x))}) \land \sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)) = 0_{A}) \to c \in {Base}_{(Scalar (A) freeLMod (y \times x))}$
178		simpr	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land c \in {Base}_{(Scalar (A) freeLMod (y \times x))}) \land \sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)) = 0_{A}) \to \sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)) = 0_{A}$
179	1 2 3 4 5 166 167 168 169 170 81 174 175 176 177 178	fedgmullem2	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land c \in {Base}_{(Scalar (A) freeLMod (y \times x))}) \land \sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)) = 0_{A}) \to c = (y \times x) \times \{0_{Scalar (A)}\}$
180	179	ex	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land c \in {Base}_{(Scalar (A) freeLMod (y \times x))}) \to (\sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)) = 0_{A} \to c = (y \times x) \times \{0_{Scalar (A)}\})$
181	180	ralrimiva	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to \forall c \in {Base}_{(Scalar (A) freeLMod (y \times x))} (\sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)) = 0_{A} \to c = (y \times x) \times \{0_{Scalar (A)}\})$
182		eqid	$⊢ {Base}_{A} = {Base}_{A}$
183		eqid	$⊢ Scalar (A) = Scalar (A)$
184		eqid	$⊢ \cdot_{A} = \cdot_{A}$
185		eqid	$⊢ 0_{A} = 0_{A}$
186		eqid	$⊢ 0_{Scalar (A)} = 0_{Scalar (A)}$
187		eqid	$⊢ {Base}_{(Scalar (A) freeLMod (y \times x))} = {Base}_{(Scalar (A) freeLMod (y \times x))}$
188	182 183 184 185 186 187	islindf4	$⊢ (A \in LMod \land y \times x \in V \land (w \in y, t \in x ⟼ t \cdot_{E} w) : y \times x ⟶ {Base}_{A}) \to ((w \in y, t \in x ⟼ t \cdot_{E} w) LIndF A \leftrightarrow \forall c \in {Base}_{(Scalar (A) freeLMod (y \times x))} (\sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)) = 0_{A} \to c = (y \times x) \times \{0_{Scalar (A)}\}))$
189	188	biimpar	$⊢ ((A \in LMod \land y \times x \in V \land (w \in y, t \in x ⟼ t \cdot_{E} w) : y \times x ⟶ {Base}_{A}) \land \forall c \in {Base}_{(Scalar (A) freeLMod (y \times x))} (\sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)) = 0_{A} \to c = (y \times x) \times \{0_{Scalar (A)}\})) \to (w \in y, t \in x ⟼ t \cdot_{E} w) LIndF A$
190	165 153 83 181 189	syl31anc	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to (w \in y, t \in x ⟼ t \cdot_{E} w) LIndF A$
191	69	anasss	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land (j \in y \land i \in x)) \to i \cdot_{E} j \in {Base}_{E}$
192	191	ralrimivva	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to \forall j \in y \forall i \in x i \cdot_{E} j \in {Base}_{E}$
193	81	rnmposs	$⊢ \forall j \in y \forall i \in x i \cdot_{E} j \in {Base}_{E} \to ran (w \in y, t \in x ⟼ t \cdot_{E} w) \subseteq {Base}_{E}$
194	192 193	syl	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to ran (w \in y, t \in x ⟼ t \cdot_{E} w) \subseteq {Base}_{E}$
195	74	ad2antrr	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to {Base}_{E} = {Base}_{A}$
196	194 195	sseqtrd	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to ran (w \in y, t \in x ⟼ t \cdot_{E} w) \subseteq {Base}_{A}$
197		eqid	$⊢ LSpan (A) = LSpan (A)$
198	182 197	lspssv	$⊢ (A \in LMod \land ran (w \in y, t \in x ⟼ t \cdot_{E} w) \subseteq {Base}_{A}) \to LSpan (A) (ran (w \in y, t \in x ⟼ t \cdot_{E} w)) \subseteq {Base}_{A}$
199	165 196 198	syl2anc	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to LSpan (A) (ran (w \in y, t \in x ⟼ t \cdot_{E} w)) \subseteq {Base}_{A}$
200		simpl	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \to ((φ \land x \in LBasis (C)) \land y \in LBasis (B))$
201	200	ad4antr	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land j \in y) \to ((φ \land x \in LBasis (C)) \land y \in LBasis (B))$
202		elmapi	$⊢ a \in ({Base}_{Scalar (B)}^{y}) \to a : y ⟶ {Base}_{Scalar (B)}$
203	202	ad4antlr	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land j \in y) \to a : y ⟶ {Base}_{Scalar (B)}$
204		simpr	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land j \in y) \to j \in y$
205	203 204	ffvelcdmd	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land j \in y) \to a (j) \in {Base}_{Scalar (B)}$
206	109	simprd	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to LSpan (C) (x) = {Base}_{C}$
207	201 206	syl	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land j \in y) \to LSpan (C) (x) = {Base}_{C}$
208	98	ad7antr	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land j \in y) \to {Base}_{Scalar (B)} = {Base}_{C}$
209	207 208	eqtr4d	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land j \in y) \to LSpan (C) (x) = {Base}_{Scalar (B)}$
210	205 209	eleqtrrd	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land j \in y) \to a (j) \in LSpan (C) (x)$
211		eqid	$⊢ {Base}_{Scalar (C)} = {Base}_{Scalar (C)}$
212		eqid	$⊢ Scalar (C) = Scalar (C)$
213		eqid	$⊢ 0_{Scalar (C)} = 0_{Scalar (C)}$
214		eqid	$⊢ \cdot_{C} = \cdot_{C}$
215	22	lveclmodd	$⊢ φ \to C \in LMod$
216	215	ad2antrr	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to C \in LMod$
217	107 39 211 212 213 214 216 41	ellspds	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to (a (j) \in LSpan (C) (x) \leftrightarrow \exists b \in ({Base}_{Scalar (C)}^{x}) ({finSupp}_{0_{Scalar (C)}} (b) \land a (j) = \underset{i \in x}{\sum_{C}} (b (i) \cdot_{C} i)))$
218	217	biimpa	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land a (j) \in LSpan (C) (x)) \to \exists b \in ({Base}_{Scalar (C)}^{x}) ({finSupp}_{0_{Scalar (C)}} (b) \land a (j) = \underset{i \in x}{\sum_{C}} (b (i) \cdot_{C} i))$
219	201 210 218	syl2anc	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land j \in y) \to \exists b \in ({Base}_{Scalar (C)}^{x}) ({finSupp}_{0_{Scalar (C)}} (b) \land a (j) = \underset{i \in x}{\sum_{C}} (b (i) \cdot_{C} i))$
220	219	ralrimiva	$⊢ ((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \to \forall j \in y \exists b \in ({Base}_{Scalar (C)}^{x}) ({finSupp}_{0_{Scalar (C)}} (b) \land a (j) = \underset{i \in x}{\sum_{C}} (b (i) \cdot_{C} i))$
221		fveq2	$⊢ w = j \to a (w) = a (j)$
222		fveq2	$⊢ v = i \to b (v) = b (i)$
223		id	$⊢ v = i \to v = i$
224	222 223	oveq12d	$⊢ v = i \to b (v) \cdot_{C} v = b (i) \cdot_{C} i$
225	224	cbvmptv	$⊢ (v \in x ⟼ b (v) \cdot_{C} v) = (i \in x ⟼ b (i) \cdot_{C} i)$
226	225	oveq2i	$⊢ \underset{v \in x}{\sum_{C}} (b (v) \cdot_{C} v) = \underset{i \in x}{\sum_{C}} (b (i) \cdot_{C} i)$
227	226	a1i	$⊢ w = j \to \underset{v \in x}{\sum_{C}} (b (v) \cdot_{C} v) = \underset{i \in x}{\sum_{C}} (b (i) \cdot_{C} i)$
228	221 227	eqeq12d	$⊢ w = j \to (a (w) = \underset{v \in x}{\sum_{C}} (b (v) \cdot_{C} v) \leftrightarrow a (j) = \underset{i \in x}{\sum_{C}} (b (i) \cdot_{C} i))$
229	228	anbi2d	$⊢ w = j \to (({finSupp}_{0_{Scalar (C)}} (b) \land a (w) = \underset{v \in x}{\sum_{C}} (b (v) \cdot_{C} v)) \leftrightarrow ({finSupp}_{0_{Scalar (C)}} (b) \land a (j) = \underset{i \in x}{\sum_{C}} (b (i) \cdot_{C} i)))$
230	229	rexbidv	$⊢ w = j \to (\exists b \in ({Base}_{Scalar (C)}^{x}) ({finSupp}_{0_{Scalar (C)}} (b) \land a (w) = \underset{v \in x}{\sum_{C}} (b (v) \cdot_{C} v)) \leftrightarrow \exists b \in ({Base}_{Scalar (C)}^{x}) ({finSupp}_{0_{Scalar (C)}} (b) \land a (j) = \underset{i \in x}{\sum_{C}} (b (i) \cdot_{C} i)))$
231	230	cbvralvw	$⊢ \forall w \in y \exists b \in ({Base}_{Scalar (C)}^{x}) ({finSupp}_{0_{Scalar (C)}} (b) \land a (w) = \underset{v \in x}{\sum_{C}} (b (v) \cdot_{C} v)) \leftrightarrow \forall j \in y \exists b \in ({Base}_{Scalar (C)}^{x}) ({finSupp}_{0_{Scalar (C)}} (b) \land a (j) = \underset{i \in x}{\sum_{C}} (b (i) \cdot_{C} i))$
232		vex	$⊢ y \in V$
233		ovex	$⊢ {Base}_{Scalar (C)}^{x} \in V$
234		breq1	$⊢ b = f (w) \to ({finSupp}_{0_{Scalar (C)}} (b) \leftrightarrow {finSupp}_{0_{Scalar (C)}} (f (w)))$
235		fveq1	$⊢ b = f (w) \to b (v) = f (w) (v)$
236	235	oveq1d	$⊢ b = f (w) \to b (v) \cdot_{C} v = f (w) (v) \cdot_{C} v$
237	236	mpteq2dv	$⊢ b = f (w) \to (v \in x ⟼ b (v) \cdot_{C} v) = (v \in x ⟼ f (w) (v) \cdot_{C} v)$
238	237	oveq2d	$⊢ b = f (w) \to \underset{v \in x}{\sum_{C}} (b (v) \cdot_{C} v) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v)$
239	238	eqeq2d	$⊢ b = f (w) \to (a (w) = \underset{v \in x}{\sum_{C}} (b (v) \cdot_{C} v) \leftrightarrow a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))$
240	234 239	anbi12d	$⊢ b = f (w) \to (({finSupp}_{0_{Scalar (C)}} (b) \land a (w) = \underset{v \in x}{\sum_{C}} (b (v) \cdot_{C} v)) \leftrightarrow ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v)))$
241	240	ac6	$⊢ (y \in V \land {Base}_{Scalar (C)}^{x} \in V \land \forall w \in y \exists b \in ({Base}_{Scalar (C)}^{x}) ({finSupp}_{0_{Scalar (C)}} (b) \land a (w) = \underset{v \in x}{\sum_{C}} (b (v) \cdot_{C} v))) \to \exists f (f : y ⟶ {Base}_{Scalar (C)}^{x} \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v)))$
242	232 233 241	mp3an12	$⊢ \forall w \in y \exists b \in ({Base}_{Scalar (C)}^{x}) ({finSupp}_{0_{Scalar (C)}} (b) \land a (w) = \underset{v \in x}{\sum_{C}} (b (v) \cdot_{C} v)) \to \exists f (f : y ⟶ {Base}_{Scalar (C)}^{x} \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v)))$
243	231 242	sylbir	$⊢ \forall j \in y \exists b \in ({Base}_{Scalar (C)}^{x}) ({finSupp}_{0_{Scalar (C)}} (b) \land a (j) = \underset{i \in x}{\sum_{C}} (b (i) \cdot_{C} i)) \to \exists f (f : y ⟶ {Base}_{Scalar (C)}^{x} \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v)))$
244	220 243	syl	$⊢ ((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \to \exists f (f : y ⟶ {Base}_{Scalar (C)}^{x} \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v)))$
245		fvexd	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \to {Base}_{Scalar (A)} \in V$
246	153	adantr	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \to y \times x \in V$
247		simpllr	$⊢ (((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land j \in y) \land i \in x) \to f : y ⟶ {Base}_{Scalar (C)}^{x}$
248		simplr	$⊢ (((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land j \in y) \land i \in x) \to j \in y$
249	247 248	ffvelcdmd	$⊢ (((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land j \in y) \land i \in x) \to f (j) \in ({Base}_{Scalar (C)}^{x})$
250	249	elmaprd	$⊢ (((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land j \in y) \land i \in x) \to f (j) : x ⟶ {Base}_{Scalar (C)}$
251	250	anasss	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land (j \in y \land i \in x)) \to f (j) : x ⟶ {Base}_{Scalar (C)}$
252		simprr	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land (j \in y \land i \in x)) \to i \in x$
253	251 252	ffvelcdmd	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land (j \in y \land i \in x)) \to f (j) (i) \in {Base}_{Scalar (C)}$
254	70 73	srasca	$⊢ φ \to E ↾_{𝑠} V = Scalar (A)$
255	5 254	eqtrid	$⊢ φ \to K = Scalar (A)$
256	46 49	srasca	$⊢ φ \to F ↾_{𝑠} V = Scalar (C)$
257	18 256	eqtr3d	$⊢ φ \to K = Scalar (C)$
258	255 257	eqtr3d	$⊢ φ \to Scalar (A) = Scalar (C)$
259	258	fveq2d	$⊢ φ \to {Base}_{Scalar (A)} = {Base}_{Scalar (C)}$
260	259	ad4antr	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land (j \in y \land i \in x)) \to {Base}_{Scalar (A)} = {Base}_{Scalar (C)}$
261	253 260	eleqtrrd	$⊢ ((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land (j \in y \land i \in x)) \to f (j) (i) \in {Base}_{Scalar (A)}$
262	261	ralrimivva	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \to \forall j \in y \forall i \in x f (j) (i) \in {Base}_{Scalar (A)}$
263	174	fmpo	$⊢ \forall j \in y \forall i \in x f (j) (i) \in {Base}_{Scalar (A)} \leftrightarrow (w \in y, v \in x ⟼ f (w) (v)) : y \times x ⟶ {Base}_{Scalar (A)}$
264	262 263	sylib	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \to (w \in y, v \in x ⟼ f (w) (v)) : y \times x ⟶ {Base}_{Scalar (A)}$
265	245 246 264	elmapdd	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \to (w \in y, v \in x ⟼ f (w) (v)) \in ({Base}_{Scalar (A)}^{(y \times x)})$
266	265	ad5ant15	$⊢ ((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \to (w \in y, v \in x ⟼ f (w) (v)) \in ({Base}_{Scalar (A)}^{(y \times x)})$
267	266	adantr	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \to (w \in y, v \in x ⟼ f (w) (v)) \in ({Base}_{Scalar (A)}^{(y \times x)})$
268	267	adantl3r	$⊢ ((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \to (w \in y, v \in x ⟼ f (w) (v)) \in ({Base}_{Scalar (A)}^{(y \times x)})$
269		simpr	$⊢ (((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \land c = (w \in y, v \in x ⟼ f (w) (v))) \to c = (w \in y, v \in x ⟼ f (w) (v))$
270	269	breq1d	$⊢ (((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \land c = (w \in y, v \in x ⟼ f (w) (v))) \to ({finSupp}_{0_{Scalar (A)}} (c) \leftrightarrow {finSupp}_{0_{Scalar (A)}} ((w \in y, v \in x ⟼ f (w) (v))))$
271	269	oveq1d	$⊢ (((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \land c = (w \in y, v \in x ⟼ f (w) (v))) \to c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w) = (w \in y, v \in x ⟼ f (w) (v)) {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)$
272	271	oveq2d	$⊢ (((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \land c = (w \in y, v \in x ⟼ f (w) (v))) \to \sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)) = \sum_{A} ((w \in y, v \in x ⟼ f (w) (v)) {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w))$
273	272	eqeq2d	$⊢ (((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \land c = (w \in y, v \in x ⟼ f (w) (v))) \to (z = \sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)) \leftrightarrow z = \sum_{A} ((w \in y, v \in x ⟼ f (w) (v)) {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)))$
274	270 273	anbi12d	$⊢ (((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \land c = (w \in y, v \in x ⟼ f (w) (v))) \to (({finSupp}_{0_{Scalar (A)}} (c) \land z = \sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w))) \leftrightarrow ({finSupp}_{0_{Scalar (A)}} ((w \in y, v \in x ⟼ f (w) (v))) \land z = \sum_{A} ((w \in y, v \in x ⟼ f (w) (v)) {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w))))$
275	6	ad8antr	$⊢ ((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \to E \in DivRing$
276	7	ad8antr	$⊢ ((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \to F \in DivRing$
277	8	ad8antr	$⊢ ((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \to K \in DivRing$
278	9	ad8antr	$⊢ ((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \to U \in SubRing (E)$
279	10	ad8antr	$⊢ ((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \to V \in SubRing (F)$
280	38	ad6antr	$⊢ ((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \to x \in LBasis (C)$
281	58	ad6antr	$⊢ ((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \to y \in LBasis (B)$
282		simpr	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \to z \in {Base}_{A}$
283	282	ad5antr	$⊢ ((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \to z \in {Base}_{A}$
284	202	ad5antlr	$⊢ ((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \to a : y ⟶ {Base}_{Scalar (B)}$
285		simp-4r	$⊢ ((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \to {finSupp}_{0_{Scalar (B)}} (a)$
286		simpllr	$⊢ ((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \to z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)$
287		id	$⊢ w = j \to w = j$
288	221 287	oveq12d	$⊢ w = j \to a (w) \cdot_{B} w = a (j) \cdot_{B} j$
289	288	cbvmptv	$⊢ (w \in y ⟼ a (w) \cdot_{B} w) = (j \in y ⟼ a (j) \cdot_{B} j)$
290	289	oveq2i	$⊢ \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w) = \underset{j \in y}{\sum_{B}} (a (j) \cdot_{B} j)$
291	286 290	eqtrdi	$⊢ ((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \to z = \underset{j \in y}{\sum_{B}} (a (j) \cdot_{B} j)$
292		simplr	$⊢ ((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \to f : y ⟶ {Base}_{Scalar (C)}^{x}$
293	171	breq1d	$⊢ w = j \to ({finSupp}_{0_{Scalar (C)}} (f (w)) \leftrightarrow {finSupp}_{0_{Scalar (C)}} (f (j)))$
294		fveq2	$⊢ v = i \to f (w) (v) = f (w) (i)$
295	294 223	oveq12d	$⊢ v = i \to f (w) (v) \cdot_{C} v = f (w) (i) \cdot_{C} i$
296	295	cbvmptv	$⊢ (v \in x ⟼ f (w) (v) \cdot_{C} v) = (i \in x ⟼ f (w) (i) \cdot_{C} i)$
297	171	fveq1d	$⊢ w = j \to f (w) (i) = f (j) (i)$
298	297	oveq1d	$⊢ w = j \to f (w) (i) \cdot_{C} i = f (j) (i) \cdot_{C} i$
299	298	mpteq2dv	$⊢ w = j \to (i \in x ⟼ f (w) (i) \cdot_{C} i) = (i \in x ⟼ f (j) (i) \cdot_{C} i)$
300	296 299	eqtrid	$⊢ w = j \to (v \in x ⟼ f (w) (v) \cdot_{C} v) = (i \in x ⟼ f (j) (i) \cdot_{C} i)$
301	300	oveq2d	$⊢ w = j \to \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v) = \underset{i \in x}{\sum_{C}} (f (j) (i) \cdot_{C} i)$
302	221 301	eqeq12d	$⊢ w = j \to (a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v) \leftrightarrow a (j) = \underset{i \in x}{\sum_{C}} (f (j) (i) \cdot_{C} i))$
303	293 302	anbi12d	$⊢ w = j \to (({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v)) \leftrightarrow ({finSupp}_{0_{Scalar (C)}} (f (j)) \land a (j) = \underset{i \in x}{\sum_{C}} (f (j) (i) \cdot_{C} i)))$
304	303	cbvralvw	$⊢ \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v)) \leftrightarrow \forall j \in y ({finSupp}_{0_{Scalar (C)}} (f (j)) \land a (j) = \underset{i \in x}{\sum_{C}} (f (j) (i) \cdot_{C} i))$
305	304	bilani	$⊢ ((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \to \forall j \in y ({finSupp}_{0_{Scalar (C)}} (f (j)) \land a (j) = \underset{i \in x}{\sum_{C}} (f (j) (i) \cdot_{C} i))$
306	305	r19.21bi	$⊢ (((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \land j \in y) \to ({finSupp}_{0_{Scalar (C)}} (f (j)) \land a (j) = \underset{i \in x}{\sum_{C}} (f (j) (i) \cdot_{C} i))$
307	306	simpld	$⊢ (((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \land j \in y) \to {finSupp}_{0_{Scalar (C)}} (f (j))$
308	306	simprd	$⊢ (((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \land j \in y) \to a (j) = \underset{i \in x}{\sum_{C}} (f (j) (i) \cdot_{C} i)$
309	1 2 3 4 5 275 276 277 278 279 81 174 280 281 283 284 285 291 292 307 308	fedgmullem1	$⊢ ((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \to ({finSupp}_{0_{Scalar (A)}} ((w \in y, v \in x ⟼ f (w) (v))) \land z = \sum_{A} ((w \in y, v \in x ⟼ f (w) (v)) {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)))$
310	268 274 309	rspcedvd	$⊢ ((((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land f : y ⟶ {Base}_{Scalar (C)}^{x}) \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v))) \to \exists c \in ({Base}_{Scalar (A)}^{(y \times x)}) ({finSupp}_{0_{Scalar (A)}} (c) \land z = \sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)))$
311	310	anasss	$⊢ (((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \land (f : y ⟶ {Base}_{Scalar (C)}^{x} \land \forall w \in y ({finSupp}_{0_{Scalar (C)}} (f (w)) \land a (w) = \underset{v \in x}{\sum_{C}} (f (w) (v) \cdot_{C} v)))) \to \exists c \in ({Base}_{Scalar (A)}^{(y \times x)}) ({finSupp}_{0_{Scalar (A)}} (c) \land z = \sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)))$
312	244 311	exlimddv	$⊢ ((((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land {finSupp}_{0_{Scalar (B)}} (a)) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)) \to \exists c \in ({Base}_{Scalar (A)}^{(y \times x)}) ({finSupp}_{0_{Scalar (A)}} (c) \land z = \sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)))$
313	312	anasss	$⊢ (((((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \land a \in ({Base}_{Scalar (B)}^{y})) \land ({finSupp}_{0_{Scalar (B)}} (a) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w))) \to \exists c \in ({Base}_{Scalar (A)}^{(y \times x)}) ({finSupp}_{0_{Scalar (A)}} (c) \land z = \sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)))$
314		eqid	$⊢ LSpan (B) = LSpan (B)$
315	59 28 314	islbs4	$⊢ y \in LBasis (B) \leftrightarrow (y \in LIndS (B) \land LSpan (B) (y) = {Base}_{B})$
316	315	bilani	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to (y \in LIndS (B) \land LSpan (B) (y) = {Base}_{B})$
317	316	simprd	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to LSpan (B) (y) = {Base}_{B}$
318	317	adantr	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \to LSpan (B) (y) = {Base}_{B}$
319	74 63	eqtr3d	$⊢ φ \to {Base}_{A} = {Base}_{B}$
320	319	ad3antrrr	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \to {Base}_{A} = {Base}_{B}$
321	318 320	eqtr4d	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \to LSpan (B) (y) = {Base}_{A}$
322	282 321	eleqtrrd	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \to z \in LSpan (B) (y)$
323		eqid	$⊢ Scalar (B) = Scalar (B)$
324	27	lveclmodd	$⊢ φ \to B \in LMod$
325	324	ad2antrr	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to B \in LMod$
326	314 59 84 323 87 85 325 61	ellspds	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to (z \in LSpan (B) (y) \leftrightarrow \exists a \in ({Base}_{Scalar (B)}^{y}) ({finSupp}_{0_{Scalar (B)}} (a) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w)))$
327	326	biimpa	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in LSpan (B) (y)) \to \exists a \in ({Base}_{Scalar (B)}^{y}) ({finSupp}_{0_{Scalar (B)}} (a) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w))$
328	200 322 327	syl2anc	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \to \exists a \in ({Base}_{Scalar (B)}^{y}) ({finSupp}_{0_{Scalar (B)}} (a) \land z = \underset{w \in y}{\sum_{B}} (a (w) \cdot_{B} w))$
329	313 328	r19.29a	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \to \exists c \in ({Base}_{Scalar (A)}^{(y \times x)}) ({finSupp}_{0_{Scalar (A)}} (c) \land z = \sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w)))$
330		eqid	$⊢ {Base}_{Scalar (A)} = {Base}_{Scalar (A)}$
331	197 182 330 183 186 184 83 165 153	ellspd	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to (z \in LSpan (A) ((w \in y, t \in x ⟼ t \cdot_{E} w) [y \times x]) \leftrightarrow \exists c \in ({Base}_{Scalar (A)}^{(y \times x)}) ({finSupp}_{0_{Scalar (A)}} (c) \land z = \sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w))))$
332	331	adantr	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \to (z \in LSpan (A) ((w \in y, t \in x ⟼ t \cdot_{E} w) [y \times x]) \leftrightarrow \exists c \in ({Base}_{Scalar (A)}^{(y \times x)}) ({finSupp}_{0_{Scalar (A)}} (c) \land z = \sum_{A} (c {\cdot_{A}}_{f} (w \in y, t \in x ⟼ t \cdot_{E} w))))$
333	329 332	mpbird	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \to z \in LSpan (A) ((w \in y, t \in x ⟼ t \cdot_{E} w) [y \times x])$
334	83	ffnd	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to (w \in y, t \in x ⟼ t \cdot_{E} w) Fn (y \times x)$
335	334	adantr	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \to (w \in y, t \in x ⟼ t \cdot_{E} w) Fn (y \times x)$
336		fnima	$⊢ (w \in y, t \in x ⟼ t \cdot_{E} w) Fn (y \times x) \to (w \in y, t \in x ⟼ t \cdot_{E} w) [y \times x] = ran (w \in y, t \in x ⟼ t \cdot_{E} w)$
337	335 336	syl	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \to (w \in y, t \in x ⟼ t \cdot_{E} w) [y \times x] = ran (w \in y, t \in x ⟼ t \cdot_{E} w)$
338	337	fveq2d	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \to LSpan (A) ((w \in y, t \in x ⟼ t \cdot_{E} w) [y \times x]) = LSpan (A) (ran (w \in y, t \in x ⟼ t \cdot_{E} w))$
339	333 338	eleqtrd	$⊢ (((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \land z \in {Base}_{A}) \to z \in LSpan (A) (ran (w \in y, t \in x ⟼ t \cdot_{E} w))$
340	199 339	eqelssd	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to LSpan (A) (ran (w \in y, t \in x ⟼ t \cdot_{E} w)) = {Base}_{A}$
341		eqid	$⊢ {Base}_{(w \in y, t \in x ⟼ t \cdot_{E} w)} = {Base}_{(w \in y, t \in x ⟼ t \cdot_{E} w)}$
342		drngnzr	$⊢ K \in DivRing \to K \in NzRing$
343	8 342	syl	$⊢ φ \to K \in NzRing$
344	255 343	eqeltrrd	$⊢ φ \to Scalar (A) \in NzRing$
345	344	ad2antrr	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to Scalar (A) \in NzRing$
346	182 341 183 184 185 186 197 165 345 153 152	lindflbs	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to (ran (w \in y, t \in x ⟼ t \cdot_{E} w) \in LBasis (A) \leftrightarrow ((w \in y, t \in x ⟼ t \cdot_{E} w) LIndF A \land LSpan (A) (ran (w \in y, t \in x ⟼ t \cdot_{E} w)) = {Base}_{A}))$
347	190 340 346	mpbir2and	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to ran (w \in y, t \in x ⟼ t \cdot_{E} w) \in LBasis (A)$
348		eqid	$⊢ LBasis (A) = LBasis (A)$
349	348	dimval	$⊢ (A \in LVec \land ran (w \in y, t \in x ⟼ t \cdot_{E} w) \in LBasis (A)) \to \dim (A) = \|ran (w \in y, t \in x ⟼ t \cdot_{E} w)\|$
350	163 347 349	syl2anc	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to \dim (A) = \|ran (w \in y, t \in x ⟼ t \cdot_{E} w)\|$
351	28	dimval	$⊢ (B \in LVec \land y \in LBasis (B)) \to \dim (B) = \|y\|$
352	88 58 351	syl2anc	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to \dim (B) = \|y\|$
353	23	dimval	$⊢ (C \in LVec \land x \in LBasis (C)) \to \dim (C) = \|x\|$
354	106 38 353	syl2anc	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to \dim (C) = \|x\|$
355	352 354	oveq12d	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to \dim (B) \cdot_{𝑒} \dim (C) = \|y\| \cdot_{𝑒} \|x\|$
356	160 350 355	3eqtr4d	$⊢ ((φ \land x \in LBasis (C)) \land y \in LBasis (B)) \to \dim (A) = \dim (B) \cdot_{𝑒} \dim (C)$
357	33 356	exlimddv	$⊢ (φ \land x \in LBasis (C)) \to \dim (A) = \dim (B) \cdot_{𝑒} \dim (C)$
358	25 357	n0limd	$⊢ φ \to \dim (A) = \dim (B) \cdot_{𝑒} \dim (C)$

Metamath Proof Explorer

Theorem fedgmul

Proof