Theorem assapropd

Description: If two structures have the same components (properties), one is an associative algebra iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015)

	Ref	Expression
Hypotheses	assapropd.1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
	assapropd.2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
	assapropd.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
	assapropd.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) )
	assapropd.5	⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐾 ) )
	assapropd.6	⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐿 ) )
	assapropd.7	⊢ 𝑃 = ( Base ‘ 𝐹 )
	assapropd.8	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
Assertion	assapropd	⊢ ( 𝜑 → ( 𝐾 ∈ AssAlg ↔ 𝐿 ∈ AssAlg ) )

Proof

Step	Hyp	Ref	Expression
1		assapropd.1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2		assapropd.2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3		assapropd.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
4		assapropd.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) )
5		assapropd.5	⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐾 ) )
6		assapropd.6	⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐿 ) )
7		assapropd.7	⊢ 𝑃 = ( Base ‘ 𝐹 )
8		assapropd.8	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
9		assalmod	⊢ ( 𝐾 ∈ AssAlg → 𝐾 ∈ LMod )
10		assaring	⊢ ( 𝐾 ∈ AssAlg → 𝐾 ∈ Ring )
11	9 10	jca	⊢ ( 𝐾 ∈ AssAlg → ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) )
12	11	a1i	⊢ ( 𝜑 → ( 𝐾 ∈ AssAlg → ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) )
13		assalmod	⊢ ( 𝐿 ∈ AssAlg → 𝐿 ∈ LMod )
14	1 2 3 5 6 7 8	lmodpropd	⊢ ( 𝜑 → ( 𝐾 ∈ LMod ↔ 𝐿 ∈ LMod ) )
15	13 14	imbitrrid	⊢ ( 𝜑 → ( 𝐿 ∈ AssAlg → 𝐾 ∈ LMod ) )
16		assaring	⊢ ( 𝐿 ∈ AssAlg → 𝐿 ∈ Ring )
17	1 2 3 4	ringpropd	⊢ ( 𝜑 → ( 𝐾 ∈ Ring ↔ 𝐿 ∈ Ring ) )
18	16 17	imbitrrid	⊢ ( 𝜑 → ( 𝐿 ∈ AssAlg → 𝐾 ∈ Ring ) )
19	15 18	jcad	⊢ ( 𝜑 → ( 𝐿 ∈ AssAlg → ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) )
20	14 17	anbi12d	⊢ ( 𝜑 → ( ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ↔ ( 𝐿 ∈ LMod ∧ 𝐿 ∈ Ring ) ) )
21	20	adantr	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → ( ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ↔ ( 𝐿 ∈ LMod ∧ 𝐿 ∈ Ring ) ) )
22		simpll	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝜑 )
23		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝐾 ∈ LMod )
24		simprl	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑟 ∈ 𝑃 )
25	5	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝐹 ) = ( Base ‘ ( Scalar ‘ 𝐾 ) ) )
26	7 25	eqtrid	⊢ ( 𝜑 → 𝑃 = ( Base ‘ ( Scalar ‘ 𝐾 ) ) )
27	22 26	syl	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑃 = ( Base ‘ ( Scalar ‘ 𝐾 ) ) )
28	24 27	eleqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) )
29		simprrl	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑧 ∈ 𝐵 )
30	22 1	syl	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝐵 = ( Base ‘ 𝐾 ) )
31	29 30	eleqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐾 ) )
32		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
33		eqid	⊢ ( Scalar ‘ 𝐾 ) = ( Scalar ‘ 𝐾 )
34		eqid	⊢ ( ·𝑠 ‘ 𝐾 ) = ( ·𝑠 ‘ 𝐾 )
35		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝐾 ) ) = ( Base ‘ ( Scalar ‘ 𝐾 ) )
36	32 33 34 35	lmodvscl	⊢ ( ( 𝐾 ∈ LMod ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ∈ ( Base ‘ 𝐾 ) )
37	23 28 31 36	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ∈ ( Base ‘ 𝐾 ) )
38	37 30	eleqtrrd	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ∈ 𝐵 )
39		simprrr	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑤 ∈ 𝐵 )
40	4	oveqrspc2v	⊢ ( ( 𝜑 ∧ ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ( .r ‘ 𝐾 ) 𝑤 ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ( .r ‘ 𝐿 ) 𝑤 ) )
41	22 38 39 40	syl12anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ( .r ‘ 𝐾 ) 𝑤 ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ( .r ‘ 𝐿 ) 𝑤 ) )
42	8	oveqrspc2v	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑃 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) )
43	22 24 29 42	syl12anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) )
44	43	oveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ( .r ‘ 𝐿 ) 𝑤 ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ( .r ‘ 𝐿 ) 𝑤 ) )
45	41 44	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ( .r ‘ 𝐾 ) 𝑤 ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ( .r ‘ 𝐿 ) 𝑤 ) )
46		eqid	⊢ ( .r ‘ 𝐾 ) = ( .r ‘ 𝐾 )
47		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝐾 ∈ Ring )
48	39 30	eleqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑤 ∈ ( Base ‘ 𝐾 ) )
49	32 46 47 31 48	ringcld	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) )
50	49 30	eleqtrrd	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 )
51	8	oveqrspc2v	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) )
52	22 24 50 51	syl12anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) )
53	4	oveqrspc2v	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) = ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) )
54	22 29 39 53	syl12anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) = ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) )
55	54	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) )
56	52 55	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) )
57	45 56	eqeq12d	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ( .r ‘ 𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ↔ ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ( .r ‘ 𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ) )
58	32 33 34 35	lmodvscl	⊢ ( ( 𝐾 ∈ LMod ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) )
59	23 28 48 58	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) )
60	59 30	eleqtrrd	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 )
61	4	oveqrspc2v	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ) ) → ( 𝑧 ( .r ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑧 ( .r ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) )
62	22 29 60 61	syl12anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑧 ( .r ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑧 ( .r ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) )
63	8	oveqrspc2v	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
64	22 24 39 63	syl12anc	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
65	64	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑧 ( .r ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑧 ( .r ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) )
66	62 65	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑧 ( .r ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑧 ( .r ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) )
67	66 56	eqeq12d	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑧 ( .r ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ↔ ( 𝑧 ( .r ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ) )
68	57 67	anbi12d	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ( .r ‘ 𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ) ↔ ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ( .r ‘ 𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ) ) )
69	68	anassrs	⊢ ( ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ( .r ‘ 𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ) ↔ ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ( .r ‘ 𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ) ) )
70	69	2ralbidva	⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ 𝑟 ∈ 𝑃 ) → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ( .r ‘ 𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ) ↔ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ( .r ‘ 𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ) ) )
71	70	ralbidva	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → ( ∀ 𝑟 ∈ 𝑃 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ( .r ‘ 𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ) ↔ ∀ 𝑟 ∈ 𝑃 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ( .r ‘ 𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ) ) )
72	26	adantr	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → 𝑃 = ( Base ‘ ( Scalar ‘ 𝐾 ) ) )
73	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → 𝐵 = ( Base ‘ 𝐾 ) )
74	73	raleqdv	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → ( ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ( .r ‘ 𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ) ↔ ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ( .r ‘ 𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ) ) )
75	73 74	raleqbidv	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ( .r ‘ 𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ( .r ‘ 𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ) ) )
76	72 75	raleqbidv	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → ( ∀ 𝑟 ∈ 𝑃 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ( .r ‘ 𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ) ↔ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ( .r ‘ 𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ) ) )
77	6	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝐹 ) = ( Base ‘ ( Scalar ‘ 𝐿 ) ) )
78	7 77	eqtrid	⊢ ( 𝜑 → 𝑃 = ( Base ‘ ( Scalar ‘ 𝐿 ) ) )
79	78	adantr	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → 𝑃 = ( Base ‘ ( Scalar ‘ 𝐿 ) ) )
80	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → 𝐵 = ( Base ‘ 𝐿 ) )
81	80	raleqdv	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → ( ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ( .r ‘ 𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ) ↔ ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ( .r ‘ 𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ) ) )
82	80 81	raleqbidv	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ( .r ‘ 𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐿 ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ( .r ‘ 𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ) ) )
83	79 82	raleqbidv	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → ( ∀ 𝑟 ∈ 𝑃 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ( .r ‘ 𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ) ↔ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∀ 𝑧 ∈ ( Base ‘ 𝐿 ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ( .r ‘ 𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ) ) )
84	71 76 83	3bitr3d	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → ( ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ( .r ‘ 𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ) ↔ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∀ 𝑧 ∈ ( Base ‘ 𝐿 ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ( .r ‘ 𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ) ) )
85	21 84	anbi12d	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → ( ( ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ∧ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ( .r ‘ 𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ) ) ↔ ( ( 𝐿 ∈ LMod ∧ 𝐿 ∈ Ring ) ∧ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∀ 𝑧 ∈ ( Base ‘ 𝐿 ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ( .r ‘ 𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ) ) ) )
86	32 33 35 34 46	isassa	⊢ ( 𝐾 ∈ AssAlg ↔ ( ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ∧ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ( .r ‘ 𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑧 ( .r ‘ 𝐾 ) 𝑤 ) ) ) ) )
87		eqid	⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
88		eqid	⊢ ( Scalar ‘ 𝐿 ) = ( Scalar ‘ 𝐿 )
89		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝐿 ) ) = ( Base ‘ ( Scalar ‘ 𝐿 ) )
90		eqid	⊢ ( ·𝑠 ‘ 𝐿 ) = ( ·𝑠 ‘ 𝐿 )
91		eqid	⊢ ( .r ‘ 𝐿 ) = ( .r ‘ 𝐿 )
92	87 88 89 90 91	isassa	⊢ ( 𝐿 ∈ AssAlg ↔ ( ( 𝐿 ∈ LMod ∧ 𝐿 ∈ Ring ) ∧ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∀ 𝑧 ∈ ( Base ‘ 𝐿 ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ( .r ‘ 𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑧 ( .r ‘ 𝐿 ) 𝑤 ) ) ) ) )
93	85 86 92	3bitr4g	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → ( 𝐾 ∈ AssAlg ↔ 𝐿 ∈ AssAlg ) )
94	93	ex	⊢ ( 𝜑 → ( ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) → ( 𝐾 ∈ AssAlg ↔ 𝐿 ∈ AssAlg ) ) )
95	12 19 94	pm5.21ndd	⊢ ( 𝜑 → ( 𝐾 ∈ AssAlg ↔ 𝐿 ∈ AssAlg ) )