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)

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

Metamath Proof Explorer

Theorem fedgmul

Proof