Theorem mat1dimelbas

Description: A matrix with dimension 1 is an ordered pair with an ordered pair (of the one and only pair of indices) as first component. (Contributed by AV, 15-Aug-2019)

	Ref	Expression
Hypotheses	mat1dim.a	⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
	mat1dim.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	mat1dim.o	⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
Assertion	mat1dimelbas	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑀 ∈ ( Base ‘ 𝐴 ) ↔ ∃ 𝑟 ∈ 𝐵 𝑀 = { ⟨ 𝑂 , 𝑟 ⟩ } ) )

Proof

Step	Hyp	Ref	Expression
1		mat1dim.a	⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
2		mat1dim.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		mat1dim.o	⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
4		snfi	⊢ { 𝐸 } ∈ Fin
5		simpl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝑅 ∈ Ring )
6	1 2	matbas2	⊢ ( ( { 𝐸 } ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐵 ↑m ( { 𝐸 } × { 𝐸 } ) ) = ( Base ‘ 𝐴 ) )
7	6	eqcomd	⊢ ( ( { 𝐸 } ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝐴 ) = ( 𝐵 ↑m ( { 𝐸 } × { 𝐸 } ) ) )
8	7	eleq2d	⊢ ( ( { 𝐸 } ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑀 ∈ ( Base ‘ 𝐴 ) ↔ 𝑀 ∈ ( 𝐵 ↑m ( { 𝐸 } × { 𝐸 } ) ) ) )
9	4 5 8	sylancr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑀 ∈ ( Base ‘ 𝐴 ) ↔ 𝑀 ∈ ( 𝐵 ↑m ( { 𝐸 } × { 𝐸 } ) ) ) )
10	2	fvexi	⊢ 𝐵 ∈ V
11		snex	⊢ { 𝐸 } ∈ V
12	11 11	pm3.2i	⊢ ( { 𝐸 } ∈ V ∧ { 𝐸 } ∈ V )
13		xpexg	⊢ ( ( { 𝐸 } ∈ V ∧ { 𝐸 } ∈ V ) → ( { 𝐸 } × { 𝐸 } ) ∈ V )
14	12 13	mp1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( { 𝐸 } × { 𝐸 } ) ∈ V )
15		elmapg	⊢ ( ( 𝐵 ∈ V ∧ ( { 𝐸 } × { 𝐸 } ) ∈ V ) → ( 𝑀 ∈ ( 𝐵 ↑m ( { 𝐸 } × { 𝐸 } ) ) ↔ 𝑀 : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ) )
16	10 14 15	sylancr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑀 ∈ ( 𝐵 ↑m ( { 𝐸 } × { 𝐸 } ) ) ↔ 𝑀 : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ) )
17	9 16	bitrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑀 ∈ ( Base ‘ 𝐴 ) ↔ 𝑀 : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ) )
18		xpsng	⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ) → ( { 𝐸 } × { 𝐸 } ) = { ⟨ 𝐸 , 𝐸 ⟩ } )
19	18	anidms	⊢ ( 𝐸 ∈ 𝑉 → ( { 𝐸 } × { 𝐸 } ) = { ⟨ 𝐸 , 𝐸 ⟩ } )
20	19	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( { 𝐸 } × { 𝐸 } ) = { ⟨ 𝐸 , 𝐸 ⟩ } )
21	20	feq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑀 : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ↔ 𝑀 : { ⟨ 𝐸 , 𝐸 ⟩ } ⟶ 𝐵 ) )
22		opex	⊢ ⟨ 𝐸 , 𝐸 ⟩ ∈ V
23	22	fsn2	⊢ ( 𝑀 : { ⟨ 𝐸 , 𝐸 ⟩ } ⟶ 𝐵 ↔ ( ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ∈ 𝐵 ∧ 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } ) )
24		risset	⊢ ( ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ∈ 𝐵 ↔ ∃ 𝑟 ∈ 𝐵 𝑟 = ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) )
25		eqcom	⊢ ( 𝑟 = ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ↔ ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑟 )
26	25	rexbii	⊢ ( ∃ 𝑟 ∈ 𝐵 𝑟 = ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ↔ ∃ 𝑟 ∈ 𝐵 ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑟 )
27	24 26	sylbb	⊢ ( ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ∈ 𝐵 → ∃ 𝑟 ∈ 𝐵 ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑟 )
28	27	ad2antrl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ∈ 𝐵 ∧ 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } ) ) → ∃ 𝑟 ∈ 𝐵 ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑟 )
29		eqeq1	⊢ ( 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } → ( 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ↔ { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ) )
30		opex	⊢ ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ ∈ V
31		sneqbg	⊢ ( ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ ∈ V → ( { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ↔ ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ = ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ ) )
32	30 31	ax-mp	⊢ ( { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ↔ ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ = ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ )
33		eqid	⊢ ⟨ 𝐸 , 𝐸 ⟩ = ⟨ 𝐸 , 𝐸 ⟩
34		vex	⊢ 𝑟 ∈ V
35	22 34	opth2	⊢ ( ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ = ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ ↔ ( ⟨ 𝐸 , 𝐸 ⟩ = ⟨ 𝐸 , 𝐸 ⟩ ∧ ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑟 ) )
36	33 35	mpbiran	⊢ ( ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ = ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ ↔ ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑟 )
37	32 36	bitri	⊢ ( { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ↔ ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑟 )
38	29 37	bitrdi	⊢ ( 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } → ( 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ↔ ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑟 ) )
39	38	adantl	⊢ ( ( ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ∈ 𝐵 ∧ 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } ) → ( 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ↔ ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑟 ) )
40	39	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ∈ 𝐵 ∧ 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } ) ) → ( 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ↔ ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑟 ) )
41	40	rexbidv	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ∈ 𝐵 ∧ 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } ) ) → ( ∃ 𝑟 ∈ 𝐵 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ↔ ∃ 𝑟 ∈ 𝐵 ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑟 ) )
42	28 41	mpbird	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ∈ 𝐵 ∧ 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } ) ) → ∃ 𝑟 ∈ 𝐵 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } )
43	42	ex	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( ( ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ∈ 𝐵 ∧ 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } ) → ∃ 𝑟 ∈ 𝐵 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ) )
44	23 43	syl5bi	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑀 : { ⟨ 𝐸 , 𝐸 ⟩ } ⟶ 𝐵 → ∃ 𝑟 ∈ 𝐵 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ) )
45	21 44	sylbid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑀 : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 → ∃ 𝑟 ∈ 𝐵 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ) )
46		f1o2sn	⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝑟 ∈ 𝐵 ) → { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } : ( { 𝐸 } × { 𝐸 } ) –1-1-onto→ { 𝑟 } )
47		f1of	⊢ ( { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } : ( { 𝐸 } × { 𝐸 } ) –1-1-onto→ { 𝑟 } → { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } : ( { 𝐸 } × { 𝐸 } ) ⟶ { 𝑟 } )
48	46 47	syl	⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝑟 ∈ 𝐵 ) → { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } : ( { 𝐸 } × { 𝐸 } ) ⟶ { 𝑟 } )
49	48	adantll	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑟 ∈ 𝐵 ) → { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } : ( { 𝐸 } × { 𝐸 } ) ⟶ { 𝑟 } )
50		snssi	⊢ ( 𝑟 ∈ 𝐵 → { 𝑟 } ⊆ 𝐵 )
51	50	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑟 ∈ 𝐵 ) → { 𝑟 } ⊆ 𝐵 )
52	49 51	fssd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑟 ∈ 𝐵 ) → { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 )
53		feq1	⊢ ( 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } → ( 𝑀 : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ↔ { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ) )
54	52 53	syl5ibrcom	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑟 ∈ 𝐵 ) → ( 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } → 𝑀 : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ) )
55	54	rexlimdva	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( ∃ 𝑟 ∈ 𝐵 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } → 𝑀 : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ) )
56	45 55	impbid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑀 : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ↔ ∃ 𝑟 ∈ 𝐵 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ) )
57	3	eqcomi	⊢ ⟨ 𝐸 , 𝐸 ⟩ = 𝑂
58	57	opeq1i	⊢ ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ = ⟨ 𝑂 , 𝑟 ⟩
59	58	sneqi	⊢ { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } = { ⟨ 𝑂 , 𝑟 ⟩ }
60	59	eqeq2i	⊢ ( 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ↔ 𝑀 = { ⟨ 𝑂 , 𝑟 ⟩ } )
61	60	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ↔ 𝑀 = { ⟨ 𝑂 , 𝑟 ⟩ } ) )
62	61	rexbidv	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( ∃ 𝑟 ∈ 𝐵 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ↔ ∃ 𝑟 ∈ 𝐵 𝑀 = { ⟨ 𝑂 , 𝑟 ⟩ } ) )
63	56 62	bitrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑀 : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ↔ ∃ 𝑟 ∈ 𝐵 𝑀 = { ⟨ 𝑂 , 𝑟 ⟩ } ) )
64	17 63	bitrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑀 ∈ ( Base ‘ 𝐴 ) ↔ ∃ 𝑟 ∈ 𝐵 𝑀 = { ⟨ 𝑂 , 𝑟 ⟩ } ) )