Theorem matunitlindflem2 37757

Description: One direction of matunitlindf 37758. (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 2734	. . . . . . 7 ⊢ (𝐼 Mat 𝑅) = (𝐼 Mat 𝑅)
2		eqid 2734	. . . . . . 7 ⊢ (Base‘(𝐼 Mat 𝑅)) = (Base‘(𝐼 Mat 𝑅))
3	1, 2	matrcl 22354	. . . . . 6 ⊢ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → (𝐼 ∈ Fin ∧ 𝑅 ∈ V))
4	3	simpld 494	. . . . 5 ⊢ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → 𝐼 ∈ Fin)
5	4	ad3antlr 731	. . . 4 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → 𝐼 ∈ Fin)
6		isfld 20671	. . . . . . 7 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
7	6	simplbi 497	. . . . . 6 ⊢ (𝑅 ∈ Field → 𝑅 ∈ DivRing)
8	7	anim1i 615	. . . . 5 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))))
9	4	ad2antrl 728	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → 𝐼 ∈ Fin)
10		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 ∈ (Base‘(𝐼 Mat 𝑅)))
11		xpfi 9218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐼 ∈ Fin ∧ 𝐼 ∈ Fin) → (𝐼 × 𝐼) ∈ Fin)
12	11	anidms 566	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ Fin → (𝐼 × 𝐼) ∈ Fin)
13		eqid 2734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 freeLMod (𝐼 × 𝐼)) = (𝑅 freeLMod (𝐼 × 𝐼))
14		eqid 2734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Base‘𝑅) = (Base‘𝑅)
15	13, 14	frlmfibas 21715	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ DivRing ∧ (𝐼 × 𝐼) ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
16	12, 15	sylan2 593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
17	1, 13	matbas 22355	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
18	17	ancoms 458	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
19	16, 18	eqtrd 2769	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
20	19	eleq2d 2820	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))))
21	4, 20	sylan2 593	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))))
22		fvex 6845	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝑅) ∈ V
23	4, 4, 11	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → (𝐼 × 𝐼) ∈ Fin)
24		elmapg 8774	. . . . . . . . . . . . . . . . . 18 ⊢ (((Base‘𝑅) ∈ V ∧ (𝐼 × 𝐼) ∈ Fin) → (𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)))
25	22, 23, 24	sylancr 587	. . . . . . . . . . . . . . . . 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 717	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅))
30		eldifsn 4740	. . . . . . . . . . . . . . . 16 ⊢ (𝐼 ∈ (Fin ∖ {∅}) ↔ (𝐼 ∈ Fin ∧ 𝐼 ≠ ∅))
31	30	biimpri 228	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ Fin ∧ 𝐼 ≠ ∅) → 𝐼 ∈ (Fin ∖ {∅}))
32	4, 31	sylan 580	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅) → 𝐼 ∈ (Fin ∖ {∅}))
33	32	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → 𝐼 ∈ (Fin ∖ {∅}))
34		curf 37738	. . . . . . . . . . . . . 14 ⊢ ((𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅) ∧ 𝐼 ∈ (Fin ∖ {∅}) ∧ (Base‘𝑅) ∈ V) → curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))
35	22, 34	mp3an3 1452	. . . . . . . . . . . . 13 ⊢ ((𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅) ∧ 𝐼 ∈ (Fin ∖ {∅})) → curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))
36	29, 33, 35	syl2anc 584	. . . . . . . . . . . 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 20667	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring)
44		eqid 2734	. . . . . . . . . . . . . 14 ⊢ (𝑅 unitVec 𝐼) = (𝑅 unitVec 𝐼)
45		eqid 2734	. . . . . . . . . . . . . 14 ⊢ (𝑅 freeLMod 𝐼) = (𝑅 freeLMod 𝐼)
46		eqid 2734	. . . . . . . . . . . . . 14 ⊢ (Base‘(𝑅 freeLMod 𝐼)) = (Base‘(𝑅 freeLMod 𝐼))
47	44, 45, 46	uvcff 21744	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (𝑅 unitVec 𝐼):𝐼⟶(Base‘(𝑅 freeLMod 𝐼)))
48	43, 47	sylan 580	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑅 unitVec 𝐼):𝐼⟶(Base‘(𝑅 freeLMod 𝐼)))
49	48	ffvelcdmda 7027	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) → ((𝑅 unitVec 𝐼)‘𝑖) ∈ (Base‘(𝑅 freeLMod 𝐼)))
50	49	ad4ant14 752	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖 ∈ 𝐼) → ((𝑅 unitVec 𝐼)‘𝑖) ∈ (Base‘(𝑅 freeLMod 𝐼)))
51		ffn 6660	. . . . . . . . . . . . . . . 16 ⊢ (curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) → curry 𝑀 Fn 𝐼)
52		fnima 6620	. . . . . . . . . . . . . . . 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 6836	. . . . . . . . . . . . 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 21702	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (𝑅 freeLMod 𝐼) ∈ LMod)
60	43, 59	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑅 freeLMod 𝐼) ∈ LMod)
61	60	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → (𝑅 freeLMod 𝐼) ∈ LMod)
62		lindfrn 21774	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 freeLMod 𝐼) ∈ LMod ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ran curry 𝑀 ∈ (LIndS‘(𝑅 freeLMod 𝐼)))
63	61, 62	sylan 580	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ran curry 𝑀 ∈ (LIndS‘(𝑅 freeLMod 𝐼)))
64	45	frlmsca 21706	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝑅 = (Scalar‘(𝑅 freeLMod 𝐼)))
65		drngnzr 20679	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing)
66	65	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝑅 ∈ NzRing)
67	64, 66	eqeltrrd 2835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing)
68	60, 67	jca 511	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing))
69		eqid 2734	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Scalar‘(𝑅 freeLMod 𝐼)) = (Scalar‘(𝑅 freeLMod 𝐼))
70	46, 69	lindff1 21773	. . . . . . . . . . . . . . . . . . . . 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 580	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:dom curry 𝑀–1-1→(Base‘(𝑅 freeLMod 𝐼)))
73		fdm 6669	. . . . . . . . . . . . . . . . . . 19 ⊢ (curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) → dom curry 𝑀 = 𝐼)
74		f1eq2 6724	. . . . . . . . . . . . . . . . . . . 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 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → curry 𝑀:𝐼–1-1→(Base‘(𝑅 freeLMod 𝐼)))
77	76	an32s 652	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:𝐼–1-1→(Base‘(𝑅 freeLMod 𝐼)))
78		f1f1orn 6783	. . . . . . . . . . . . . . . . 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 8905	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ Fin ∧ curry 𝑀:𝐼–1-1-onto→ran curry 𝑀) → 𝐼 ≈ ran curry 𝑀)
81	58, 79, 80	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → 𝐼 ≈ ran curry 𝑀)
82	81	ensymd 8940	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ran curry 𝑀 ≈ 𝐼)
83		lindsenlbs 37755	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ ran curry 𝑀 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ ran curry 𝑀 ≈ 𝐼) → ran curry 𝑀 ∈ (LBasis‘(𝑅 freeLMod 𝐼)))
84	57, 58, 63, 82, 83	syl31anc 1375	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ran curry 𝑀 ∈ (LBasis‘(𝑅 freeLMod 𝐼)))
85		eqid 2734	. . . . . . . . . . . . . 14 ⊢ (LBasis‘(𝑅 freeLMod 𝐼)) = (LBasis‘(𝑅 freeLMod 𝐼))
86		eqid 2734	. . . . . . . . . . . . . 14 ⊢ (LSpan‘(𝑅 freeLMod 𝐼)) = (LSpan‘(𝑅 freeLMod 𝐼))
87	46, 85, 86	lbssp 21029	. . . . . . . . . . . . 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 2769	. . . . . . . . . . 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 2837	. . . . . . . . 9 ⊢ (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖 ∈ 𝐼) → ((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)))
92		eqid 2734	. . . . . . . . . . . . 13 ⊢ (Base‘(Scalar‘(𝑅 freeLMod 𝐼))) = (Base‘(Scalar‘(𝑅 freeLMod 𝐼)))
93		eqid 2734	. . . . . . . . . . . . 13 ⊢ (0g‘(Scalar‘(𝑅 freeLMod 𝐼))) = (0g‘(Scalar‘(𝑅 freeLMod 𝐼)))
94		eqid 2734	. . . . . . . . . . . . 13 ⊢ ( ·𝑠 ‘(𝑅 freeLMod 𝐼)) = ( ·𝑠 ‘(𝑅 freeLMod 𝐼))
95	45, 14	frlmfibas 21715	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m 𝐼) = (Base‘(𝑅 freeLMod 𝐼)))
96	95	feq3d 6645	. . . . . . . . . . . . . 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 21756	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → (((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) ↔ ∃𝑛 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = ((𝑅 freeLMod 𝐼) Σg (𝑛 ∘f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀))))
101	45	frlmsca 21706	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → 𝑅 = (Scalar‘(𝑅 freeLMod 𝐼)))
102	101	fveq2d 6836	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (Base‘𝑅) = (Base‘(Scalar‘(𝑅 freeLMod 𝐼))))
103	102	oveq1d 7371	. . . . . . . . . . . . . 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 8784	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ((Base‘𝑅) ↑m 𝐼) → 𝑛:𝐼⟶(Base‘𝑅))
106		ffn 6660	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛:𝐼⟶(Base‘𝑅) → 𝑛 Fn 𝐼)
107	106	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → 𝑛 Fn 𝐼)
108	51	ad2antlr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → curry 𝑀 Fn 𝐼)
109		simpllr 775	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → 𝐼 ∈ Fin)
110		inidm 4177	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐼 ∩ 𝐼) = 𝐼
111		eqidd 2735	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝑛‘𝑘) = (𝑛‘𝑘))
112		eqidd 2735	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘) = (curry 𝑀‘𝑘))
113	107, 108, 109, 109, 110, 111, 112	offval 7629	. . . . . . . . . . . . . . . . . 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 7024	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛:𝐼⟶(Base‘𝑅) ∧ 𝑘 ∈ 𝐼) → (𝑛‘𝑘) ∈ (Base‘𝑅))
116	115	adantll 714	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝑛‘𝑘) ∈ (Base‘𝑅))
117		ffvelcdm 7024	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘) ∈ ((Base‘𝑅) ↑m 𝐼))
118	117	ad4ant24 754	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘) ∈ ((Base‘𝑅) ↑m 𝐼))
119	95	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → ((Base‘𝑅) ↑m 𝐼) = (Base‘(𝑅 freeLMod 𝐼)))
120	118, 119	eleqtrd 2836	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘) ∈ (Base‘(𝑅 freeLMod 𝐼)))
121		eqid 2734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (.r‘𝑅) = (.r‘𝑅)
122	45, 46, 14, 114, 116, 120, 94, 121	frlmvscafval 21719	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝑛‘𝑘)( ·𝑠 ‘(𝑅 freeLMod 𝐼))(curry 𝑀‘𝑘)) = ((𝐼 × {(𝑛‘𝑘)}) ∘f (.r‘𝑅)(curry 𝑀‘𝑘)))
123		fvex 6845	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛‘𝑘) ∈ V
124		fnconstg 6720	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛‘𝑘) ∈ V → (𝐼 × {(𝑛‘𝑘)}) Fn 𝐼)
125	123, 124	mp1i 13	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝐼 × {(𝑛‘𝑘)}) Fn 𝐼)
126		elmapfn 8800	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((curry 𝑀‘𝑘) ∈ ((Base‘𝑅) ↑m 𝐼) → (curry 𝑀‘𝑘) Fn 𝐼)
127	117, 126	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘) Fn 𝐼)
128	127	ad4ant24 754	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘) Fn 𝐼)
129	123	fvconst2 7148	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ 𝐼 → ((𝐼 × {(𝑛‘𝑘)})‘𝑗) = (𝑛‘𝑘))
130	129	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((𝐼 × {(𝑛‘𝑘)})‘𝑗) = (𝑛‘𝑘))
131		eqidd 2735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((curry 𝑀‘𝑘)‘𝑗) = ((curry 𝑀‘𝑘)‘𝑗))
132	125, 128, 114, 114, 110, 130, 131	offval 7629	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝐼 × {(𝑛‘𝑘)}) ∘f (.r‘𝑅)(curry 𝑀‘𝑘)) = (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))
133	122, 132	eqtrd 2769	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝑛‘𝑘)( ·𝑠 ‘(𝑅 freeLMod 𝐼))(curry 𝑀‘𝑘)) = (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))
134	133	mpteq2dva 5189	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)( ·𝑠 ‘(𝑅 freeLMod 𝐼))(curry 𝑀‘𝑘))) = (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))))
135	113, 134	eqtrd 2769	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑛 ∘f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀) = (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))))
136	135	oveq2d 7372	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → ((𝑅 freeLMod 𝐼) Σg (𝑛 ∘f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀)) = ((𝑅 freeLMod 𝐼) Σg (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))))
137		eqid 2734	. . . . . . . . . . . . . . . . 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 753	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑛‘𝑘) ∈ (Base‘𝑅))
141		simplr 768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))
142		elmapi 8784	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((curry 𝑀‘𝑘) ∈ ((Base‘𝑅) ↑m 𝐼) → (curry 𝑀‘𝑘):𝐼⟶(Base‘𝑅))
143	117, 142	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘):𝐼⟶(Base‘𝑅))
144	143	ffvelcdmda 7027	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((curry 𝑀‘𝑘)‘𝑗) ∈ (Base‘𝑅))
145	141, 144	sylanl1 680	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((curry 𝑀‘𝑘)‘𝑗) ∈ (Base‘𝑅))
146	14, 121	ringcl 20183	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ (𝑛‘𝑘) ∈ (Base‘𝑅) ∧ ((curry 𝑀‘𝑘)‘𝑗) ∈ (Base‘𝑅)) → ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)) ∈ (Base‘𝑅))
147	139, 140, 145, 146	syl3anc 1373	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)) ∈ (Base‘𝑅))
148	147	fmpttd 7058	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))):𝐼⟶(Base‘𝑅))
149		elmapg 8774	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((Base‘𝑅) ∈ V ∧ 𝐼 ∈ Fin) → ((𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ ((Base‘𝑅) ↑m 𝐼) ↔ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))):𝐼⟶(Base‘𝑅)))
150	22, 149	mpan 690	. . . . . . . . . . . . . . . . . . . . 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 2820	. . . . . . . . . . . . . . . . . . . 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 730	. . . . . . . . . . . . . . . . . 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 7165	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐼 ∈ Fin → (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ V)
157	156	ralrimivw 3130	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ Fin → ∀𝑘 ∈ 𝐼 (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ V)
158		eqid 2734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))) = (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))
159	158	fnmpt 6630	. . . . . . . . . . . . . . . . . . . 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 6847	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐼 ∈ Fin → (0g‘(𝑅 freeLMod 𝐼)) ∈ V)
163	160, 161, 162	fndmfifsupp 9279	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐼 ∈ Fin → (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))) finSupp (0g‘(𝑅 freeLMod 𝐼)))
164	163	ad3antlr 731	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))) finSupp (0g‘(𝑅 freeLMod 𝐼)))
165	45, 46, 137, 109, 109, 138, 155, 164	frlmgsum 21725	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → ((𝑅 freeLMod 𝐼) Σg (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))))
166	136, 165	eqtr2d 2770	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) = ((𝑅 freeLMod 𝐼) Σg (𝑛 ∘f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀)))
167	105, 166	sylan2 593	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)) → (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) = ((𝑅 freeLMod 𝐼) Σg (𝑛 ∘f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀)))
168	167	eqeq2d 2745	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ((𝑅 unitVec 𝐼)‘𝑖) = ((𝑅 freeLMod 𝐼) Σg (𝑛 ∘f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀))))
169	104, 168	rexeqbidva 3301	. . . . . . . . . . . 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 680	. . . . . . . . . 10 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → (((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) ↔ ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))))))
172	171	ad2antrr 726	. . . . . . . . 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 3126	. . . . . . 7 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))))
175	42, 174	sylan 580	. . . . . 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 8800	. . . . . . . . 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 646	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗 ∈ 𝐼) ∧ 𝑘 ∈ 𝐼) ↔ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼))
181		df-3an 1088	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ 𝐼) ↔ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼))
182	180, 181	bitr4i 278	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗 ∈ 𝐼) ∧ 𝑘 ∈ 𝐼) ↔ (𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ 𝐼))
183		curfv 37740	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ 𝐼) ∧ 𝐼 ∈ Fin) → ((curry 𝑀‘𝑘)‘𝑗) = (𝑘𝑀𝑗))
184	182, 183	sylanb 581	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗 ∈ 𝐼) ∧ 𝑘 ∈ 𝐼) ∧ 𝐼 ∈ Fin) → ((curry 𝑀‘𝑘)‘𝑗) = (𝑘𝑀𝑗))
185	184	an32s 652	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗 ∈ 𝐼) ∧ 𝐼 ∈ Fin) ∧ 𝑘 ∈ 𝐼) → ((curry 𝑀‘𝑘)‘𝑗) = (𝑘𝑀𝑗))
186	185	oveq2d 7372	. . . . . . . . . . . . . . 15 ⊢ ((((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗 ∈ 𝐼) ∧ 𝐼 ∈ Fin) ∧ 𝑘 ∈ 𝐼) → ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)) = ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))
187	186	mpteq2dva 5189	. . . . . . . . . . . . . 14 ⊢ (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗 ∈ 𝐼) ∧ 𝐼 ∈ Fin) → (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) = (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))
188	187	an32s 652	. . . . . . . . . . . . 13 ⊢ (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) ∧ 𝑗 ∈ 𝐼) → (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) = (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))
189	188	oveq2d 7372	. . . . . . . . . . . 12 ⊢ (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) ∧ 𝑗 ∈ 𝐼) → (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))) = (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
190	189	mpteq2dva 5189	. . . . . . . . . . 11 ⊢ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) → (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))))
191	190	eqeq2d 2745	. . . . . . . . . 10 ⊢ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
192	191	rexbidv 3158	. . . . . . . . 9 ⊢ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) → (∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
193	192	ralbidv 3157	. . . . . . . 8 ⊢ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) → (∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
194	178, 179, 193	syl2anc 584	. . . . . . 7 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
195	194	ad2antrr 726	. . . . . 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 680	. . . 4 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))))
198		fveq1 6831	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑓‘𝑖) → (𝑛‘𝑘) = ((𝑓‘𝑖)‘𝑘))
199		uncov 37741	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ V ∧ 𝑘 ∈ V) → (𝑖uncurry 𝑓𝑘) = ((𝑓‘𝑖)‘𝑘))
200	199	el2v 3445	. . . . . . . . . . 11 ⊢ (𝑖uncurry 𝑓𝑘) = ((𝑓‘𝑖)‘𝑘)
201	198, 200	eqtr4di 2787	. . . . . . . . . 10 ⊢ (𝑛 = (𝑓‘𝑖) → (𝑛‘𝑘) = (𝑖uncurry 𝑓𝑘))
202	201	oveq1d 7371	. . . . . . . . 9 ⊢ (𝑛 = (𝑓‘𝑖) → ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)) = ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))
203	202	mpteq2dv 5190	. . . . . . . 8 ⊢ (𝑛 = (𝑓‘𝑖) → (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))) = (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))
204	203	oveq2d 7372	. . . . . . 7 ⊢ (𝑛 = (𝑓‘𝑖) → (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))) = (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
205	204	mpteq2dv 5190	. . . . . 6 ⊢ (𝑛 = (𝑓‘𝑖) → (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))))
206	205	eqeq2d 2745	. . . . 5 ⊢ (𝑛 = (𝑓‘𝑖) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) ↔ ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
207	206	ac6sfi 9182	. . . 4 ⊢ ((𝐼 ∈ Fin ∧ ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → ∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
208	5, 197, 207	syl2anc 584	. . 3 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
209		uncf 37739	. . . . . . 7 ⊢ (𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) → uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅))
210	13, 14	frlmfibas 21715	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ Field ∧ (𝐼 × 𝐼) ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
211	12, 210	sylan2 593	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
212	1, 13	matbas 22355	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ Field) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
213	212	ancoms 458	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
214	211, 213	eqtrd 2769	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
215	4, 214	sylan2 593	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
216	215	eleq2d 2820	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (uncurry 𝑓 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅))))
217		elmapg 8774	. . . . . . . . . . . . . 14 ⊢ (((Base‘𝑅) ∈ V ∧ (𝐼 × 𝐼) ∈ Fin) → (uncurry 𝑓 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)))
218	22, 23, 217	sylancr 587	. . . . . . . . . . . . 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 1915	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗(((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼)
224		nfmpt1 5195	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗(𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
225	224	nfeq2 2914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
226		fveq1 6831	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) → (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗) = ((𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))‘𝑗))
227	7, 43	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∈ Field → 𝑅 ∈ Ring)
228	227, 4	anim12i 613	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑅 ∈ Ring ∧ 𝐼 ∈ Fin))
229	228	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (𝑅 ∈ Ring ∧ 𝐼 ∈ Fin))
230		equcom 2019	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑗 ↔ 𝑗 = 𝑖)
231		ifbi 4500	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖 = 𝑗 ↔ 𝑗 = 𝑖) → if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)) = if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅)))
232	230, 231	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)) = if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))
233		eqid 2734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1r‘𝑅) = (1r‘𝑅)
234		eqid 2734	. . . . . . . . . . . . . . . . . . . . 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 2734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1r‘(𝐼 Mat 𝑅)) = (1r‘(𝐼 Mat 𝑅))
240	1, 233, 234, 235, 236, 237, 238, 239	mat1ov 22390	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)))
241		df-3an 1088	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin ∧ 𝑖 ∈ 𝐼) ↔ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼))
242	44, 233, 234	uvcvval 21739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗) = if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅)))
243	241, 242	sylanbr 582	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗) = if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅)))
244	232, 240, 243	3eqtr4a 2795	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗))
245	229, 244	sylanl1 680	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗))
246		ovex 7389	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))) ∈ V
247		eqid 2734	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
248	247	fvmpt2 6950	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ 𝐼 ∧ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))) ∈ V) → ((𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))‘𝑗) = (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
249	246, 248	mpan2 691	. . . . . . . . . . . . . . . . . . . 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 2734	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩) = (𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)
252		simp-4l 782	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑅 ∈ Field)
253	4	ad4antlr 733	. . . . . . . . . . . . . . . . . . . 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 2837	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)))
258	257	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 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 22336	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑖(uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀)𝑗) = (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
262	1, 251	matmulr 22380	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ Field) → (𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩) = (.r‘(𝐼 Mat 𝑅)))
263	262	ancoms 458	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩) = (.r‘(𝐼 Mat 𝑅)))
264	263	oveqd 7373	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀))
265	264	oveqd 7373	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (𝑖(uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀)𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))
266	4, 265	sylan2 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑖(uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀)𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))
267	266	ad3antrrr 730	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑖(uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀)𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))
268	250, 261, 267	3eqtr2rd 2776	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗) = ((𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))‘𝑗))
269	245, 268	eqeq12d 2750	. . . . . . . . . . . . . . . . 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 3239	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) → ∀𝑗 ∈ 𝐼 (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
274	273	ralimdva 3146	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) → ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
275	1, 2, 239	mat1bas 22391	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (1r‘(𝐼 Mat 𝑅)) ∈ (Base‘(𝐼 Mat 𝑅)))
276	13, 14	frlmfibas 21715	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ Ring ∧ (𝐼 × 𝐼) ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
277	12, 276	sylan2 593	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
278	1, 13	matbas 22355	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ Ring) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
279	278	ancoms 458	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
280	277, 279	eqtrd 2769	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
281	275, 280	eleqtrrd 2837	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (1r‘(𝐼 Mat 𝑅)) ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)))
282		elmapfn 8800	. . . . . . . . . . . . . . . 16 ⊢ ((1r‘(𝐼 Mat 𝑅)) ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) → (1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼))
283	281, 282	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼))
284	227, 4, 283	syl2an 596	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼))
285	284	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼))
286	1	matring 22385	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐼 Mat 𝑅) ∈ Ring)
287	4, 227, 286	syl2anr 597	. . . . . . . . . . . . . . . . 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 2734	. . . . . . . . . . . . . . . . 17 ⊢ (.r‘(𝐼 Mat 𝑅)) = (.r‘(𝐼 Mat 𝑅))
291	2, 290	ringcl 20183	. . . . . . . . . . . . . . . 16 ⊢ (((𝐼 Mat 𝑅) ∈ Ring ∧ uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ∈ (Base‘(𝐼 Mat 𝑅)))
292	288, 221, 289, 291	syl3anc 1373	. . . . . . . . . . . . . . 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 2837	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)))
295		elmapfn 8800	. . . . . . . . . . . . . 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 7486	. . . . . . . . . . . . 13 ⊢ (((1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼) ∧ (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) Fn (𝐼 × 𝐼)) → ((1r‘(𝐼 Mat 𝑅)) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ↔ ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
298	285, 296, 297	syl2anc 584	. . . . . . . . . . . 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 2740	. . . . . . . . 9 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
302		oveq1 7363	. . . . . . . . . . 11 ⊢ (𝑛 = uncurry 𝑓 → (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀))
303	302	eqeq1d 2736	. . . . . . . . . 10 ⊢ (𝑛 = uncurry 𝑓 → ((𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)) ↔ (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))))
304	303	rspcev 3574	. . . . . . . . 9 ⊢ ((uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
305	222, 301, 304	syl2anc 584	. . . . . . . 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 604	. . . . . 6 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))))
308	307	exlimdv 1934	. . . . 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 715	. . 3 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ ∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
311	208, 310	syldan 591	. 2 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
312	6	simprbi 496	. . . 4 ⊢ (𝑅 ∈ Field → 𝑅 ∈ CRing)
313		eqid 2734	. . . . . . . . . 10 ⊢ (𝐼 maDet 𝑅) = (𝐼 maDet 𝑅)
314	313, 1, 2, 14	mdetcl 22538	. . . . . . . . 9 ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Base‘𝑅))
315	313, 1, 2, 14	mdetcl 22538	. . . . . . . . 9 ⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘𝑛) ∈ (Base‘𝑅))
316		eqid 2734	. . . . . . . . . 10 ⊢ (∥r‘𝑅) = (∥r‘𝑅)
317	14, 316, 121	dvdsrmul 20298	. . . . . . . . 9 ⊢ ((((𝐼 maDet 𝑅)‘𝑀) ∈ (Base‘𝑅) ∧ ((𝐼 maDet 𝑅)‘𝑛) ∈ (Base‘𝑅)) → ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
318	314, 315, 317	syl2an 596	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑅 ∈ CRing ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
319	318	anandis 678	. . . . . . 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 717	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
322		fveq2 6832	. . . . . . . . 9 ⊢ ((𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)) → ((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))))
323	1, 2, 313, 121, 290	mdetmul 22565	. . . . . . . . . . . 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 652	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = (((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
326	313, 1, 239, 233	mdet1 22543	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ Fin) → ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))) = (1r‘𝑅))
327	4, 326	sylan2 593	. . . . . . . . . . 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 2750	. . . . . . . . 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 5108	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → (((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)) ↔ ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(1r‘𝑅)))
333		eqid 2734	. . . . . . . 8 ⊢ (Unit‘𝑅) = (Unit‘𝑅)
334	333, 233, 316	crngunit 20312	. . . . . . 7 ⊢ (𝑅 ∈ CRing → (((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅) ↔ ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(1r‘𝑅)))
335	334	ad2antrr 726	. . . . . 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 680	. . 3 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))
339	338	ad4ant14 752	. 2 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))
340	311, 339	rexlimddv 3141	1 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541  ∃wex 1780   ∈ wcel 2113   ≠ wne 2930  ∀wral 3049  ∃wrex 3058  Vcvv 3438   ∖ cdif 3896  ∅c0 4283  ifcif 4477  {csn 4578  ⟨cotp 4586   class class class wbr 5096   ↦ cmpt 5177   × cxp 5620  dom cdm 5622  ran crn 5623   “ cima 5625   Fn wfn 6485  ⟶wf 6486  –1-1→wf1 6487  –1-1-onto→wf1o 6489  ‘cfv 6490  (class class class)co 7356   ∘_f cof 7618  curry ccur 8205  uncurry cunc 8206   ↑_m cmap 8761   ≈ cen 8878  Fincfn 8881   finSupp cfsupp 9262  Basecbs 17134  ._rcmulr 17176  Scalarcsca 17178   ·_𝑠 cvsca 17179  0_gc0g 17357   Σ_g cgsu 17358  1_rcur 20114  Ringcrg 20166  CRingccrg 20167  ∥_rcdsr 20288  Unitcui 20289  NzRingcnzr 20443  DivRingcdr 20660  Fieldcfield 20661  LModclmod 20809  LSpanclspn 20920  LBasisclbs 21024   freeLMod cfrlm 21699   unitVec cuvc 21735   LIndF clindf 21757  LIndSclinds 21758   maMul cmmul 22332   Mat cmat 22349   maDet cmdat 22526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-rep 5222  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-cnex 11080  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-mulcom 11088  ax-addass 11089  ax-mulass 11090  ax-distr 11091  ax-i2m1 11092  ax-1ne0 11093  ax-1rid 11094  ax-rnegex 11095  ax-rrecex 11096  ax-cnre 11097  ax-pre-lttri 11098  ax-pre-lttrn 11099  ax-pre-ltadd 11100  ax-pre-mulgt0 11101  ax-addf 11103  ax-mulf 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-xor 1513  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rmo 3348  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-tp 4583  df-op 4585  df-ot 4587  df-uni 4862  df-int 4901  df-iun 4946  df-iin 4947  df-br 5097  df-opab 5159  df-mpt 5178  df-tr 5204  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-se 5576  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-isom 6499  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-of 7620  df-om 7807  df-1st 7931  df-2nd 7932  df-supp 8101  df-tpos 8166  df-cur 8207  df-unc 8208  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-2o 8396  df-er 8633  df-map 8763  df-pm 8764  df-ixp 8834  df-en 8882  df-dom 8883  df-sdom 8884  df-fin 8885  df-fsupp 9263  df-sup 9343  df-oi 9413  df-card 9849  df-pnf 11166  df-mnf 11167  df-xr 11168  df-ltxr 11169  df-le 11170  df-sub 11364  df-neg 11365  df-div 11793  df-nn 12144  df-2 12206  df-3 12207  df-4 12208  df-5 12209  df-6 12210  df-7 12211  df-8 12212  df-9 12213  df-n0 12400  df-xnn0 12473  df-z 12487  df-dec 12606  df-uz 12750  df-rp 12904  df-fz 13422  df-fzo 13569  df-seq 13923  df-exp 13983  df-hash 14252  df-word 14435  df-lsw 14484  df-concat 14492  df-s1 14518  df-substr 14563  df-pfx 14593  df-splice 14671  df-reverse 14680  df-s2 14769  df-struct 17072  df-sets 17089  df-slot 17107  df-ndx 17119  df-base 17135  df-ress 17156  df-plusg 17188  df-mulr 17189  df-starv 17190  df-sca 17191  df-vsca 17192  df-ip 17193  df-tset 17194  df-ple 17195  df-ds 17197  df-unif 17198  df-hom 17199  df-cco 17200  df-0g 17359  df-gsum 17360  df-prds 17365  df-pws 17367  df-mre 17503  df-mrc 17504  df-mri 17505  df-acs 17506  df-mgm 18563  df-sgrp 18642  df-mnd 18658  df-mhm 18706  df-submnd 18707  df-efmnd 18792  df-grp 18864  df-minusg 18865  df-sbg 18866  df-mulg 18996  df-subg 19051  df-ghm 19140  df-gim 19186  df-cntz 19244  df-oppg 19273  df-symg 19297  df-pmtr 19369  df-psgn 19418  df-evpm 19419  df-cmn 19709  df-abl 19710  df-mgp 20074  df-rng 20086  df-ur 20115  df-srg 20120  df-ring 20168  df-cring 20169  df-oppr 20271  df-dvdsr 20291  df-unit 20292  df-invr 20322  df-dvr 20335  df-rhm 20406  df-nzr 20444  df-subrng 20477  df-subrg 20501  df-drng 20662  df-field 20663  df-lmod 20811  df-lss 20881  df-lsp 20921  df-lmhm 20972  df-lbs 21025  df-lvec 21053  df-sra 21123  df-rgmod 21124  df-cnfld 21308  df-zring 21400  df-zrh 21456  df-dsmm 21685  df-frlm 21700  df-uvc 21736  df-lindf 21759  df-linds 21760  df-mamu 22333  df-mat 22350  df-mdet 22527

This theorem is referenced by:  matunitlindf  37758