Theorem matunitlindflem2 37577

Description: One direction of matunitlindf 37578. (Contributed by Brendan Leahy, 2-Jun-2021.)

Assertion

Ref	Expression
matunitlindflem2	⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))

Proof of Theorem matunitlindflem2

Dummy variables 𝑓 𝑖 𝑗 𝑘 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2740	. . . . . . 7 ⊢ (𝐼 Mat 𝑅) = (𝐼 Mat 𝑅)
2		eqid 2740	. . . . . . 7 ⊢ (Base‘(𝐼 Mat 𝑅)) = (Base‘(𝐼 Mat 𝑅))
3	1, 2	matrcl 22437	. . . . . 6 ⊢ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → (𝐼 ∈ Fin ∧ 𝑅 ∈ V))
4	3	simpld 494	. . . . 5 ⊢ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → 𝐼 ∈ Fin)
5	4	ad3antlr 730	. . . 4 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → 𝐼 ∈ Fin)
6		isfld 20762	. . . . . . 7 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
7	6	simplbi 497	. . . . . 6 ⊢ (𝑅 ∈ Field → 𝑅 ∈ DivRing)
8	7	anim1i 614	. . . . 5 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))))
9	4	ad2antrl 727	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → 𝐼 ∈ Fin)
10		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 ∈ (Base‘(𝐼 Mat 𝑅)))
11		xpfi 9386	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐼 ∈ Fin ∧ 𝐼 ∈ Fin) → (𝐼 × 𝐼) ∈ Fin)
12	11	anidms 566	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ Fin → (𝐼 × 𝐼) ∈ Fin)
13		eqid 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 freeLMod (𝐼 × 𝐼)) = (𝑅 freeLMod (𝐼 × 𝐼))
14		eqid 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Base‘𝑅) = (Base‘𝑅)
15	13, 14	frlmfibas 21805	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ DivRing ∧ (𝐼 × 𝐼) ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
16	12, 15	sylan2 592	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
17	1, 13	matbas 22438	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
18	17	ancoms 458	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
19	16, 18	eqtrd 2780	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
20	19	eleq2d 2830	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))))
21	4, 20	sylan2 592	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))))
22		fvex 6933	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝑅) ∈ V
23	4, 4, 11	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → (𝐼 × 𝐼) ∈ Fin)
24		elmapg 8897	. . . . . . . . . . . . . . . . . 18 ⊢ (((Base‘𝑅) ∈ V ∧ (𝐼 × 𝐼) ∈ Fin) → (𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)))
25	22, 23, 24	sylancr 586	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → (𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)))
26	25	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)))
27	21, 26	bitr3d 281	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)))
28	10, 27	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅))
29	28	adantrr 716	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅))
30		eldifsn 4811	. . . . . . . . . . . . . . . 16 ⊢ (𝐼 ∈ (Fin ∖ {∅}) ↔ (𝐼 ∈ Fin ∧ 𝐼 ≠ ∅))
31	30	biimpri 228	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ Fin ∧ 𝐼 ≠ ∅) → 𝐼 ∈ (Fin ∖ {∅}))
32	4, 31	sylan 579	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅) → 𝐼 ∈ (Fin ∖ {∅}))
33	32	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → 𝐼 ∈ (Fin ∖ {∅}))
34		curf 37558	. . . . . . . . . . . . . 14 ⊢ ((𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅) ∧ 𝐼 ∈ (Fin ∖ {∅}) ∧ (Base‘𝑅) ∈ V) → curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))
35	22, 34	mp3an3 1450	. . . . . . . . . . . . 13 ⊢ ((𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅) ∧ 𝐼 ∈ (Fin ∖ {∅})) → curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))
36	29, 33, 35	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))
37	9, 36	jca 511	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)))
38	37	ex 412	. . . . . . . . . 10 ⊢ (𝑅 ∈ DivRing → ((𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅) → (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))))
39	38	imdistani 568	. . . . . . . . 9 ⊢ ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → (𝑅 ∈ DivRing ∧ (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))))
40	39	anassrs 467	. . . . . . . 8 ⊢ (((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) → (𝑅 ∈ DivRing ∧ (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))))
41		anass 468	. . . . . . . 8 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ↔ (𝑅 ∈ DivRing ∧ (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))))
42	40, 41	sylibr 234	. . . . . . 7 ⊢ (((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) → ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)))
43		drngring 20758	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring)
44		eqid 2740	. . . . . . . . . . . . . 14 ⊢ (𝑅 unitVec 𝐼) = (𝑅 unitVec 𝐼)
45		eqid 2740	. . . . . . . . . . . . . 14 ⊢ (𝑅 freeLMod 𝐼) = (𝑅 freeLMod 𝐼)
46		eqid 2740	. . . . . . . . . . . . . 14 ⊢ (Base‘(𝑅 freeLMod 𝐼)) = (Base‘(𝑅 freeLMod 𝐼))
47	44, 45, 46	uvcff 21834	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (𝑅 unitVec 𝐼):𝐼⟶(Base‘(𝑅 freeLMod 𝐼)))
48	43, 47	sylan 579	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑅 unitVec 𝐼):𝐼⟶(Base‘(𝑅 freeLMod 𝐼)))
49	48	ffvelcdmda 7118	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) → ((𝑅 unitVec 𝐼)‘𝑖) ∈ (Base‘(𝑅 freeLMod 𝐼)))
50	49	ad4ant14 751	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖 ∈ 𝐼) → ((𝑅 unitVec 𝐼)‘𝑖) ∈ (Base‘(𝑅 freeLMod 𝐼)))
51		ffn 6747	. . . . . . . . . . . . . . . 16 ⊢ (curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) → curry 𝑀 Fn 𝐼)
52		fnima 6710	. . . . . . . . . . . . . . . 16 ⊢ (curry 𝑀 Fn 𝐼 → (curry 𝑀 “ 𝐼) = ran curry 𝑀)
53	51, 52	syl 17	. . . . . . . . . . . . . . 15 ⊢ (curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) → (curry 𝑀 “ 𝐼) = ran curry 𝑀)
54	53	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → (curry 𝑀 “ 𝐼) = ran curry 𝑀)
55	54	fveq2d 6924	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) = ((LSpan‘(𝑅 freeLMod 𝐼))‘ran curry 𝑀))
56	55	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) = ((LSpan‘(𝑅 freeLMod 𝐼))‘ran curry 𝑀))
57		simplll 774	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → 𝑅 ∈ DivRing)
58		simpllr 775	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → 𝐼 ∈ Fin)
59	45	frlmlmod 21792	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (𝑅 freeLMod 𝐼) ∈ LMod)
60	43, 59	sylan 579	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑅 freeLMod 𝐼) ∈ LMod)
61	60	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → (𝑅 freeLMod 𝐼) ∈ LMod)
62		lindfrn 21864	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 freeLMod 𝐼) ∈ LMod ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ran curry 𝑀 ∈ (LIndS‘(𝑅 freeLMod 𝐼)))
63	61, 62	sylan 579	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ran curry 𝑀 ∈ (LIndS‘(𝑅 freeLMod 𝐼)))
64	45	frlmsca 21796	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝑅 = (Scalar‘(𝑅 freeLMod 𝐼)))
65		drngnzr 20770	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing)
66	65	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝑅 ∈ NzRing)
67	64, 66	eqeltrrd 2845	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing)
68	60, 67	jca 511	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing))
69		eqid 2740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Scalar‘(𝑅 freeLMod 𝐼)) = (Scalar‘(𝑅 freeLMod 𝐼))
70	46, 69	lindff1 21863	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:dom curry 𝑀–1-1→(Base‘(𝑅 freeLMod 𝐼)))
71	70	3expa 1118	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:dom curry 𝑀–1-1→(Base‘(𝑅 freeLMod 𝐼)))
72	68, 71	sylan 579	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:dom curry 𝑀–1-1→(Base‘(𝑅 freeLMod 𝐼)))
73		fdm 6756	. . . . . . . . . . . . . . . . . . 19 ⊢ (curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) → dom curry 𝑀 = 𝐼)
74		f1eq2 6813	. . . . . . . . . . . . . . . . . . . 20 ⊢ (dom curry 𝑀 = 𝐼 → (curry 𝑀:dom curry 𝑀–1-1→(Base‘(𝑅 freeLMod 𝐼)) ↔ curry 𝑀:𝐼–1-1→(Base‘(𝑅 freeLMod 𝐼))))
75	74	biimpac 478	. . . . . . . . . . . . . . . . . . 19 ⊢ ((curry 𝑀:dom curry 𝑀–1-1→(Base‘(𝑅 freeLMod 𝐼)) ∧ dom curry 𝑀 = 𝐼) → curry 𝑀:𝐼–1-1→(Base‘(𝑅 freeLMod 𝐼)))
76	72, 73, 75	syl2an 595	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → curry 𝑀:𝐼–1-1→(Base‘(𝑅 freeLMod 𝐼)))
77	76	an32s 651	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:𝐼–1-1→(Base‘(𝑅 freeLMod 𝐼)))
78		f1f1orn 6873	. . . . . . . . . . . . . . . . 17 ⊢ (curry 𝑀:𝐼–1-1→(Base‘(𝑅 freeLMod 𝐼)) → curry 𝑀:𝐼–1-1-onto→ran curry 𝑀)
79	77, 78	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:𝐼–1-1-onto→ran curry 𝑀)
80		f1oeng 9031	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ Fin ∧ curry 𝑀:𝐼–1-1-onto→ran curry 𝑀) → 𝐼 ≈ ran curry 𝑀)
81	58, 79, 80	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → 𝐼 ≈ ran curry 𝑀)
82	81	ensymd 9065	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ran curry 𝑀 ≈ 𝐼)
83		lindsenlbs 37575	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ ran curry 𝑀 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ ran curry 𝑀 ≈ 𝐼) → ran curry 𝑀 ∈ (LBasis‘(𝑅 freeLMod 𝐼)))
84	57, 58, 63, 82, 83	syl31anc 1373	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ran curry 𝑀 ∈ (LBasis‘(𝑅 freeLMod 𝐼)))
85		eqid 2740	. . . . . . . . . . . . . 14 ⊢ (LBasis‘(𝑅 freeLMod 𝐼)) = (LBasis‘(𝑅 freeLMod 𝐼))
86		eqid 2740	. . . . . . . . . . . . . 14 ⊢ (LSpan‘(𝑅 freeLMod 𝐼)) = (LSpan‘(𝑅 freeLMod 𝐼))
87	46, 85, 86	lbssp 21101	. . . . . . . . . . . . 13 ⊢ (ran curry 𝑀 ∈ (LBasis‘(𝑅 freeLMod 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘ran curry 𝑀) = (Base‘(𝑅 freeLMod 𝐼)))
88	84, 87	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘ran curry 𝑀) = (Base‘(𝑅 freeLMod 𝐼)))
89	56, 88	eqtrd 2780	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) = (Base‘(𝑅 freeLMod 𝐼)))
90	89	adantr 480	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖 ∈ 𝐼) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) = (Base‘(𝑅 freeLMod 𝐼)))
91	50, 90	eleqtrrd 2847	. . . . . . . . 9 ⊢ (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖 ∈ 𝐼) → ((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)))
92		eqid 2740	. . . . . . . . . . . . 13 ⊢ (Base‘(Scalar‘(𝑅 freeLMod 𝐼))) = (Base‘(Scalar‘(𝑅 freeLMod 𝐼)))
93		eqid 2740	. . . . . . . . . . . . 13 ⊢ (0g‘(Scalar‘(𝑅 freeLMod 𝐼))) = (0g‘(Scalar‘(𝑅 freeLMod 𝐼)))
94		eqid 2740	. . . . . . . . . . . . 13 ⊢ ( ·𝑠 ‘(𝑅 freeLMod 𝐼)) = ( ·𝑠 ‘(𝑅 freeLMod 𝐼))
95	45, 14	frlmfibas 21805	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m 𝐼) = (Base‘(𝑅 freeLMod 𝐼)))
96	95	feq3d 6734	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) ↔ curry 𝑀:𝐼⟶(Base‘(𝑅 freeLMod 𝐼))))
97	96	biimpa 476	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → curry 𝑀:𝐼⟶(Base‘(𝑅 freeLMod 𝐼)))
98	59	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → (𝑅 freeLMod 𝐼) ∈ LMod)
99		simplr 768	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → 𝐼 ∈ Fin)
100	86, 46, 92, 69, 93, 94, 97, 98, 99	elfilspd 21846	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → (((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) ↔ ∃𝑛 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = ((𝑅 freeLMod 𝐼) Σg (𝑛 ∘f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀))))
101	45	frlmsca 21796	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → 𝑅 = (Scalar‘(𝑅 freeLMod 𝐼)))
102	101	fveq2d 6924	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (Base‘𝑅) = (Base‘(Scalar‘(𝑅 freeLMod 𝐼))))
103	102	oveq1d 7463	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m 𝐼) = ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ↑m 𝐼))
104	103	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → ((Base‘𝑅) ↑m 𝐼) = ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ↑m 𝐼))
105		elmapi 8907	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ((Base‘𝑅) ↑m 𝐼) → 𝑛:𝐼⟶(Base‘𝑅))
106		ffn 6747	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛:𝐼⟶(Base‘𝑅) → 𝑛 Fn 𝐼)
107	106	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → 𝑛 Fn 𝐼)
108	51	ad2antlr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → curry 𝑀 Fn 𝐼)
109		simpllr 775	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → 𝐼 ∈ Fin)
110		inidm 4248	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐼 ∩ 𝐼) = 𝐼
111		eqidd 2741	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝑛‘𝑘) = (𝑛‘𝑘))
112		eqidd 2741	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘) = (curry 𝑀‘𝑘))
113	107, 108, 109, 109, 110, 111, 112	offval 7723	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑛 ∘f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀) = (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)( ·𝑠 ‘(𝑅 freeLMod 𝐼))(curry 𝑀‘𝑘))))
114		simp-4r 783	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → 𝐼 ∈ Fin)
115		ffvelcdm 7115	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛:𝐼⟶(Base‘𝑅) ∧ 𝑘 ∈ 𝐼) → (𝑛‘𝑘) ∈ (Base‘𝑅))
116	115	adantll 713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝑛‘𝑘) ∈ (Base‘𝑅))
117		ffvelcdm 7115	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘) ∈ ((Base‘𝑅) ↑m 𝐼))
118	117	ad4ant24 753	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘) ∈ ((Base‘𝑅) ↑m 𝐼))
119	95	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → ((Base‘𝑅) ↑m 𝐼) = (Base‘(𝑅 freeLMod 𝐼)))
120	118, 119	eleqtrd 2846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘) ∈ (Base‘(𝑅 freeLMod 𝐼)))
121		eqid 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (.r‘𝑅) = (.r‘𝑅)
122	45, 46, 14, 114, 116, 120, 94, 121	frlmvscafval 21809	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝑛‘𝑘)( ·𝑠 ‘(𝑅 freeLMod 𝐼))(curry 𝑀‘𝑘)) = ((𝐼 × {(𝑛‘𝑘)}) ∘f (.r‘𝑅)(curry 𝑀‘𝑘)))
123		fvex 6933	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛‘𝑘) ∈ V
124		fnconstg 6809	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛‘𝑘) ∈ V → (𝐼 × {(𝑛‘𝑘)}) Fn 𝐼)
125	123, 124	mp1i 13	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝐼 × {(𝑛‘𝑘)}) Fn 𝐼)
126		elmapfn 8923	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((curry 𝑀‘𝑘) ∈ ((Base‘𝑅) ↑m 𝐼) → (curry 𝑀‘𝑘) Fn 𝐼)
127	117, 126	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘) Fn 𝐼)
128	127	ad4ant24 753	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘) Fn 𝐼)
129	123	fvconst2 7241	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ 𝐼 → ((𝐼 × {(𝑛‘𝑘)})‘𝑗) = (𝑛‘𝑘))
130	129	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((𝐼 × {(𝑛‘𝑘)})‘𝑗) = (𝑛‘𝑘))
131		eqidd 2741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((curry 𝑀‘𝑘)‘𝑗) = ((curry 𝑀‘𝑘)‘𝑗))
132	125, 128, 114, 114, 110, 130, 131	offval 7723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝐼 × {(𝑛‘𝑘)}) ∘f (.r‘𝑅)(curry 𝑀‘𝑘)) = (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))
133	122, 132	eqtrd 2780	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝑛‘𝑘)( ·𝑠 ‘(𝑅 freeLMod 𝐼))(curry 𝑀‘𝑘)) = (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))
134	133	mpteq2dva 5266	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)( ·𝑠 ‘(𝑅 freeLMod 𝐼))(curry 𝑀‘𝑘))) = (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))))
135	113, 134	eqtrd 2780	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑛 ∘f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀) = (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))))
136	135	oveq2d 7464	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → ((𝑅 freeLMod 𝐼) Σg (𝑛 ∘f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀)) = ((𝑅 freeLMod 𝐼) Σg (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))))
137		eqid 2740	. . . . . . . . . . . . . . . . 17 ⊢ (0g‘(𝑅 freeLMod 𝐼)) = (0g‘(𝑅 freeLMod 𝐼))
138		simplll 774	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → 𝑅 ∈ Ring)
139		simp-5l 784	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑅 ∈ Ring)
140	115	ad4ant23 752	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑛‘𝑘) ∈ (Base‘𝑅))
141		simplr 768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))
142		elmapi 8907	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((curry 𝑀‘𝑘) ∈ ((Base‘𝑅) ↑m 𝐼) → (curry 𝑀‘𝑘):𝐼⟶(Base‘𝑅))
143	117, 142	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘):𝐼⟶(Base‘𝑅))
144	143	ffvelcdmda 7118	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((curry 𝑀‘𝑘)‘𝑗) ∈ (Base‘𝑅))
145	141, 144	sylanl1 679	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((curry 𝑀‘𝑘)‘𝑗) ∈ (Base‘𝑅))
146	14, 121	ringcl 20277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ (𝑛‘𝑘) ∈ (Base‘𝑅) ∧ ((curry 𝑀‘𝑘)‘𝑗) ∈ (Base‘𝑅)) → ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)) ∈ (Base‘𝑅))
147	139, 140, 145, 146	syl3anc 1371	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)) ∈ (Base‘𝑅))
148	147	fmpttd 7149	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))):𝐼⟶(Base‘𝑅))
149		elmapg 8897	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((Base‘𝑅) ∈ V ∧ 𝐼 ∈ Fin) → ((𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ ((Base‘𝑅) ↑m 𝐼) ↔ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))):𝐼⟶(Base‘𝑅)))
150	22, 149	mpan 689	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐼 ∈ Fin → ((𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ ((Base‘𝑅) ↑m 𝐼) ↔ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))):𝐼⟶(Base‘𝑅)))
151	150	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ ((Base‘𝑅) ↑m 𝐼) ↔ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))):𝐼⟶(Base‘𝑅)))
152	95	eleq2d 2830	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ ((Base‘𝑅) ↑m 𝐼) ↔ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ (Base‘(𝑅 freeLMod 𝐼))))
153	151, 152	bitr3d 281	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))):𝐼⟶(Base‘𝑅) ↔ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ (Base‘(𝑅 freeLMod 𝐼))))
154	153	ad3antrrr 729	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))):𝐼⟶(Base‘𝑅) ↔ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ (Base‘(𝑅 freeLMod 𝐼))))
155	148, 154	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ (Base‘(𝑅 freeLMod 𝐼)))
156		mptexg 7258	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐼 ∈ Fin → (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ V)
157	156	ralrimivw 3156	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ Fin → ∀𝑘 ∈ 𝐼 (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ V)
158		eqid 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))) = (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))
159	158	fnmpt 6720	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑘 ∈ 𝐼 (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ V → (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))) Fn 𝐼)
160	157, 159	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐼 ∈ Fin → (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))) Fn 𝐼)
161		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐼 ∈ Fin → 𝐼 ∈ Fin)
162		fvexd 6935	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐼 ∈ Fin → (0g‘(𝑅 freeLMod 𝐼)) ∈ V)
163	160, 161, 162	fndmfifsupp 9447	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐼 ∈ Fin → (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))) finSupp (0g‘(𝑅 freeLMod 𝐼)))
164	163	ad3antlr 730	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))) finSupp (0g‘(𝑅 freeLMod 𝐼)))
165	45, 46, 137, 109, 109, 138, 155, 164	frlmgsum 21815	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → ((𝑅 freeLMod 𝐼) Σg (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))))
166	136, 165	eqtr2d 2781	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) = ((𝑅 freeLMod 𝐼) Σg (𝑛 ∘f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀)))
167	105, 166	sylan2 592	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)) → (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) = ((𝑅 freeLMod 𝐼) Σg (𝑛 ∘f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀)))
168	167	eqeq2d 2751	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ((𝑅 unitVec 𝐼)‘𝑖) = ((𝑅 freeLMod 𝐼) Σg (𝑛 ∘f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀))))
169	104, 168	rexeqbidva 3341	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → (∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ∃𝑛 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = ((𝑅 freeLMod 𝐼) Σg (𝑛 ∘f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀))))
170	100, 169	bitr4d 282	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → (((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) ↔ ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))))))
171	43, 170	sylanl1 679	. . . . . . . . . 10 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → (((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) ↔ ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))))))
172	171	ad2antrr 725	. . . . . . . . 9 ⊢ (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖 ∈ 𝐼) → (((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) ↔ ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))))))
173	91, 172	mpbid 232	. . . . . . . 8 ⊢ (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖 ∈ 𝐼) → ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))))
174	173	ralrimiva 3152	. . . . . . 7 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))))
175	42, 174	sylan 579	. . . . . 6 ⊢ ((((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))))
176	10, 21	mpbird 257	. . . . . . . . 9 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)))
177		elmapfn 8923	. . . . . . . . 9 ⊢ (𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) → 𝑀 Fn (𝐼 × 𝐼))
178	176, 177	syl 17	. . . . . . . 8 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 Fn (𝐼 × 𝐼))
179	4	adantl 481	. . . . . . . 8 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝐼 ∈ Fin)
180		an32 645	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗 ∈ 𝐼) ∧ 𝑘 ∈ 𝐼) ↔ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼))
181		df-3an 1089	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ 𝐼) ↔ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼))
182	180, 181	bitr4i 278	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗 ∈ 𝐼) ∧ 𝑘 ∈ 𝐼) ↔ (𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ 𝐼))
183		curfv 37560	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ 𝐼) ∧ 𝐼 ∈ Fin) → ((curry 𝑀‘𝑘)‘𝑗) = (𝑘𝑀𝑗))
184	182, 183	sylanb 580	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗 ∈ 𝐼) ∧ 𝑘 ∈ 𝐼) ∧ 𝐼 ∈ Fin) → ((curry 𝑀‘𝑘)‘𝑗) = (𝑘𝑀𝑗))
185	184	an32s 651	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗 ∈ 𝐼) ∧ 𝐼 ∈ Fin) ∧ 𝑘 ∈ 𝐼) → ((curry 𝑀‘𝑘)‘𝑗) = (𝑘𝑀𝑗))
186	185	oveq2d 7464	. . . . . . . . . . . . . . 15 ⊢ ((((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗 ∈ 𝐼) ∧ 𝐼 ∈ Fin) ∧ 𝑘 ∈ 𝐼) → ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)) = ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))
187	186	mpteq2dva 5266	. . . . . . . . . . . . . 14 ⊢ (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗 ∈ 𝐼) ∧ 𝐼 ∈ Fin) → (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) = (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))
188	187	an32s 651	. . . . . . . . . . . . 13 ⊢ (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) ∧ 𝑗 ∈ 𝐼) → (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) = (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))
189	188	oveq2d 7464	. . . . . . . . . . . 12 ⊢ (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) ∧ 𝑗 ∈ 𝐼) → (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))) = (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
190	189	mpteq2dva 5266	. . . . . . . . . . 11 ⊢ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) → (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))))
191	190	eqeq2d 2751	. . . . . . . . . 10 ⊢ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
192	191	rexbidv 3185	. . . . . . . . 9 ⊢ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) → (∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
193	192	ralbidv 3184	. . . . . . . 8 ⊢ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) → (∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
194	178, 179, 193	syl2anc 583	. . . . . . 7 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
195	194	ad2antrr 725	. . . . . 6 ⊢ ((((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → (∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
196	175, 195	mpbid 232	. . . . 5 ⊢ ((((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))))
197	8, 196	sylanl1 679	. . . 4 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))))
198		fveq1 6919	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑓‘𝑖) → (𝑛‘𝑘) = ((𝑓‘𝑖)‘𝑘))
199		uncov 37561	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ V ∧ 𝑘 ∈ V) → (𝑖uncurry 𝑓𝑘) = ((𝑓‘𝑖)‘𝑘))
200	199	el2v 3495	. . . . . . . . . . 11 ⊢ (𝑖uncurry 𝑓𝑘) = ((𝑓‘𝑖)‘𝑘)
201	198, 200	eqtr4di 2798	. . . . . . . . . 10 ⊢ (𝑛 = (𝑓‘𝑖) → (𝑛‘𝑘) = (𝑖uncurry 𝑓𝑘))
202	201	oveq1d 7463	. . . . . . . . 9 ⊢ (𝑛 = (𝑓‘𝑖) → ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)) = ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))
203	202	mpteq2dv 5268	. . . . . . . 8 ⊢ (𝑛 = (𝑓‘𝑖) → (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))) = (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))
204	203	oveq2d 7464	. . . . . . 7 ⊢ (𝑛 = (𝑓‘𝑖) → (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))) = (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
205	204	mpteq2dv 5268	. . . . . 6 ⊢ (𝑛 = (𝑓‘𝑖) → (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))))
206	205	eqeq2d 2751	. . . . 5 ⊢ (𝑛 = (𝑓‘𝑖) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) ↔ ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
207	206	ac6sfi 9348	. . . 4 ⊢ ((𝐼 ∈ Fin ∧ ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → ∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
208	5, 197, 207	syl2anc 583	. . 3 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
209		uncf 37559	. . . . . . 7 ⊢ (𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) → uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅))
210	13, 14	frlmfibas 21805	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ Field ∧ (𝐼 × 𝐼) ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
211	12, 210	sylan2 592	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
212	1, 13	matbas 22438	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ Field) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
213	212	ancoms 458	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
214	211, 213	eqtrd 2780	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
215	4, 214	sylan2 592	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
216	215	eleq2d 2830	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (uncurry 𝑓 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅))))
217		elmapg 8897	. . . . . . . . . . . . . 14 ⊢ (((Base‘𝑅) ∈ V ∧ (𝐼 × 𝐼) ∈ Fin) → (uncurry 𝑓 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)))
218	22, 23, 217	sylancr 586	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → (uncurry 𝑓 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)))
219	218	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (uncurry 𝑓 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)))
220	216, 219	bitr3d 281	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)) ↔ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)))
221	220	biimpar 477	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)))
222	221	adantr 480	. . . . . . . . 9 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)))
223		nfv 1913	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗(((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼)
224		nfmpt1 5274	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗(𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
225	224	nfeq2 2926	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
226		fveq1 6919	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) → (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗) = ((𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))‘𝑗))
227	7, 43	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∈ Field → 𝑅 ∈ Ring)
228	227, 4	anim12i 612	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑅 ∈ Ring ∧ 𝐼 ∈ Fin))
229	228	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (𝑅 ∈ Ring ∧ 𝐼 ∈ Fin))
230		equcom 2017	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑗 ↔ 𝑗 = 𝑖)
231		ifbi 4570	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖 = 𝑗 ↔ 𝑗 = 𝑖) → if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)) = if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅)))
232	230, 231	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)) = if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))
233		eqid 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1r‘𝑅) = (1r‘𝑅)
234		eqid 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0g‘𝑅) = (0g‘𝑅)
235		simpllr 775	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝐼 ∈ Fin)
236		simplll 774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑅 ∈ Ring)
237		simplr 768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑖 ∈ 𝐼)
238		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑗 ∈ 𝐼)
239		eqid 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1r‘(𝐼 Mat 𝑅)) = (1r‘(𝐼 Mat 𝑅))
240	1, 233, 234, 235, 236, 237, 238, 239	mat1ov 22475	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)))
241		df-3an 1089	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin ∧ 𝑖 ∈ 𝐼) ↔ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼))
242	44, 233, 234	uvcvval 21829	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗) = if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅)))
243	241, 242	sylanbr 581	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗) = if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅)))
244	232, 240, 243	3eqtr4a 2806	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗))
245	229, 244	sylanl1 679	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗))
246		ovex 7481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))) ∈ V
247		eqid 2740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
248	247	fvmpt2 7040	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ 𝐼 ∧ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))) ∈ V) → ((𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))‘𝑗) = (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
249	246, 248	mpan2 690	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ 𝐼 → ((𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))‘𝑗) = (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
250	249	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))‘𝑗) = (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
251		eqid 2740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩) = (𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)
252		simp-4l 782	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑅 ∈ Field)
253	4	ad4antlr 732	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝐼 ∈ Fin)
254	218	biimpar 477	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → uncurry 𝑓 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)))
255	254	ad5ant23 759	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → uncurry 𝑓 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)))
256		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 ∈ (Base‘(𝐼 Mat 𝑅)))
257	256, 215	eleqtrrd 2847	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)))
258	257	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)))
259		simplr 768	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑖 ∈ 𝐼)
260		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑗 ∈ 𝐼)
261	251, 14, 121, 252, 253, 253, 253, 255, 258, 259, 260	mamufv 22419	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑖(uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀)𝑗) = (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
262	1, 251	matmulr 22465	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ Field) → (𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩) = (.r‘(𝐼 Mat 𝑅)))
263	262	ancoms 458	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩) = (.r‘(𝐼 Mat 𝑅)))
264	263	oveqd 7465	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀))
265	264	oveqd 7465	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (𝑖(uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀)𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))
266	4, 265	sylan2 592	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑖(uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀)𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))
267	266	ad3antrrr 729	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑖(uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀)𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))
268	250, 261, 267	3eqtr2rd 2787	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗) = ((𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))‘𝑗))
269	245, 268	eqeq12d 2756	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗) ↔ (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗) = ((𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))‘𝑗)))
270	226, 269	imbitrrid 246	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
271	270	ex 412	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) → (𝑗 ∈ 𝐼 → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))))
272	271	com23 86	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) → (𝑗 ∈ 𝐼 → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))))
273	223, 225, 272	ralrimd 3270	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) → ∀𝑗 ∈ 𝐼 (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
274	273	ralimdva 3173	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) → ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
275	1, 2, 239	mat1bas 22476	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (1r‘(𝐼 Mat 𝑅)) ∈ (Base‘(𝐼 Mat 𝑅)))
276	13, 14	frlmfibas 21805	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ Ring ∧ (𝐼 × 𝐼) ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
277	12, 276	sylan2 592	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
278	1, 13	matbas 22438	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ Ring) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
279	278	ancoms 458	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
280	277, 279	eqtrd 2780	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
281	275, 280	eleqtrrd 2847	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (1r‘(𝐼 Mat 𝑅)) ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)))
282		elmapfn 8923	. . . . . . . . . . . . . . . 16 ⊢ ((1r‘(𝐼 Mat 𝑅)) ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) → (1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼))
283	281, 282	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼))
284	227, 4, 283	syl2an 595	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼))
285	284	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼))
286	1	matring 22470	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐼 Mat 𝑅) ∈ Ring)
287	4, 227, 286	syl2anr 596	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝐼 Mat 𝑅) ∈ Ring)
288	287	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (𝐼 Mat 𝑅) ∈ Ring)
289		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → 𝑀 ∈ (Base‘(𝐼 Mat 𝑅)))
290		eqid 2740	. . . . . . . . . . . . . . . . 17 ⊢ (.r‘(𝐼 Mat 𝑅)) = (.r‘(𝐼 Mat 𝑅))
291	2, 290	ringcl 20277	. . . . . . . . . . . . . . . 16 ⊢ (((𝐼 Mat 𝑅) ∈ Ring ∧ uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ∈ (Base‘(𝐼 Mat 𝑅)))
292	288, 221, 289, 291	syl3anc 1371	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ∈ (Base‘(𝐼 Mat 𝑅)))
293	215	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
294	292, 293	eleqtrrd 2847	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)))
295		elmapfn 8923	. . . . . . . . . . . . . 14 ⊢ ((uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) Fn (𝐼 × 𝐼))
296	294, 295	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) Fn (𝐼 × 𝐼))
297		eqfnov2 7580	. . . . . . . . . . . . 13 ⊢ (((1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼) ∧ (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) Fn (𝐼 × 𝐼)) → ((1r‘(𝐼 Mat 𝑅)) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ↔ ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
298	285, 296, 297	syl2anc 583	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → ((1r‘(𝐼 Mat 𝑅)) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ↔ ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
299	274, 298	sylibrd 259	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) → (1r‘(𝐼 Mat 𝑅)) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)))
300	299	imp 406	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → (1r‘(𝐼 Mat 𝑅)) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀))
301	300	eqcomd 2746	. . . . . . . . 9 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
302		oveq1 7455	. . . . . . . . . . 11 ⊢ (𝑛 = uncurry 𝑓 → (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀))
303	302	eqeq1d 2742	. . . . . . . . . 10 ⊢ (𝑛 = uncurry 𝑓 → ((𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)) ↔ (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))))
304	303	rspcev 3635	. . . . . . . . 9 ⊢ ((uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
305	222, 301, 304	syl2anc 583	. . . . . . . 8 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
306	305	expl 457	. . . . . . 7 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))))
307	209, 306	sylani 603	. . . . . 6 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))))
308	307	exlimdv 1932	. . . . 5 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))))
309	308	imp 406	. . . 4 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ ∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
310	309	adantlr 714	. . 3 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ ∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
311	208, 310	syldan 590	. 2 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
312	6	simprbi 496	. . . 4 ⊢ (𝑅 ∈ Field → 𝑅 ∈ CRing)
313		eqid 2740	. . . . . . . . . 10 ⊢ (𝐼 maDet 𝑅) = (𝐼 maDet 𝑅)
314	313, 1, 2, 14	mdetcl 22623	. . . . . . . . 9 ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Base‘𝑅))
315	313, 1, 2, 14	mdetcl 22623	. . . . . . . . 9 ⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘𝑛) ∈ (Base‘𝑅))
316		eqid 2740	. . . . . . . . . 10 ⊢ (∥r‘𝑅) = (∥r‘𝑅)
317	14, 316, 121	dvdsrmul 20390	. . . . . . . . 9 ⊢ ((((𝐼 maDet 𝑅)‘𝑀) ∈ (Base‘𝑅) ∧ ((𝐼 maDet 𝑅)‘𝑛) ∈ (Base‘𝑅)) → ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
318	314, 315, 317	syl2an 595	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑅 ∈ CRing ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
319	318	anandis 677	. . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
320	319	anassrs 467	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
321	320	adantrr 716	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
322		fveq2 6920	. . . . . . . . 9 ⊢ ((𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)) → ((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))))
323	1, 2, 313, 121, 290	mdetmul 22650	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = (((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
324	323	3expa 1118	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = (((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
325	324	an32s 651	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = (((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
326	313, 1, 239, 233	mdet1 22628	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ Fin) → ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))) = (1r‘𝑅))
327	4, 326	sylan2 592	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))) = (1r‘𝑅))
328	327	adantr 480	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))) = (1r‘𝑅))
329	325, 328	eqeq12d 2756	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → (((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))) ↔ (((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)) = (1r‘𝑅)))
330	322, 329	imbitrid 244	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)) → (((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)) = (1r‘𝑅)))
331	330	impr 454	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → (((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)) = (1r‘𝑅))
332	331	breq2d 5178	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → (((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)) ↔ ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(1r‘𝑅)))
333		eqid 2740	. . . . . . . 8 ⊢ (Unit‘𝑅) = (Unit‘𝑅)
334	333, 233, 316	crngunit 20404	. . . . . . 7 ⊢ (𝑅 ∈ CRing → (((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅) ↔ ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(1r‘𝑅)))
335	334	ad2antrr 725	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → (((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅) ↔ ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(1r‘𝑅)))
336	332, 335	bitr4d 282	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → (((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)) ↔ ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅)))
337	321, 336	mpbid 232	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))
338	312, 337	sylanl1 679	. . 3 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))
339	338	ad4ant14 751	. 2 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))
340	311, 339	rexlimddv 3167	1 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1537  ∃wex 1777   ∈ wcel 2108   ≠ wne 2946  ∀wral 3067  ∃wrex 3076  Vcvv 3488   ∖ cdif 3973  ∅c0 4352  ifcif 4548  {csn 4648  ⟨cotp 4656   class class class wbr 5166   ↦ cmpt 5249   × cxp 5698  dom cdm 5700  ran crn 5701   “ cima 5703   Fn wfn 6568  ⟶wf 6569  –1-1→wf1 6570  –1-1-onto→wf1o 6572  ‘cfv 6573  (class class class)co 7448   ∘_f cof 7712  curry ccur 8306  uncurry cunc 8307   ↑_m cmap 8884   ≈ cen 9000  Fincfn 9003   finSupp cfsupp 9431  Basecbs 17258  ._rcmulr 17312  Scalarcsca 17314   ·_𝑠 cvsca 17315  0_gc0g 17499   Σ_g cgsu 17500  1_rcur 20208  Ringcrg 20260  CRingccrg 20261  ∥_rcdsr 20380  Unitcui 20381  NzRingcnzr 20538  DivRingcdr 20751  Fieldcfield 20752  LModclmod 20880  LSpanclspn 20992  LBasisclbs 21096   freeLMod cfrlm 21789   unitVec cuvc 21825   LIndF clindf 21847  LIndSclinds 21848   maMul cmmul 22415   Mat cmat 22432   maDet cmdat 22611

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261  ax-addf 11263  ax-mulf 11264

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-xor 1509  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-ot 4657  df-uni 4932  df-int 4971  df-iun 5017  df-iin 5018  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-isom 6582  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-of 7714  df-om 7904  df-1st 8030  df-2nd 8031  df-supp 8202  df-tpos 8267  df-cur 8308  df-unc 8309  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-2o 8523  df-er 8763  df-map 8886  df-pm 8887  df-ixp 8956  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-fsupp 9432  df-sup 9511  df-oi 9579  df-card 10008  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-div 11948  df-nn 12294  df-2 12356  df-3 12357  df-4 12358  df-5 12359  df-6 12360  df-7 12361  df-8 12362  df-9 12363  df-n0 12554  df-xnn0 12626  df-z 12640  df-dec 12759  df-uz 12904  df-rp 13058  df-fz 13568  df-fzo 13712  df-seq 14053  df-exp 14113  df-hash 14380  df-word 14563  df-lsw 14611  df-concat 14619  df-s1 14644  df-substr 14689  df-pfx 14719  df-splice 14798  df-reverse 14807  df-s2 14897  df-struct 17194  df-sets 17211  df-slot 17229  df-ndx 17241  df-base 17259  df-ress 17288  df-plusg 17324  df-mulr 17325  df-starv 17326  df-sca 17327  df-vsca 17328  df-ip 17329  df-tset 17330  df-ple 17331  df-ds 17333  df-unif 17334  df-hom 17335  df-cco 17336  df-0g 17501  df-gsum 17502  df-prds 17507  df-pws 17509  df-mre 17644  df-mrc 17645  df-mri 17646  df-acs 17647  df-mgm 18678  df-sgrp 18757  df-mnd 18773  df-mhm 18818  df-submnd 18819  df-efmnd 18904  df-grp 18976  df-minusg 18977  df-sbg 18978  df-mulg 19108  df-subg 19163  df-ghm 19253  df-gim 19299  df-cntz 19357  df-oppg 19386  df-symg 19411  df-pmtr 19484  df-psgn 19533  df-evpm 19534  df-cmn 19824  df-abl 19825  df-mgp 20162  df-rng 20180  df-ur 20209  df-srg 20214  df-ring 20262  df-cring 20263  df-oppr 20360  df-dvdsr 20383  df-unit 20384  df-invr 20414  df-dvr 20427  df-rhm 20498  df-nzr 20539  df-subrng 20572  df-subrg 20597  df-drng 20753  df-field 20754  df-lmod 20882  df-lss 20953  df-lsp 20993  df-lmhm 21044  df-lbs 21097  df-lvec 21125  df-sra 21195  df-rgmod 21196  df-cnfld 21388  df-zring 21481  df-zrh 21537  df-dsmm 21775  df-frlm 21790  df-uvc 21826  df-lindf 21849  df-linds 21850  df-mamu 22416  df-mat 22433  df-mdet 22612

This theorem is referenced by:  matunitlindf  37578